1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
The debug-me protocol is a series of messages, exchanged between
the two participants, known as the user and the developer.
The messages are serialized as JSON in debug-me log files, and protocol
buffers are used when sending the messages over the wire. We won't go into
the full details here. See Types.hs for the data types that JSON
serialization instances are derived from, and ProocolBuffers.hs for the
protocol buffers format. There is also a simple framing protocol used for
communicating over websockets; see WebSockets.hs.
The Activity type is the main message type. The user sends Activity
Seen messages, and the developer responds with Activity Entered.
There are also Control messages, which can be sent by either
party at any time, and do not affect IO to the console.
The first message in a debug-me session is a Control sent by the
user, which establishes a session key (see below for details). The second
message is an Activity Seen.
Activity Seen and Activity Entered messages have a prevActivity,
which points to the Hash of a previous Activity. (And is Nothing for the
first Activity Seen.) So a chain of messages is built up.
(The exact details about how objects are hashed is not described here;
see Hash.hs for the implementation. Note that the JSON strings are *not*
directly hashed (to avoid tying hashing to JSON serialization details),
instead the values in the data types are hashed.)
The user and developer have different points of view. For example,
the developer could send an Activity Entered at the same time the user
is sending an Activity Seen. It's not clear in which order these two
Activities occurred -- in fact they occurred in different orders in
different places -- and so the user and developer will disagree
about it.
Since the goal of debug-me is to produce a proof of the sequence of events
that occurred in a session, that is a problem. Perhaps the developer was
entering "y" in response to "Display detailed reactor logs?" at the same time
that a new "Vent core to atmosphere?" question was being displayed!
The debug-me protocol is designed to prevent such conflicts of opinion.
The user only processes a new Activity Entered when it meets one of these
requirements:
1. The Activity Entered has as its prevActivity the last Activity
(Entered or Seen) that the user processed.
2. The Activity Entered has as its prevActivity an older Activity
that the user processed, and its echoData matches the concacenation
of every Activity Seen after the prevActivity, up to the most recent
Activity Seen.
(This allows the developer to enter a command quickly without waiting
for each letter to echo back to them.)
When an Activity Entered does not meet these rules, the user sends
it back in a Rejected message to let the developer know the input was not
allowed.
The developer also checks the prevActivity of Activity Seen messages it
receives from the user, to make sure that it's receiving a valid chain of
messages. The developer accepts a new Activity Seen when either:
1. The Activity Seen has a prevActivity that points to the last
Activity Seen that the developer accepted.
2. The Activity Seen has as its prevActivity an Activity Entered
that the developer generated, after the last Activity Seen
that the developer accepted.
At the start of the debug-me session, Ed25519 session key pairs are
generated by both the user and the developer. The first message
in the protocol is the user sending their session pubic key
in a Control message containing a SessionKey.
Before the developer can enter anything, they must send a SessionKey message
with their session key, and it must be accepted by the user. The developer
must have a gpg private key, which is used to sign their session key.
(The user may have a gpg private key, which may sign their session key
if available, but this is optional.) The user will reject session keys
that are not signed by a gpg key or when the gpg key is not one they
trust. The user sends a SessionKeyAccepted/SessionKeyRejected control
message to indicate if they accepted the developer's key or not.
Each message in the debug-me session is signed by the party that sends it,
using their session key. The hash of a message includes its signature, so
the activity chain proves who sent a message, and who sent the message
before it, etc.
Note that there could be multiple developers, in which case each will
send their session key before being able to do anything except observe
the debug-me session.
The prevActivity hash is actually not included in the data sent across the
wire. It's left out to save space, and gets added back in by the receiver.
The receiver uses the signature of the message to tell when it's found
the right prevActivity hash to add back in.
|
