Skip to content
This repository has been archived by the owner on Jun 17, 2024. It is now read-only.

Commit

Permalink
migrating to trimmed down MR interface
Browse files Browse the repository at this point in the history
  • Loading branch information
@aseemr
aseemr committed Dec 28, 2017
1 parent 37547c9 commit be1b889
Show file tree
Hide file tree
Showing 5 changed files with 62 additions and 62 deletions.
9 changes: 5 additions & 4 deletions src/tls/AEADOpenssl.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ open TLSInfo

module MM = FStar.Monotonic.Map
module MR = FStar.Monotonic.RRef
module HS = FStar.HyperStack

type id = i:id{~(PlaintextID? i) /\ AEAD? (aeAlg_of_id i)}
let alg (i:id) = AEAD?._0 (aeAlg_of_id i)
Expand Down Expand Up @@ -67,8 +68,8 @@ noeq type state (i:id) (rw:rw) =

type empty_log (#i:id) (#rw:rw) (st:state i rw) h =
authId i ==>
(MR.m_contains (ilog st.log) h /\
MR.m_sel h (ilog st.log) == MM.empty_map (iv i) entry)
(HS.contains h (ilog st.log) /\
HS.sel h (ilog st.log) == MM.empty_map (iv i) entry)

type writer i = s:state i Writer
type reader i = s:state i Reader
Expand Down Expand Up @@ -150,7 +151,7 @@ let encrypt #i #l e iv ad p =
if authId i then
begin
let log = ilog e.log in
MR.m_recall log;
recall log;
let c = CoreCrypto.random (cipherlen i l) in
MM.extend log iv (Entry ad p c);
c
Expand Down Expand Up @@ -181,7 +182,7 @@ let decrypt #i #l d iv ad c =
if authId i then
begin
let log = ilog d.log in
MR.m_recall log;
recall log;
match MM.lookup log iv with
| None -> assume false; None
| Some (Entry ad' p c') ->
Expand Down
19 changes: 9 additions & 10 deletions src/tls/Nonce.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,17 +49,17 @@ let nonce_rid_table : MM.t tls_tables_region random n_rid injective =
MM.alloc #tls_tables_region #random #n_rid #injective

//A nonce n is fresh in h if the nonce_rid_table doesn't contain it
let fresh (n:random) (h:HS.mem) = MM.sel (MR.m_sel h nonce_rid_table) n = None
let fresh (n:random) (h:HS.mem) = MM.sel (HS.sel h nonce_rid_table) n = None

//A region is fresh if no nonce is associated with it
let fresh_region (r:ex_rid) (h:HS.mem) =
forall n. Some r <> MM.sel (MR.m_sel h nonce_rid_table) n
forall n. Some r <> MM.sel (HS.sel h nonce_rid_table) n

//A nonce n is registered to region r, if the table contains n -> Some r;
//This mapping is stable (that's what the MR.witnessed means)
let registered (n:random) (r:MR.rid) =
MR.witnessed (MR.rid_exists r) /\
MR.witnessed (MM.contains nonce_rid_table n r)
witnessed (MR.rid_exists r) /\
witnessed (MM.contains nonce_rid_table n r)

let testify (n:random) (r:MR.rid)
: ST unit (requires (fun h -> registered n r))
Expand All @@ -79,14 +79,13 @@ abstract let role_nonce (cs:role) (n:random) (r:ex_rid) = registered n r
val mkHelloRandom: cs:role -> r:ex_rid -> ST random
(requires (fun h -> fresh_region r h))
(ensures (fun h0 n h1 ->
let nonce_rid_table_as_hsref = MR.as_hsref nonce_rid_table in
HS.modifies (Set.singleton tls_tables_region) h0 h1 /\ //modifies at most the tables region
HS.modifies_ref tls_tables_region (Set.singleton (HS.as_addr nonce_rid_table_as_hsref)) h0 h1 /\ //and within it, at most the nonce_rid_table
HS.modifies_ref tls_tables_region (Set.singleton (HS.as_addr nonce_rid_table)) h0 h1 /\ //and within it, at most the nonce_rid_table
(ideal ==> fresh n h0 /\ //if we're ideal then the nonce is fresh
registered n r /\ //the nonce n is associated with r
role_nonce cs n r))) //and the triple are associated as well, for ever more
let rec mkHelloRandom cs r =
MR.m_recall nonce_rid_table;
recall nonce_rid_table;
let n : random = timestamp() @| CoreCrypto.random 28 in
if ideal then
match MM.lookup nonce_rid_table n with
Expand All @@ -106,7 +105,7 @@ let lookup role n = MM.lookup nonce_rid_table n
(* Would be nice to make this a local let in new_region.
Except, implicit argument inference for testify_forall fails *)
private let nonce_rids_exists (m:MM.map' random n_rid) =
forall (n:random{Some? (MM.sel m n)}). MR.witnessed (MR.rid_exists (Some?.v (MM.sel m n)))
forall (n:random{Some? (MM.sel m n)}). witnessed (MR.rid_exists (Some?.v (MM.sel m n)))

(*
A convenient wrapper around FStar.ST.new_region,
Expand All @@ -123,8 +122,8 @@ val new_region: parent:MR.rid -> ST ex_rid
HS.fresh_region r h0 h1 /\ //it's fresh with respect to the current heap
fresh_region r h1)) //and it's not in the nonce table
let new_region parent =
MR.m_recall nonce_rid_table;
let m0 = MR.m_read nonce_rid_table in
recall nonce_rid_table;
let m0 = !nonce_rid_table in
let tok : squash (nonce_rids_exists m0) = () in
MR.testify_forall tok;
MR.ex_rid_of_rid (new_region parent)
Expand Down
26 changes: 13 additions & 13 deletions src/tls/PSK.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,10 @@ private let app_psk_table : MM.t psk_region psk_identifier app_psk_entry psk_tab
MM.alloc #psk_region #psk_identifier #app_psk_entry #psk_table_invariant

abstract type registered_psk (i:psk_identifier) =
MR.witnessed (MM.defined app_psk_table i)
witnessed (MM.defined app_psk_table i)

let valid_app_psk (ctx:pskInfo) (i:psk_identifier) (h:mem) =
match MM.sel (MR.m_sel h app_psk_table) i with
match MM.sel (sel h app_psk_table) i with
| Some (_, c, _) -> b2t (c = ctx)
| _ -> False

Expand All @@ -77,7 +77,7 @@ let psk_value (i:pskid) : ST (app_psk i)
(requires (fun h0 -> True))
(ensures (fun h0 _ h1 -> modifies_none h0 h1))
=
MR.m_recall app_psk_table;
recall app_psk_table;
MR.testify (MM.defined app_psk_table i);
match MM.lookup app_psk_table i with
| Some (psk, _, _) -> psk
Expand All @@ -86,7 +86,7 @@ let psk_info (i:pskid) : ST (pskInfo)
(requires (fun h0 -> True))
(ensures (fun h0 _ h1 -> modifies_none h0 h1))
=
MR.m_recall app_psk_table;
recall app_psk_table;
MR.testify (MM.defined app_psk_table i);
match MM.lookup app_psk_table i with
| Some (_, ctx, _) -> ctx
Expand All @@ -97,7 +97,7 @@ let psk_lookup (i:psk_identifier) : ST (option pskInfo)
modifies_none h0 h1
/\ (Some? r ==> registered_psk i)))
=
MR.m_recall app_psk_table;
recall app_psk_table;
match MM.lookup app_psk_table i with
| Some (_, ctx, _) ->
assume(MR.stable_on_t app_psk_table (MM.defined app_psk_table i));
Expand All @@ -109,7 +109,7 @@ type honest_st (i:pskid) (h:mem) =
(MM.defined app_psk_table i h /\
(let (_,_,b) = MM.value app_psk_table i h in b = true))

