From cc20e08d7e3f3678fa844e1622fd8dfeaa770f1c Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Mon, 2 Dec 2019 13:14:09 +0000 Subject: [PATCH] docs: Move peer-keys documentation into a README file This is externally visible and should be in documentation. For now we put it in NOTES.peer-keys. At some point the secnet docs really need to be (re)organised... Signed-off-by: Ian Jackson --- NOTES.peer-keys | 112 ++++++++++++++++++++++++++++++++++++++++++++++++ README | 2 +- site.c | 112 ------------------------------------------------ 3 files changed, 113 insertions(+), 113 deletions(-) create mode 100644 NOTES.peer-keys diff --git a/NOTES.peer-keys b/NOTES.peer-keys new file mode 100644 index 0000000..2c58213 --- /dev/null +++ b/NOTES.peer-keys @@ -0,0 +1,112 @@ +peerkeys files +-------------- + + live file, loaded on startup, updated by secnet + (only). * in-memory peerkeys_current is kept + synced with this file + + ~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. + + ~proc update file being processed by secnet. + only secnet may write or remove. + + ~incoming update file from peer, being received by secnet + may be incomplete, unverified, or even malicious + only secnet may write or remove. + + ~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 ... diff --git a/README b/README index 8c7e214..1d29c55 100644 --- a/README +++ b/README @@ -399,7 +399,7 @@ site: dict argument port (integer): mandatory if 'address' is specified: the port used to contact our peer peer-keys (string): path (prefix) for peer public key set file(s); - see README.make-secnet-sites re `pub' etc. + see README.make-secnet-sites re `pub' etc. and NOTES.peer-keys. key (sigpubkey closure): our peer's public key (obsolete) transform (transform closure): how to mangle packets sent between sites dh (dh closure) diff --git a/site.c b/site.c index e8b507f..ea85e0e 100644 --- a/site.c +++ b/site.c @@ -929,118 +929,6 @@ static void peerkeys_maybe_incorporate(struct site *st, const char *file, static void peerkeys_check_for_update(struct site *st) { - /* peerkeys files - * - * live file, loaded on startup, updated by secnet - * (only). * in-memory peerkeys_current is kept - * synced with this file - * - * ~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. - * - * ~proc update file being processed by secnet. - * only secnet may write or remove. - * - * ~incoming update file from peer, being received by secnet - * may be incomplete, unverified, or even malicious - * only secnet may write or remove. - * - * ~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"); -- 2.30.2