ept

theory
  Consensus_Demo
imports
  Network
begin

datatype 'val msg
  = Propose 'val
  | Accept 'val

ept

# Parameters:
prob_nodefail = 0.001     # Probability of a single node failing
replication_factor = 3    # Number of copies of each partition (r)
partitions_per_node = 256 # Number of partitions per node
max_nodes = 10000         # Maximum number of nodes to consider

# (n - r)! / n! == r! / (n choose r)
# Intuitively: the fraction of the n! possible permutations of n nodes that
# results in the replicas of one particular partition to be mapped to three
# particular nodes, in a particular order.

ept

How to add syntax-highlighted code to PowerPoint slides (Mac OS)

1. pygmentize -f rtf FILE | pbcopy
2. Paste into TextEdit (in rich text mode: Format → Make Rich Text before pasting), and copy to clipboard again.
3. In PowerPoint, Edit → Paste Special… → Styled Text.

(Pasting RTF directly into PowerPoint doesn't work correctly, at least with PowerPoint 2008 — it extends colour spans longer than it should, and sometimes removes line breaks. Going via TextEdit seems to solve the problem.)

ept

const ROOT_ID = '00000000-0000-0000-0000-000000000000'

/**
 * Miniature implementation of a subset of Automerge. Supports the following:
 *  - only map, list, and primitive datatypes (no table, text, counter, or date objects)
 *  - no undo/redo
 *  - no conflicts on concurrent updates to the same field (uses last-writer-wins instead)
 *  - no API for creating new changes (you need to create change objects yourself)
 *  - no buffering of changes that are missing their causal dependencies
 *  - no saving or loading in serialised form

ept

Notes from Coed:Ethics conference, London, 13 July 2018

Cori Crider - "When data kills" / Weaponised AI

• Imam Salem bin Ali Jaber preached in Yemen against Islamic extremism; guest at a wedding of relative; hit by a US Hellfire missile fired from a drone. Relative Faisal made contact with Cori, went to Washington DC. No explanation ever made by government (although compensation was paid).
• Decision-making process behind the attack not known exactly. But there is significant evidence that such attacks serve to further radicalise people; attack results in ~3x more new recruits than extremists killed by attack.
• Most drone attacks are not on named individuals, but rather "signature strikes" — a euphemism for killing people the military doesn't even know, but who match a certain behavioural pattern (perhaps based on metadata — Hayden: "we kill people based on metadata"
• Skynet (known through Snowden relevations): use machine learning to try to find courier

ept

import java.io.ByteArrayOutputStream;
import java.io.IOException;
import org.apache.avro.Schema;
import org.apache.avro.generic.GenericData;
import org.apache.avro.generic.GenericDatumReader;
import org.apache.avro.generic.GenericDatumWriter;
import org.apache.avro.generic.GenericRecordBuilder;
import org.apache.avro.io.BinaryDecoder;
import org.apache.avro.io.BinaryEncoder;
import org.apache.avro.io.DatumReader;

ept

Stylus input and the benefits of a standard

Notes from a talk by Mark Hayter

Mark Hayter is Senior Engineering Director in the Chrome OS Hardware team at Google, and currently a visitor from industry with the Computer Architecture team in the Computer Lab.

• 1990s: Apple Newton, Palm Pilot used graffiti input (one letter at a time, stylised), Lectrice
• 2000s: Microsoft Tablet PC

ept

import java.io.ByteArrayOutputStream;
import java.io.IOException;
import org.apache.avro.Schema;
import org.apache.avro.generic.GenericData;
import org.apache.avro.generic.GenericDatumReader;
import org.apache.avro.generic.GenericDatumWriter;
import org.apache.avro.generic.GenericRecordBuilder;
import org.apache.avro.io.BinaryDecoder;
import org.apache.avro.io.BinaryEncoder;
import org.apache.avro.io.DecoderFactory;

ept

TRVE Data update — November 2016

This update was sent by email to the TRVE Data mailing list on 1 December 2016. Please subscribe to the mailing list or follow us on Twitter for future updates.

Hello TRVE Data supporters,

Here's an update on what we've been doing in November.

• Stephan has made great progress on understanding Tor network traffic. He is now able to trace almost all data transfer through the various layers — application data, Tor circuits, calls to the OpenSSL library, down to actual network packets — and thus analyse each packet to determine why it was sent or received. This is especially important when using Tor on mobile devices, since every network packet uses battery energy and costs money (depending on your data plan). By labelling network packets, we can compare protocol changes to

ept

TRVE Data update — Sept/Oct 2016

Hello TRVE Data supporters,

Sorry for the lack of an update last month. Here's what we've been up to in September and October.

Diana and Martin presented an introduction to end-to-end encryption protocols at the Strange Loop conference in St Louis, and repeated the talk in Cambridge. We illustrated network communication and man-in-the-middle attacks by passing pieces of cardboard back and forth on the stage -- a visualisation that went down well with the audience.

Alastair and Martin have been working together with Dominic Mulligan and Victor Gomes, also researchers in Cambridge, on formalising our JSON CRDT definition using the Isabelle proof assistant. We are converting the hand-written convergence proof in our paper into a machine-checkable proof,