type honest_psk (i:pskid) = MR.witnessed (honest_st i)
type honest_psk (i:pskid) = witnessed (honest_st i)

// Generates a fresh PSK identity
val fresh_psk_id: unit -> ST psk_identifier
Expand All @@ -133,14 +133,14 @@ let gen_psk (i:psk_identifier) (ctx:pskInfo)
registered_psk i /\
honest_psk i))
=
MR.m_recall app_psk_table;
recall app_psk_table;
let psk = (abyte 1z) @| CoreCrypto.random 32 in
assume(index psk 0 = 1z);
let add : app_psk_entry i = (psk, ctx, true) in
MM.extend app_psk_table i add;
MM.contains_stable app_psk_table i add;
let h = get () in
cut(MM.sel (MR.m_sel h app_psk_table) i == Some add);
cut(MM.sel (sel h app_psk_table) i == Some add);
assume(MR.stable_on_t app_psk_table (honest_st i));
MR.witness app_psk_table (honest_st i)

Expand All @@ -152,12 +152,12 @@ let coerce_psk (i:psk_identifier) (ctx:pskInfo) (k:app_psk i)
registered_psk i /\
~(honest_psk i)))
=
MR.m_recall app_psk_table;
recall app_psk_table;
let add : app_psk_entry i = (k, ctx, false) in
MM.extend app_psk_table i add;
MM.contains_stable app_psk_table i add;
let h = get () in
cut(MM.sel (MR.m_sel h app_psk_table) i == Some add);
cut(MM.sel (sel h app_psk_table) i == Some add);
admit()

