NOTES.peer-keys

   1 peerkeys files
   2 --------------
   3
   4  <F>            live file, loaded on startup, updated by secnet
   5                  (only).  * in-memory peerkeys_current is kept
   6                  synced with this file
   7
   8  <F>~update     update file from config manager, checked before
   9                  every key exchange.  config manager must rename
  10                  this file into place; it will be renamed and
  11                  then removed by secnet.
  12
  13  <F>~proc       update file being processed by secnet.
  14                  only secnet may write or remove.
  15
  16  <F>~incoming   update file from peer, being received by secnet
  17                  may be incomplete, unverified, or even malicious
  18                  only secnet may write or remove.
  19
  20  <F>~tmp        update file from config manager, only mss may
  21                  write or rename
  22
  23 secnet discards updates that are not more recent than (by
  24 serial) the live file.  But it may not process updates
  25 immediately.
  26
  27 The implied keyset to be used is MAX(live, proc, update).
  28
  29 secnet does:
  30  check live vs proc, either mv proc live or rm proc
  31  if proc doesn't exist, mv update proc
  32
  33 make-secnet-sites does:
  34  write: rename something onto update
  35  read: read update,proc,live in that order and take max
  36
  37 We support only one concurrent secnet, one concurrent
  38 writing make-secnet-sites, and any number of readers.
  39 We want to maintain a live file at all times as that
  40 is what secnet actually reads at startup and uses.
  41
  42 Proof that this is sound:
  43   Let us regard update,proc,live as i=0,1,2
  44   Files contain public key sets and are manipulated as
  45    a whole, and we may regard key sets with the same
  46    serial as equivalent.
  47   We talk below about reading as if it were atomic.
  48    Actually the atomic operation is open(2); the
  49    reading gets whatever that name refers to.  So
  50    we can model this as an atomic read.
  51   secnet eventually moves all data into the live file
  52    or deletes it, so there should be no indefinitely
  53    stale data; informally this means we can disregard
  54    the possibility of very old serials and regard
  55    serials as fully ordered.  (We don't bother with
  56    a formal proof of this property.)
  57   Consequently we will only think about the serial
  58    and not the contents.  We treat absent files as
  59    minimal (we will write -1 for convenience although
  60    we don't mean a numerical value).  We write S(i).
  61
  62 Invariant 1 for secnet's transformations is as follows:
  63   Each file S(i) is only reduced (to S'(i)) if for some j S'(j)
  64   >= S(i), with S'(j) either being >= S(i) beforehand, or
  65   updated atomically together with S(i).
  66
  67 Proof of invariant 1 for the secnet operations:
  68   (a) check live vs proc, proc>live, mv:
  69      j=2, i=1; S'(i)=-1, so S(i) is being reduced.  S'(j) is
  70      equal to S(i), and the rename is atomic [1], so S'(j) and
  71      S'(i) are updated simultaneously.  S(j) is being
  72      increased.  (There are no hazards from concurrent writers;
  73      only we ourselves (secnet) write to live or proc.)
  74   (b) check live vs proc, proc<=live, rm:
  75      j=2, i=1; S'(i)=-1, so S(i) is being reduced.  But
  76      S(j) is >= $(i) throughout.  (Again, no concurrent
  77      writer hazards.)
  78   (c) mv update proc (when proc does not exist):
  79      j=1, i=0; S(i) is being reduced to -1.  But simultaneously
  80      S(j) is being increased to the old S(i).  Our precondition
  81      (proc not existing) is not subject to a concurrent writer
  82      hazards because only we write to proc; our action is
  83      atomic and takes whatever update is available (if any).
  84
  85 Proof of soundness for the mss reading operation:
  86   Let M be MAX(\forall S) at the point where mss reads update.
  87   Invariant 2: when mss reads S(k), MAX(K, S(k)..S(2)) >= M,
  88   where K is the max S it has seen so far.  Clearly this is
  89   true for k=0 (with K==-1).  secnet's operations never break
  90   this invariant because if any S() is reduced, another one
  91   counted must be increased.  mss's step operation
  92   updates K with S(k), so MAX(K', S(k+1)..)=MAX(K, S(k)..),
  93   and updates k to k+1, preserving the invariant.
  94   At the end we have k=3 and K=>M.  Since secnet never
  95   invents serials, K=M in the absence of an mss update
  96   with a bigger S.
  97
  98 Consideration of the mss update operation:
  99   Successive serials from sites file updates etc. are supposed
 100   to be increasing.  When this is true, M is increased.  A
 101   concurrent reading mss which makes its first read after the
 102   update will get the new data (by the proofs above).  This
 103   seems to be the required property.
 104
 105 QED.
 106
 107 [1] From "Base Specifications issue 7",
 108  2.9.7 Thread Interactions with Regular File Operations
 109  All of the following functions shall be atomic with respect to
 110  each other in the effects specified in POSIX.1-2017 when they
 111  operate on regular files or symbolic links:
 112   ... rename ... open ...