--- /dev/null
+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 ...
static void peerkeys_check_for_update(struct site *st)
{
- /* 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 ...
- */
if (!st->peerkeys_path) return;
pathprefix_template_setsuffix(&st->peerkeys_tmpl,"~proc");
~ian / secnet.git / commitdiff