abstract let compatible_hash_ae_st (i:pskid) (ha:hash_alg) (ae:aeadAlg) (h:mem) =
Expand All @@ -166,21 +166,21 @@ abstract let compatible_hash_ae_st (i:pskid) (ha:hash_alg) (ae:aeadAlg) (h:mem)
ha = pskInfo_hash ctx /\ ae = pskInfo_ae ctx))

let compatible_hash_ae (i:pskid) (h:hash_alg) (a:aeadAlg) =
MR.witnessed (compatible_hash_ae_st i h a)
witnessed (compatible_hash_ae_st i h a)

abstract let compatible_info_st (i:pskid) (c:pskInfo) (h:mem) =
(MM.defined app_psk_table i h /\
(let (_,ctx,_) = MM.value app_psk_table i h in c = ctx))

let compatible_info (i:pskid) (c:pskInfo) =
MR.witnessed (compatible_info_st i c)
witnessed (compatible_info_st i c)

let verify_hash_ae (i:pskid) (ha:hash_alg) (ae:aeadAlg) : ST bool
(requires (fun h0 -> True))
(ensures (fun h0 b h1 ->
b ==> compatible_hash_ae i ha ae))
=
MR.m_recall app_psk_table;
recall app_psk_table;
MR.testify (MM.defined app_psk_table i);
match MM.lookup app_psk_table i with
| Some x ->
Expand Down
64 changes: 32 additions & 32 deletions src/tls/StreamAE.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,10 +105,10 @@ let genPost (#i:id) parent h0 (w:writer i) h1 =
fresh_region (AEAD.region w.aead) h0 h1 /\
color (AEAD.region w.aead) = color parent /\
(authId i ==>
(m_contains (ilog w.log) h1 /\
m_sel h1 (ilog w.log) == createEmpty)) /\
m_contains (ctr w.counter) h1 /\
m_sel h1 (ctr w.counter) === 0
(HS.contains h1 (ilog w.log) /\
HS.sel h1 (ilog w.log) == createEmpty)) /\
HS.contains h1 (ctr w.counter) /\
HS.sel h1 (ctr w.counter) === 0
//16-04-30 how to share the whole ST ... instead of genPost?

// Generate a fresh instance with index i in a fresh sub-region of r0
Expand All @@ -129,7 +129,7 @@ let gen parent i =
let ectr: ideal_ctr #writer_r writer_r i log = new_seqn #writer_r #(entry i) #max_ctr writer_r 0 log in
State #i #Writer #writer_r #writer_r aead log ectr
else
let ectr: concrete_ctr writer_r i = m_alloc writer_r 0 in
let ectr: concrete_ctr writer_r i = ralloc writer_r 0 in
State #i #Writer #writer_r #writer_r aead () ectr

