Verification infrastructure for table of connections

[s-zanella]

Requirements

We need to maintain a table of connections, mapping a unique connection ID to the connection state.
Each connection evolves monotonically according to the reflexive transitive closure of a step relation encoding the TLS state machine.

• We need to prove and maintain correspondence assertions between connections in the table. These typically have the form

forall (c:connection). p c ==> exists (c'.connection). q c c'

For instance: if there is a server connection in the table that has received a ClientHello with a cookie extension then there must have been an earlier connection where a HelloRetryRequest was sent, and the cookie must match the original ClientHello message.

• We would like to avoid as much as possible stateful invariants on the connection table, and rely instead on monotonicity, so as not to have to prove and apply framing lemmas, etc.

• We want to extract invididual connections to e.g. a single C struct. Whatever representation we chose for the table of connections the table itself and any additional ideal state must be erased at extraction.

• We want to be able to free memory allocated for storing the state of a connection. E.g. after sending a HelloRetryRequest a server may close the connection and free any allocated memory. This means that any non-ideal state in the table of connections must be manually managed and freeable.

• We want the infrastructure to verifiably support stateless retry using Crypto.{AE,AEAD} for cookie encryption. For this, we should be able to attach a predicate to plaintext cookies that witnesses stable properties of the connection table: e.g. an authenticated encrypted cookie must match a ClientHello received in a previous connection that ended with a HelloRetryRequest message.

We explored 3 alternative representations for the table of connections.

[s-zanella]

First approach

The first alternative depends on a generalization of FStar.Monotonic.DependentMap, allowing entries to evolve according to a dependent preorder rel. The preorder of the table itself is defined as

let grows (#a:eqtype) (#b:a -> Type) 
  (#inv:(partial_dependent_map a b -> Type))
  (rel: (x:a) -> Preorder.preorder (b x)) : Preorder.preorder (imap a b inv) =
  fun (m1:imap a b inv) (m2:imap a b inv) ->
    forall x.{:pattern (Some? (sel m1 x))}
      Some? (sel m1 x) ==>
      (Some? (sel m2 x) /\ rel x (Some?.v (sel m1 x)) (Some?.v (sel m2 x)))

That is, the table can be extended, or entries can be updated according to rel. FStar.Monotonic.DependentMap is a special case where rel k x y == (x == y).

We keep a monotonic dependent table mapping connection IDs to values of an inductive type encoding the state of the connection. We insantiate inv above as the trivial invariant fun _ -> True.

type connection_table (r:erid) = 
  T.t r connection_id (fun id -> connection) (fun _ -> True) (closure step)

This allows for an API for extending and updating the table, as well as witnessing correspondence assertions. The properties we witness must be stable with respect to grows rel; we can prove this using lemmas in FStar.Montonic.ReflexiveTransitiveClosure.

Two main drawbacks of this alternative:
a. it requires correspondence assertions to be stable;
b. entries in the table are values and so must be erased. This requires storing the same value in separate concrete state and maintaing the equivalence of both values as an stateful invariant

[s-zanella]

Second approach

The second alternative uses a table mapping connection IDs to monotonic references to values of the same inductive type of connection states as before. We use the table invariant to keep correspondence assertions, expressed in terms of witnesses (i.e. token_p):

val inv: partial_dependent_map connection_id (c:mreference connection rel{recallable c}) -> Type0
let inv m =
  forall (id:connection_id{Some? (DM.sel m id)}) (r:nat) (ck:cookie).
   let c = Some?.v (DM.sel m id) in
   token_p c (fun h -> 
     is_retry (sel h c) /\ cookie_of (sel h c) == ck /\ nonce_of (sel h c) == r)
   ==>
   (exists (id':connection_id{Some? (DM.sel m id')}).
     let c' = Some?.v (DM.sel m id') in
     token_p c' (fun h -> 
       Sent_HRR? (sel h c') /\ 
       nonce_of (sel h c') == r /\
       ck `matches` Sent_HRR?.ch (sel h c')))

type connection_table (r:erid) = 
  T.t r connection_id (fun _ -> c:mreference connection rel{recallable c}) 
    inv (fun _ _ _ -> True)

Here the challenge is to manipulate token_p witnesses. We could do this only with the addition of an axiom that does not seem provable in the current memory model (thanks @aseemr). We used this axiom to reason about occurences of token_p on the left-hand-side of the implication in inv

val token_not: 
    #a:Type
  -> #rel:Preorder.preorder a
  -> r:mreference a rel{recallable r}
  -> p:mem_predicate
  -> ST unit
    (requires fun h -> token_p r (fun h -> ~(p h)))
    (ensures  fun h0 _ h1 -> h0 == h1 /\ ~(token_p r p))

