X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=blobdiff_plain;f=site.c;fp=site.c;h=ea85e0e223441ad754e75f311121a269066c9626;hb=cc20e08d7e3f3678fa844e1622fd8dfeaa770f1c;hp=e8b507ff0540fc2302420f0eccbb959897e22072;hpb=0513b753eb9005a69b8fc737be981c1a5624edf2;p=secnet.git 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");