4 <F> live file, loaded on startup, updated by secnet
5 (only). * in-memory peerkeys_current is kept
8 <F>~update update file from config manager, checked before
9 every key exchange. config manager must rename
10 this file into place; it will be renamed and
11 then removed by secnet.
13 <F>~proc update file being processed by secnet.
14 only secnet may write or remove.
16 <F>~incoming update file from peer, being received by secnet
17 may be incomplete, unverified, or even malicious
18 only secnet may write or remove.
20 <F>~tmp update file from config manager, only mss may
23 secnet discards updates that are not more recent than (by
24 serial) the live file. But it may not process updates
27 The implied keyset to be used is MAX(live, proc, update).
30 check live vs proc, either mv proc live or rm proc
31 if proc doesn't exist, mv update proc
33 make-secnet-sites does:
34 write: rename something onto update
35 read: read update,proc,live in that order and take max
37 We support only one concurrent secnet, one concurrent
38 writing make-secnet-sites, and any number of readers.
39 We want to maintain a live file at all times as that
40 is what secnet actually reads at startup and uses.
42 Proof that this is sound:
43 Let us regard update,proc,live as i=0,1,2
44 Files contain public key sets and are manipulated as
45 a whole, and we may regard key sets with the same
47 We talk below about reading as if it were atomic.
48 Actually the atomic operation is open(2); the
49 reading gets whatever that name refers to. So
50 we can model this as an atomic read.
51 secnet eventually moves all data into the live file
52 or deletes it, so there should be no indefinitely
53 stale data; informally this means we can disregard
54 the possibility of very old serials and regard
55 serials as fully ordered. (We don't bother with
56 a formal proof of this property.)
57 Consequently we will only think about the serial
58 and not the contents. We treat absent files as
59 minimal (we will write -1 for convenience although
60 we don't mean a numerical value). We write S(i).
62 Invariant 1 for secnet's transformations is as follows:
63 Each file S(i) is only reduced (to S'(i)) if for some j S'(j)
64 >= S(i), with S'(j) either being >= S(i) beforehand, or
65 updated atomically together with S(i).
67 Proof of invariant 1 for the secnet operations:
68 (a) check live vs proc, proc>live, mv:
69 j=2, i=1; S'(i)=-1, so S(i) is being reduced. S'(j) is
70 equal to S(i), and the rename is atomic [1], so S'(j) and
71 S'(i) are updated simultaneously. S(j) is being
72 increased. (There are no hazards from concurrent writers;
73 only we ourselves (secnet) write to live or proc.)
74 (b) check live vs proc, proc<=live, rm:
75 j=2, i=1; S'(i)=-1, so S(i) is being reduced. But
76 S(j) is >= $(i) throughout. (Again, no concurrent
78 (c) mv update proc (when proc does not exist):
79 j=1, i=0; S(i) is being reduced to -1. But simultaneously
80 S(j) is being increased to the old S(i). Our precondition
81 (proc not existing) is not subject to a concurrent writer
82 hazards because only we write to proc; our action is
83 atomic and takes whatever update is available (if any).
85 Proof of soundness for the mss reading operation:
86 Let M be MAX(\forall S) at the point where mss reads update.
87 Invariant 2: when mss reads S(k), MAX(K, S(k)..S(2)) >= M,
88 where K is the max S it has seen so far. Clearly this is
89 true for k=0 (with K==-1). secnet's operations never break
90 this invariant because if any S() is reduced, another one
91 counted must be increased. mss's step operation
92 updates K with S(k), so MAX(K', S(k+1)..)=MAX(K, S(k)..),
93 and updates k to k+1, preserving the invariant.
94 At the end we have k=3 and K=>M. Since secnet never
95 invents serials, K=M in the absence of an mss update
98 Consideration of the mss update operation:
99 Successive serials from sites file updates etc. are supposed
100 to be increasing. When this is true, M is increased. A
101 concurrent reading mss which makes its first read after the
102 update will get the new data (by the proofs above). This
103 seems to be the required property.
107 [1] From "Base Specifications issue 7",
108 2.9.7 Thread Interactions with Regular File Operations
109 All of the following functions shall be atomic with respect to
110 each other in the effects specified in POSIX.1-2017 when they
111 operate on regular files or symbolic links:
112 ... rename ... open ...