Two main drawbacks of this alternative:
a. it requires the above axiom;
b. it requires references in entries to be recallable and thus not freeable;

[s-zanella]

Third approach

The third alternative uses a table mapping connection IDs to monotonic references storing the connection state. In contrast to the previous representation the references are manually managed and freeable.

let connection_ref (id:connection_id) = r:mmmref connection rel{frameOf r `extends` rgn}

let minv (m:partial_dependent_map connection_id connection_ref) =
  forall id1 id2.{:pattern (Some? (DM.sel m id1)); (Some? (DM.sel m id2))}
    (id1 <> id2 /\ Some? (DM.sel m id1) /\ Some? (DM.sel m id2)) ==>
    frameOf (Some?.v (DM.sel m id1)) `disjoint` frameOf (Some?.v (DM.sel m id2))

type connection_table = T.t rgn connection_id connection_ref minv

We keep correspondence assertions in a separate stateful invariant, with a stateful left-hand-side and a stable right-hand-side expressed in terms of token_p:

let connection_inv m c =
  match c with
  | Sent_ServerHello ch id1 | Complete ch id1 ->
    if has_cookie ch then
      match T.sel m id1 with
      | Some c' ->
        token_p c' (fun h0 -> 
          Sent_HRR? (sel h0 c') /\
          ch_of_cookie ch == Sent_HRR?.ch (sel h0 c'))
      | _ -> False
    else True
  | _ -> True

val inv: t:connection_table -> h:mem -> Type0
let inv t h = 
  h `contains` t /\
  (let m = sel h t in
  forall (id:connection_id).{:pattern (T.defined t id h)}
    (T.defined t id h /\ h `contains` (T.value_of t id h))
    ==> connection_inv m (sel h (Some?.v (T.sel m id))))

This is more flexible than the previous approach because it does not require the negation of the left-hand-side to be stable, which is required to establish the invariant. This problem shows when adding an Init initial connection state, which may or may not transition to a connection retry. One can therefore not prove the token_p assertion on the left-hand-side or its negation, and must prove that the right-hand-side holds, but it might not.

This mix of stateful and monotonic assertions in the table invariant means that the end event of a correspondence assertion might become unprovable when a connection is freed, while the begin event will continue to hold by monotonicity. This is enough because we typically need to invoke the correspondence assertion for live connections, and all bets are off once the connection is freed.

[s-zanella]

By allocating a global connection table we can support stateless server retry with cookies encrypted using Crypto.{AEAD,AE}. We attach the following predicate to plaintext cookies (depending on table):

let phi s = 
  Seq.length s >= 32 /\
  (if model then
    let random = Seq.slice s 0 32 in
    let id = id_of_random random in
    let t:_connection_table = table in
    token_p t (fun h -> 
      T.defined t id h /\
      (let c = T.value_of t id h in
      token_p c (fun h' -> 
        Sent_HRR? (sel h' c) /\
        CH1 random == Sent_HRR?.ch (sel h' c))))
   else True)

Upon successful decryption of a cookie appearing in a ClientHello message, a server can recover the initial ClientHello and HelloRetryRequest messages and any additional state and resume the handshake.

See this test for a working example of this. The only complication in the proof is threading the connection table invariant inv through stateful computations outside of the ConnectionTable API. We provide an appropriate framing lemma to frame the invariant from computations modifying locations outside the table's own region:

val framing: h0:mem -> t:_connection_table -> l:B.loc -> h1:mem -> Lemma
  (requires B.modifies l h0 h1 /\ 
            B.loc_disjoint l (B.loc_all_regions_from true rgn) /\
            h0 `contains` t /\
            (forall a rel (r:mreference a rel). 
              frameOf r `extends` table_rgn ==> 
              h1 `contains` r ==> h0 `contains` r) /\
            inv t h0)
  (ensures  inv t h1)

Adding a pattern to this lemma would suffice to automate framing. However, while developing the experiment, which uses LowStar.Buffer.mmalloc to allocate buffers for encrypting cookies, we realized that the current specification of allocations in LowStar.Monotonic.Buffer.alloc_post_mem_common is insufficient because it allows e.g. an implementation of mmalloc to allocate more references than the one requested, which makes impossible to prove

    (forall a rel (r:mreference a rel). 
              frameOf r `extends` table_rgn ==> 
              h1 `contains` r ==> h0 `contains` r) 

After discussing this issue, we agreed that a solution would be to add a new conjunct in alloc_post_mem_common with an abstract predicate, and a corresponding elimination lemma that says that no new references have been allocated in other regions.