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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
peerkeys files
--------------
<F> live file, loaded on startup, updated by secnet
(only). * in-memory peerkeys_current is kept
synced with this file
<F>~update update file from config manager, checked before
every key exchange. config manager must rename
this file into place; it will be renamed and
then removed by secnet.
<F>~proc update file being processed by secnet.
only secnet may write or remove.
<F>~incoming update file from peer, being received by secnet
may be incomplete, unverified, or even malicious
only secnet may write or remove.
<F>~tmp update file from config manager, only mss may
write or rename
secnet discards updates that are not more recent than (by
serial) the live file. But it may not process updates
immediately.
The implied keyset to be used is MAX(live, proc, update).
secnet does:
check live vs proc, either mv proc live or rm proc
if proc doesn't exist, mv update proc
make-secnet-sites does:
write: rename something onto update
read: read update,proc,live in that order and take max
We support only one concurrent secnet, one concurrent
writing make-secnet-sites, and any number of readers.
We want to maintain a live file at all times as that
is what secnet actually reads at startup and uses.
Proof that this is sound:
Let us regard update,proc,live as i=0,1,2
Files contain public key sets and are manipulated as
a whole, and we may regard key sets with the same
serial as equivalent.
We talk below about reading as if it were atomic.
Actually the atomic operation is open(2); the
reading gets whatever that name refers to. So
we can model this as an atomic read.
secnet eventually moves all data into the live file
or deletes it, so there should be no indefinitely
stale data; informally this means we can disregard
the possibility of very old serials and regard
serials as fully ordered. (We don't bother with
a formal proof of this property.)
Consequently we will only think about the serial
and not the contents. We treat absent files as
minimal (we will write -1 for convenience although
we don't mean a numerical value). We write S(i).
Invariant 1 for secnet's transformations is as follows:
Each file S(i) is only reduced (to S'(i)) if for some j S'(j)
>= S(i), with S'(j) either being >= S(i) beforehand, or
updated atomically together with S(i).
Proof of invariant 1 for the secnet operations:
(a) check live vs proc, proc>live, mv:
j=2, i=1; S'(i)=-1, so S(i) is being reduced. S'(j) is
equal to S(i), and the rename is atomic [1], so S'(j) and
S'(i) are updated simultaneously. S(j) is being
increased. (There are no hazards from concurrent writers;
only we ourselves (secnet) write to live or proc.)
(b) check live vs proc, proc<=live, rm:
j=2, i=1; S'(i)=-1, so S(i) is being reduced. But
S(j) is >= $(i) throughout. (Again, no concurrent
writer hazards.)
(c) mv update proc (when proc does not exist):
j=1, i=0; S(i) is being reduced to -1. But simultaneously
S(j) is being increased to the old S(i). Our precondition
(proc not existing) is not subject to a concurrent writer
hazards because only we write to proc; our action is
atomic and takes whatever update is available (if any).
Proof of soundness for the mss reading operation:
Let M be MAX(\forall S) at the point where mss reads update.
Invariant 2: when mss reads S(k), MAX(K, S(k)..S(2)) >= M,
where K is the max S it has seen so far. Clearly this is
true for k=0 (with K==-1). secnet's operations never break
this invariant because if any S() is reduced, another one
counted must be increased. mss's step operation
updates K with S(k), so MAX(K', S(k+1)..)=MAX(K, S(k)..),
and updates k to k+1, preserving the invariant.
At the end we have k=3 and K=>M. Since secnet never
invents serials, K=M in the absence of an mss update
with a bigger S.
Consideration of the mss update operation:
Successive serials from sites file updates etc. are supposed
to be increasing. When this is true, M is increased. A
concurrent reading mss which makes its first read after the
update will get the new data (by the proofs above). This
seems to be the required property.
QED.
[1] From "Base Specifications issue 7",
2.9.7 Thread Interactions with Regular File Operations
All of the following functions shall be atomic with respect to
each other in the effects specified in POSIX.1-2017 when they
operate on regular files or symbolic links:
... rename ... open ...
--
This file is part of secnet.
See LICENCE and CREDITS for full list of copyright holders.
SPDX-License-Identifier: GPL-3.0-or-later
There is NO WARRANTY.
|
