From a8cbefc5f93521d25bb0ba36fe14d96889ed0007 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Thu, 28 Nov 2019 13:26:03 +0000 Subject: [PATCH] site: Write an argument for the soundness of key file update This argument is not yet in its final form. There are two further commits which come along in a moment. Signed-off-by: Ian Jackson --- site.c | 81 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) diff --git a/site.c b/site.c index 640ca68..fda3dcc 100644 --- a/site.c +++ b/site.c @@ -945,6 +945,87 @@ static void peerkeys_check_for_update(struct site *st) * ~incoming update file from peer, being received by secnet * may be incomplete, unverified, or even malicious * only secnet may write or remove. + * + * 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 + * + * 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. + * (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. + * (c) mv update proc (when update 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). + * + * 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; -- 2.30.2