Merge pull request #228 from project-everest/adl_memory_model

Update memory model (see #227)

Author: ad-l

src/parsers/Parsers.rfc

@@ -1224,6 +1224,7 @@ struct {
 opaque SessionID<0..32>;
 
 enum /*@open*/ { nullCompression(0), (255) } CompressionMethod;
+enum { nullCompression(0), (255) } LegacyCompression;
 
 /** Shared Handshake Message Types **/
 
@@ -1232,18 +1233,62 @@ struct {
   Random random;
   SessionID session_id;
   CipherSuite cipher_suites<2..2^16-2>;
-  CompressionMethod compression_method<1..2^8-1>;
+  CompressionMethod compression_methods<1..2^8-1>;
   ClientHelloExtensions extensions;
 } ClientHello;
 
+struct {
+  SessionID session_id;
+  CipherSuite cipher_suite;
+  CompressionMethod compression_method;
+  ServerHelloExtensions extensions;
+} SHKind;
+
+struct {
+  SessionID session_id;
+  CipherSuite cipher_suite;
+  LegacyCompression legacy_compression;
+  HRRExtensions extensions;
+} HRRKind;
+
+/*
+We need to change the definition of the ServerHello
+type to account for the syntactic differences between
+ServerHello and HelloRetryRequest.
+
+In a HRR, the compression_method must be null and the
+format of some extensions is different (e.g. key_share
+is a KeyShareEntry in SH and a GroupName in HRR)
+*/
+struct {
+  ProtocolVersion version;
+  opaque random[32];
+  (if random = "CF21AD74E59A6111BE1D8C021E65B891C2A211167ABB8C5E079E09E2C8A8339C"
+    HRRKind
+  else
+    SHKind) is_hrr;
+} ServerHello;
+
+/*
+Using an if-then-else type is annoying, in the specification
+of the handshake we want to convert it to either SH or HRR.
+*/
 struct {
   ProtocolVersion version;
   Random random;
   SessionID session_id;
   CipherSuite cipher_suite;
   CompressionMethod compression_method;
   ServerHelloExtensions extensions;
-} ServerHello;
+} RealServerHello;
+
+struct {
+  ProtocolVersion version;
+  SessionID session_id;
+  CipherSuite cipher_suite;
+  LegacyCompression legacy_compression;
+  HRRExtensions extensions;
+} HelloRetryRequest;
 
 /** TLS 1.3 Handshake Messages */
 

src/tls/Crypto.CRF.fst

@@ -2,6 +2,7 @@ module Crypto.CRF
 
 module Concrete = EverCrypt.Hash.Incremental
 module Hash = EverCrypt.Hash
+module HD = Spec.Hash.Definitions
 
 module B = LowStar.Buffer
 module ST = FStar.HyperStack.ST
@@ -53,69 +54,59 @@ assume val of_seq
 /// ---------------------------
 
 /// This is very finely tuned to avoid inference issues.
-type mstate a = a': Concrete.alg { a' == a } & p:B.pointer bytes {
+type mstate a = a': alg { a' == a } & p:B.pointer bytes {
   B.(loc_disjoint (loc_addr_of_buffer p) (loc_region_only true Mem.tls_tables_region))
 }
 
 inline_for_extraction
-let state (a: Concrete.alg) =
+let state (a: alg) =
   if model then
     mstate a
   else
     Concrete.state a
 
