chiark / gitweb /
docs: Move peer-keys documentation into a README file
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 2 Dec 2019 13:14:09 +0000 (13:14 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sat, 15 Feb 2020 21:56:51 +0000 (21:56 +0000)
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 <ijackson@chiark.greenend.org.uk>
NOTES.peer-keys [new file with mode: 0644]
README
site.c

diff --git a/NOTES.peer-keys b/NOTES.peer-keys
new file mode 100644 (file)
index 0000000..2c58213
--- /dev/null
@@ -0,0 +1,112 @@
+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 ...
diff --git a/README b/README
index 8c7e214..1d29c55 100644 (file)
--- 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 (file)
--- 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
-     *
-     *  <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");