#reset-options
Expand All @@ -143,8 +143,8 @@ val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
color r.region = color parent /\
fresh_region r.region h0 h1 /\
w.log == r.log /\
m_contains (ctr r.counter) h1 /\
m_sel h1 (ctr r.counter) === 0))
HS.contains h1 (ctr r.counter) /\
HS.sel h1 (ctr r.counter) === 0))
// encryption (on concrete bytes), returns (cipher @| tag)
// Keeps seqn and nonce implicit; requires the counter not to overflow
// encryption of plaintexts; safe instances are idealized
Expand All @@ -160,7 +160,7 @@ let genReader parent #i w =
let log : ideal_log w.region i = w.log in
let dctr: ideal_ctr reader_r i log = new_seqn reader_r 0 log in
State #i #Reader #reader_r #writer_r raead w.log dctr
else let dctr : concrete_ctr reader_r i = m_alloc reader_r 0 in
else let dctr : concrete_ctr reader_r i = ralloc reader_r 0 in
State #i #Reader #reader_r #writer_r raead () dctr

// Coerce a writer with index i in a fresh subregion of parent
Expand All @@ -172,7 +172,7 @@ val coerce: parent:rgn -> i:id{~(authId i)} -> kv:key i -> iv:iv i -> ST (writer
let coerce parent i kv iv =
assume false; // coerce missing post-condition
let writer_r = new_region parent in
let ectr: concrete_ctr writer_r i = m_alloc writer_r 0 in
let ectr: concrete_ctr writer_r i = ralloc writer_r 0 in
let aead = AEAD.coerce i parent kv iv in
State #i #Writer #writer_r #writer_r aead () ectr

Expand All @@ -196,19 +196,19 @@ val encrypt: #i:id -> e:writer i -> l:plainLen -> p:plain i l -> ST (cipher i l)
lemma_ID13 i;
HS.disjoint e.region (AEAD.log_region #i e.aead) /\
l <= max_TLSPlaintext_fragment_length /\ // FIXME ADL: why is plainLen <= max_TLSCiphertext_fragment_length_13 ?? Fix StreamPlain!
m_sel h0 (ctr e.counter) < max_ctr))
HS.sel h0 (ctr e.counter) < max_ctr))
(ensures (fun h0 c h1 ->
lemma_ID13 i;
modifies (Set.as_set [e.log_region; AEAD.log_region #i e.aead]) h0 h1 /\
m_contains (ctr e.counter) h1 /\
m_sel h1 (ctr e.counter) === m_sel h0 (ctr e.counter) + 1 /\
HS.contains h1 (ctr e.counter) /\
HS.sel h1 (ctr e.counter) === HS.sel h0 (ctr e.counter) + 1 /\
(authId i ==>
(let log = ilog e.log in
let ent = Entry l c p in
let n = Seq.length (m_sel h0 log) in
m_contains log h1 /\
Monotonic.RRef.witnessed (at_least n ent log) /\
m_sel h1 log == snoc (m_sel h0 log) ent))))
let n = Seq.length (HS.sel h0 log) in
HS.contains h1 log /\
witnessed (at_least n ent log) /\
HS.sel h1 log == snoc (HS.sel h0 log) ent))))

