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 <ijackson@chiark.greenend.org.uk>

diff --git a/site.c b/site.c
index 640ca68ba57ebb4ef4aa18ee0d4ee0939e142507..fda3dcc11c5bbc6d5d0de83ecfb8f7c9cf8b7463 100644 (file)
--- a/site.c
+++ b/site.c
@@ -945,6 +945,87 @@ static void peerkeys_check_for_update(struct site *st)
      *  <F>~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;