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
|
The debug-me protocol is a series of JSON objects, exchanged between
the two participants, known as the user and the developer.
The exact composition of the JSON objects is not described here; see
Types.hs for the data types that JSON serialization instances are derived
from. The Activity type is the main message type.
The first message in a debug-me session is sent by the user, and it has
Nothing as its prevActivity. All subsequent messages sent by either the
user or the developer must have a prevActivity that points to the Hash
of a previous message. So a chain of messages is built up.
The exact details about how these 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 either:
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 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 very first
message in the protocol is the user sending their session pubic key.
Before the developer can do anything, they must send a 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 will 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.
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.
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 its
prevActivity points to, etc.
|