(* we primarily model the ideal functionality, the concrete code that actually
runs on the network is what remains after dead code elimination when
Expand All @@ -218,9 +218,9 @@ val encrypt: #i:id -> e:writer i -> l:plainLen -> p:plain i l -> ST (cipher i l)
let encrypt #i e l p =
let h0 = get() in
let ctr = ctr e.counter in
m_recall ctr;
recall ctr;
let text = if safeId i then createBytes l 0z else repr i l p in
let n = m_read ctr in
let n = !ctr in
lemma_repr_bytes_values n;
let nb = bytes_of_int (AEAD.noncelen i) n in
let iv = AEAD.create_nonce e.aead nb in
Expand All @@ -231,16 +231,16 @@ let encrypt #i e l p =
if authId i then
begin
let ilog = ilog e.log in
m_recall ilog;
recall ilog;
let ictr: ideal_ctr e.region i ilog = e.counter in
testify_seqn ictr;
write_at_end ilog (Entry l c p); //need to extend the log first, before incrementing the counter for monotonicity; do this only if ideal
m_recall ictr;
recall ictr;
increment_seqn ictr;
m_recall ictr
recall ictr
end
else
m_write ctr (n + 1);
ctr := (n + 1);
c

(* val matches: #i:id -> l:plainLen -> cipher i l -> entry i -> Tot bool *)
Expand All @@ -253,20 +253,20 @@ val decrypt: #i:id -> d:reader i -> l:plainLen -> c:cipher i l
-> ST (option (plain i (min l (max_TLSPlaintext_fragment_length + 1))))
(requires (fun h0 ->
l <= max_TLSPlaintext_fragment_length /\ // FIXME ADL: why is plainLen <= max_TLSCiphertext_fragment_length_13 ?? Fix StreamPlain!
m_sel h0 (ctr d.counter) < max_ctr))
HS.sel h0 (ctr d.counter) < max_ctr))
(ensures (fun h0 res h1 ->
let j : nat = m_sel h0 (ctr d.counter) in
let j : nat = HS.sel h0 (ctr d.counter) in
(authId i ==>
(let log = m_sel h0 (ilog d.log) in
(let log = HS.sel h0 (ilog d.log) in
if j < Seq.length log && matches l c (Seq.index log j)
then res = Some (Entry?.p (Seq.index log j))
else res = None)) /\
(match res with
| None -> HS.modifies_transitively Set.empty h0 h1
| _ -> let ctr_counter_as_hsref = as_hsref (ctr d.counter) in
| _ -> let ctr_counter_as_hsref = ctr d.counter in
HS.modifies_one d.region h0 h1 /\
modifies_ref d.region (Set.singleton (Heap.addr_of (as_ref ctr_counter_as_hsref))) h0 h1 /\
m_sel h1 (ctr d.counter) === j + 1)))
HS.sel h1 (ctr d.counter) === j + 1)))

val strip_refinement: #a:Type -> #p:(a -> Type0) -> o:option (x:a{p x}) -> option a
let strip_refinement #a #p = function
Expand All @@ -277,18 +277,18 @@ let strip_refinement #a #p = function
// decryption, idealized as a lookup of (c,ad) in the log for safe instances
let decrypt #i d l c =
let ctr = ctr d.counter in
m_recall ctr;
let j = m_read ctr in
recall ctr;
let j = !ctr in
if authId i
then
let ilog = ilog d.log in
let log = m_read ilog in
let log = !ilog in
let ictr: ideal_ctr d.region i ilog = d.counter in
let _ = testify_seqn ictr in //now we know that j <= Seq.length log
if j < Seq.length log && matches l c (Seq.index log j) then
begin
increment_seqn ictr;
m_recall ctr;
recall ctr;
Some (Entry?.p (Seq.index log j))
end
else None
Expand All @@ -305,7 +305,7 @@ let decrypt #i d l c =
begin
assert (Platform.Bytes.length pr == l);
let p = strip_refinement (mk_plain i l pr) in
if Some? p then m_write ctr (j + 1);
if Some? p then ctr := (j + 1);
p
end
end
Expand Down
6 changes: 3 additions & 3 deletions src/tls/TLSInfo.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ let safety_table : s_table =
type registered (i:pre_index) =
(if Flags.ideal_KEF then
let log : i_safety_log = safety_table in
MR.witnessed (MM.defined log i)
witnessed (MM.defined log i)
else True)

type valid (i:pre_index) =
Expand Down Expand Up @@ -563,13 +563,13 @@ type index = i:pre_index{valid i}
type honest (i:index) =
(if Flags.ideal_KEF then
let log : i_safety_log = safety_table in
MR.witnessed (MM.contains log i true)
witnessed (MM.contains log i true)
else False)

type dishonest (i:index) =
(if Flags.ideal_KEF then
let log : i_safety_log = safety_table in
MR.witnessed (MM.contains log i false)
witnessed (MM.contains log i false)
else True)

type esId = i:pre_esId{valid (I_ES i)}
Expand Down

0 comments on commit be1b889

Please sign in to comment.