-// UGH!!!
-noextract inline_for_extraction
-let fst (#a: e_alg) (s: state (G.reveal a){model}):
-  Tot (a': Concrete.alg { G.reveal a == a' })
-=
-  if model then
-    let (| a, s |) = (s <: mstate (G.reveal a)) in
-    a
-  else
-    false_elim ()
-
-noextract inline_for_extraction
-let snd (#a: e_alg) (s: state (G.reveal a){model}):
-  Tot (p:B.pointer bytes {
-    B.(loc_disjoint (loc_addr_of_buffer p) (loc_region_only true Mem.tls_tables_region))
-  })
-=
-  if model then
-    let (| a, s |) = (s <: mstate (G.reveal a)) in
-    s
-  else
-    false_elim ()
+noextract let ideal (#a:alg) (s:state a)
+  : Pure (mstate a) (requires model) (ensures fun _ -> True)
+  = s
+noextract let gideal (#a:e_alg) (s:state (G.reveal a))
+  : Pure (mstate (G.reveal a)) (requires model) (ensures fun _ -> True)
+  = s
+
+inline_for_extraction noextract let real (#a:alg) (s:state a)
+  : Pure (Concrete.state a) (requires not model) (ensures fun _ -> True)
+  = s
+inline_for_extraction noextract let greal (#a:e_alg) (s:state (G.reveal a))
+  : Pure (Concrete.state (G.reveal a)) (requires not model) (ensures fun _ -> True)
+  = s
 
 let freeable #a h (s:state a) =
   if model then
-    let s: B.pointer bytes = snd #(G.hide a) s in
+    let (| a, s |) = ideal s in
     B.freeable s
   else
-    Concrete.freeable #a h s
+    Concrete.freeable h (real s)
 
 let footprint #a h (s: state a) =
   if model then
-    B.loc_addr_of_buffer (snd #(G.hide a) s)
+    B.loc_addr_of_buffer (dsnd (ideal s))
   else
-    Concrete.footprint #a h s
+    Concrete.footprint h (real s)
 
 let invariant #a h (s: state a) =
   if model then
-    let s: B.pointer bytes = snd #(G.hide a) s in
+    let (| _, s |) = ideal s in
     B.live h s /\ S.length (B.deref h s) < pow2 61
   else
-    Concrete.invariant #a h s
+    Concrete.invariant h (real s)
 
 let invariant_loc_in_footprint #_ _ _ = ()
 
 let hashed #a h (s: state a) =
   if model then
-    let s: B.pointer bytes = snd #(G.hide a) s in
+    let (| _, s |) = ideal s in
     B.deref h s
   else
-    let s: Concrete.state a = s in
-    Concrete.hashed h s
+    Concrete.hashed h (real s)
 
 #push-options "--max_ifuel 1"
 let hash_fits #_ _ _ =
@@ -141,25 +132,23 @@ let create_in a r =
 let init a s =
   let open LowStar.BufferOps in
   if model then
-    let s: B.pointer bytes = snd s in
-    s *= S.empty
+    dsnd (gideal s) *= S.empty
   else
-    Concrete.init a s
+    Concrete.init a (greal s)
 
 let update a s data len =
   let open LowStar.BufferOps in
   if model then
-    let s: B.pointer bytes = snd s in
+    let (| _, s |) = gideal s in
     s *= (S.append !*s (to_seq data len))
   else
-    Concrete.update a s data len
+    Concrete.update a (greal s) data len
 
 #push-options "--z3rlimit 50"
 let finish a st dst =
   let open LowStar.BufferOps in
   if model then
-    let a = fst #a st in
-    let s: B.pointer bytes = snd st in
+    let (| a, s |) = gideal st in
     (**) assert B.(loc_disjoint (B.loc_addr_of_buffer s)
       (B.loc_region_only true Mem.tls_tables_region));
     (**) let h0 = ST.get () in
@@ -175,7 +164,6 @@ let finish a st dst =
 
 let free a s =
   if model then
-    B.free (snd s)
+    B.free (dsnd (gideal s))
   else
     Concrete.free a s
-

src/tls/Crypto.CRF.fsti

@@ -12,6 +12,7 @@ module Crypto.CRF
 
 module Concrete = EverCrypt.Hash.Incremental
 module Hash = EverCrypt.Hash
+module HD = Spec.Hash.Definitions
 
 module B = LowStar.Buffer
 module ST = FStar.HyperStack.ST
@@ -20,6 +21,7 @@ module S = FStar.Seq
 module U32 = FStar.UInt32
 module G = FStar.Ghost
 
+open Mem
 open FStar.HyperStack.ST
 
 inline_for_extraction
@@ -51,45 +53,45 @@ unfold noextract
 let bytes = Model.CRF.bytes
 
 unfold noextract
-let e_alg = Concrete.e_alg
+let alg = Concrete.alg
 
 unfold noextract
-let fresh_loc = Concrete.fresh_loc
+let e_alg = Concrete.e_alg
 
 /// Overriding things
 /// -----------------
 
 inline_for_extraction
-val state: Concrete.alg -> Type0
+val state: alg -> Type0
 
-val freeable: #a:Concrete.alg -> HS.mem -> state a -> Type0
+val freeable: #a:alg -> HS.mem -> state a -> Type0
 
 let preserves_freeable #a (s: state a) (h0 h1: HS.mem) =
   freeable h0 s ==> freeable h1 s
 
-val footprint: #a:Concrete.alg -> HS.mem -> state a -> GTot B.loc
+val footprint: #a:alg -> HS.mem -> state a -> GTot B.loc
 
-val invariant: #a:Concrete.alg -> HS.mem -> state a -> Type0
+val invariant: #a:alg -> HS.mem -> state a -> Type0
 
 val invariant_loc_in_footprint
-  (#a: Concrete.alg)
+  (#a: alg)
   (s: state a)
   (m: HS.mem)
 : Lemma
   (requires (invariant m s))
-  (ensures (Concrete.loc_in (footprint m s) m))
+  (ensures (loc_in (footprint m s) m))
   [SMTPat (invariant m s)]
 
-val hashed: #a:Concrete.alg -> HS.mem -> state a -> GTot bytes
+val hashed: #a:alg -> HS.mem -> state a -> GTot bytes
 
-val hash_fits (#a:Hash.alg) (h:HS.mem) (s:state a): Lemma
+val hash_fits (#a:alg) (h:HS.mem) (s:state a): Lemma
   (requires (
     invariant h s))
   (ensures (
-    S.length (hashed h s) < Spec.Hash.Definitions.max_input_length a))
+    S.length (hashed h s) < HD.max_input_length a))
   [ SMTPat (hashed h s) ]
 
-val frame_invariant (#a: Concrete.alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
+val frame_invariant (#a: alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
   (requires (
     invariant h0 s /\
     B.loc_disjoint l (footprint h0 s) /\
@@ -99,15 +101,15 @@ val frame_invariant (#a: Concrete.alg) (l: B.loc) (s: state a) (h0 h1: HS.mem):
     footprint h0 s == footprint h1 s))
   [ SMTPat (invariant h1 s); SMTPat (B.modifies l h0 h1) ]
 
-val frame_hashed (#a: Concrete.alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
+val frame_hashed (#a: alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
   (requires (
     invariant h0 s /\
     B.loc_disjoint l (footprint h0 s) /\
     B.modifies l h0 h1))
   (ensures (hashed h0 s == hashed h1 s))
   [ SMTPat (hashed h1 s); SMTPat (B.modifies l h0 h1) ]
 
-val frame_freeable (#a: Concrete.alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
+val frame_freeable (#a: alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): Lemma
   (requires (
     invariant h0 s /\
     freeable h0 s /\
@@ -121,7 +123,7 @@ val frame_freeable (#a: Concrete.alg) (l: B.loc) (s: state a) (h0 h1: HS.mem): L
 
 (** @type: true
 *)
-val create_in (a: Hash.alg) (r: HS.rid): ST (state a)
+val create_in (a: alg) (r: HS.rid): ST (state a)
   (requires (fun _ ->
     // NEW! ↓
     B.(loc_disjoint (loc_region_only true r) (loc_region_only true Mem.tls_tables_region)) /\