From c161a1755c08dfc69eb2c6db023669f59e980177 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Tue, 7 Jan 2025 20:40:59 +0100 Subject: [PATCH] Cleaning up the trusted compute file --- theories/cap_lang.v | 6 + theories/examples/enclaves/trusted_compute.v | 319 ++++++------------- theories/logical_mapsto.v | 16 +- theories/logrel.v | 100 +++++- theories/machine_base.v | 19 ++ theories/rules/rules_EStoreId.v | 6 - 6 files changed, 241 insertions(+), 225 deletions(-) diff --git a/theories/cap_lang.v b/theories/cap_lang.v index 37da2310..d082aeb6 100644 --- a/theories/cap_lang.v +++ b/theories/cap_lang.v @@ -445,6 +445,12 @@ Section opsem. then Some (Nat.div (Z.to_nat oa) 2) else Some (Nat.div (Z.to_nat (oa^-1)%f) 2). + Definition has_seal (ot : Z) (tid : TIndex) : Prop := + match finz.of_z ot with + | Some ot => tid_of_otype ot = Some tid + | None => False + end. + Definition measure (m : Mem) (b e: Addr) := let instructions : list Word := map snd diff --git a/theories/examples/enclaves/trusted_compute.v b/theories/examples/enclaves/trusted_compute.v index bdc859a3..76c9fe8c 100644 --- a/theories/examples/enclaves/trusted_compute.v +++ b/theories/examples/enclaves/trusted_compute.v @@ -7,72 +7,12 @@ From cap_machine Require Import proofmode. From cap_machine Require Import macros_new. Open Scope Z_scope. -(* TODO move in finz *) -Lemma finz_incr_minus_id - {finz_bound : Z} - (f : finz finz_bound) (z : Z) - (finz_lt : (z LSCap p b e a v - | SSealRange p b e a => LSSealRange p b e a - end. - -Definition word_to_lword (w : Word) (v : Version) := - match w with - | WInt z => LInt z - | WSealable sb => LWSealable (sealable_to_lsealable sb v) - | WSealed ot sb => LWSealed ot (sealable_to_lsealable sb v) - end. - -(* TODO move in common file for sealing *) -(* This section redefines useful definitions from `arch_sealing` along with further explanations. *) -Section invariants. - Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ} - {nainv: logrel_na_invs Σ} `{MP: MachineParameters}. - Definition valid_sealed w o (Φ : LWord -> iProp Σ) := - (∃ sb, ⌜w = LWSealed o sb⌝ ∗ ⌜∀ w : leibnizO LWord, Persistent (Φ w)⌝ - ∗ seal_pred o Φ ∗ Φ (LWSealable sb))%I. - Lemma interp_valid_sealed sb o: - interp (LWSealed o sb) -∗ ∃ Φ, ▷ valid_sealed (LWSealed o sb) o Φ. - Proof. - iIntros "Hsl /=". rewrite fixpoint_interp1_eq /= /valid_sealed. - iDestruct "Hsl" as (P) "(%Hpers & Hpred & HP)". - iExists P, sb; repeat iSplit; [auto | auto | iFrame.. ]. - Qed. - - Lemma seal_pred_valid_sealed_eq τ w Φ Φ' {Hpers : ∀ w, Persistent (Φ w)} : - seal_pred τ Φ -∗ valid_sealed w τ Φ' -∗ (∀ w, ▷ (Φ w ≡ Φ' w)). - Proof. - iIntros "Hsp Hvs". - iDestruct "Hvs" as (sb) "(_ & _ & Hsp' & _)". - iApply (seal_pred_agree with "Hsp Hsp'"). - Qed. - -End invariants. - +(* TODO @June is there a way to define a typeclass or something + for helping with reasoning and modularity ? *) Section sealed_42. Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ} {nainv: logrel_na_invs Σ} `{MP: MachineParameters}. - - Definition seal_capN : namespace := nroot .@ "seal_cap". - Program Definition f42 : Addr := (finz.FinZ 42 eq_refl eq_refl). Definition sealed_42 : LWord → iProp Σ := λ w, (∃ b e v, ⌜w = LCap O b e f42 v⌝)%I. @@ -93,7 +33,10 @@ End sealed_42. Section trusted_compute_example. - Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg : sealStoreG Σ} `{MP: MachineParameters}. + Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg : sealStoreG Σ} + {nainv: logrel_na_invs Σ} `{MP: MachineParameters}. + + Definition trusted_computeN : namespace := nroot .@ "trusted_compute". (* Data part, following the directly the main code *) Definition trusted_compute_data (linking_table_cap : LWord) : list LWord := @@ -199,15 +142,17 @@ Section trusted_compute_example. Definition trusted_compute_enclave (enclave_data_cap : LWord) : list LWord := enclave_data_cap::trusted_compute_enclave_code. - Axiom hash_trusted_compute_enclave : Z. + (* TODO @june use measure! *) + Definition hash_trusted_compute_enclave (tc_addr : Addr) : Z := + hash_concat (hash tc_addr) (hash trusted_compute_enclave_code). - Definition trusted_compute_main_code (assert_lt_offset : Z) : list LWord := + Definition trusted_compute_main_code (assert_lt_offset : Z) (tc_addr : Addr ): list LWord := let init := 0%Z in let callback := trusted_compute_main_init_len in let data := trusted_compute_main_init_len + trusted_compute_main_callback_len in let fails := (data - 1)%Z in (trusted_compute_main_code_init0 init callback data) ++ - (trusted_compute_main_code_callback0 callback fails hash_trusted_compute_enclave assert_lt_offset). + (trusted_compute_main_code_callback0 callback fails (hash_trusted_compute_enclave tc_addr) assert_lt_offset). Definition trusted_compute_main_code_len : Z := Eval cbv in trusted_compute_main_init_len + trusted_compute_main_callback_len. @@ -216,154 +161,17 @@ Section trusted_compute_example. Eval cbv in trusted_compute_main_code_len + trusted_compute_main_data_len. - (** Specification init code *) - Lemma trusted_compute_main_init_spec - (b_main : Addr) - (pc_v adv_v : Version) - (assert_lt_offset : Z) - (w0 w1 w2 w3 w4 wadv : LWord) - φ : - - let e_main := (b_main ^+ trusted_compute_main_len)%a in - let a_callback := (b_main ^+ trusted_compute_main_init_len)%a in - let a_data := (b_main ^+ trusted_compute_main_code_len)%a in - - let trusted_compute_main := trusted_compute_main_code assert_lt_offset in - ContiguousRegion b_main trusted_compute_main_len -> - ⊢ (( - codefrag b_main pc_v trusted_compute_main - - ∗ PC ↦ᵣ LCap RWX b_main e_main b_main pc_v - ∗ r_t0 ↦ᵣ wadv - ∗ r_t1 ↦ᵣ w1 - ∗ r_t2 ↦ᵣ w2 - (* NOTE this post-condition stops after jumping to the adversary *) - ∗ ▷ ( codefrag b_main pc_v trusted_compute_main - ∗ PC ↦ᵣ updatePcPermL wadv - ∗ r_t0 ↦ᵣ wadv - ∗ r_t1 ↦ᵣ (LCap E b_main e_main a_callback pc_v) - ∗ r_t2 ↦ᵣ LInt 0 - -∗ WP Seq (Instr Executable) {{ φ }})) - -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})%I. - Proof. - - (* We define a local version of solve_addr, which subst and unfold every computed addresses *) - Local Tactic Notation "solve_addr'" := - repeat (lazymatch goal with x := _ |- _ => subst x end) - ; repeat (match goal with - | H: ContiguousRegion _ _ |- _ => - rewrite /ContiguousRegion /trusted_compute_main_len in H - end) - ; rewrite !/trusted_compute_main_code_len /trusted_compute_main_len - /trusted_compute_main_init_len /trusted_compute_main_callback_len - ; solve_addr. - - intros ???? Hregion. - iIntros "(Hcode & HPC & Hr0 & Hr1 & Hr2 & Hφ)". - codefrag_facts "Hcode". - iGo "Hcode". - rewrite decode_encode_perm_inv; by cbn. - rewrite decode_encode_perm_inv. - iGo "Hcode". - iApply (wp_wand with "[-]"); last (iIntros (v) "H"; by iLeft). - iApply "Hφ". - iFrame. - Qed. - - (** Specification callback code *) - - Context {nainv: logrel_na_invs Σ} . - (* Define all the invariants *) - Definition trusted_computeN : namespace := nroot .@ "trusted_compute". - - (* Linking table invariant *) - Definition link_tableN := (trusted_computeN.@"link_table"). - Definition link_table_inv - v_link - assert_entry b_assert e_assert v_assert := - na_inv logrel_nais link_tableN - ((assert_entry, v_link) ↦ₐ LCap E b_assert e_assert b_assert v_assert)%I. - - (* Assert invariant *) - Definition assertN := (trusted_computeN.@"assert"). - Definition assert_inv b_a a_flag e_a v_assert := - na_inv logrel_nais assertN (assert_inv b_a a_flag e_a v_assert). - - Definition flag_assertN := (trusted_computeN.@"flag_assert"). - Definition flag_inv a_flag v_flag := - inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z). - - (* TODO move in common file for custom enclave *) - Record CustomEnclave := - MkCustomEnclave { - code : list LWord; - code_region : Addr; - Penc : LWord -> iProp Σ; - Psign : LWord -> iProp Σ; - }. - - Definition custom_enclaves_map : Type := - gmap EIdentity CustomEnclave. - - Definition custom_enclaves_map_wf (cenclaves : custom_enclaves_map) := - map_Forall - (fun I ce => I = hash_concat (hash (code_region ce)) (hash (code ce))) - cenclaves. - - Definition custom_enclaveN := (trusted_computeN.@"custom_enclave"). - Definition custom_enclave_inv (cenclaves : custom_enclaves_map) := - inv custom_enclaveN - ( - ⌜ custom_enclaves_map_wf cenclaves ⌝ -∗ - □ ∀ (I : EIdentity) (tid : TIndex) (ot : OType) (ce : CustomEnclave), - enclave_all tid I - ∗ ⌜ cenclaves !! I = Some ce ⌝ - ∗ ⌜ has_seal ot tid ⌝ -∗ - if (Z.even (finz.to_z ot)) - then (seal_pred ot (Penc ce) ∗ seal_pred (ot ^+ 1)%ot (Psign ce)) - else (seal_pred (ot ^+ (-1))%ot (Penc ce) ∗ seal_pred ot (Psign ce)) - ). - - Definition custom_enclave_contract - (cenclaves : custom_enclaves_map) - := - forall - (I : EIdentity) - (b e a : Addr) (v : Version) - (b' e' a' : Addr) (v' : Version) - (enclave_data : list LWord) - (ot : OType) - (ce : CustomEnclave), - custom_enclaves_map_wf cenclaves -> - cenclaves !! I = Some ce -> - (code ce) !! 0%nat = Some (LCap RW b' e' a' v') -> - enclave_data !! 0%nat = Some (LSealRange (true,true) ot (ot^+2)%ot ot) -> - (ot + 2)%f = Some (ot ^+ 2)%f -> (* Well-formness: otype does not overflow *) - (* TODO I think we can derive following from [b',e'] -> .... *) - b' < e' -> (* Well-formness: data region contains at least one *) - b < e -> (* Well-formness: code region contains at all the code *) - I = hash_concat (hash b) (hash (tail (code ce))) -> - b = (code_region ce) -> - e = (b ^+ (length (code ce)))%a -> - (* TODO: either points-to in invariant, or upd modality in implication *) - na_inv logrel_nais (trusted_computeN.@I) - ([[ b , e ]] ↦ₐ{ v } [[ (code ce) ]] ∗ - [[ b' , e' ]] ↦ₐ{ v' } [[ enclave_data ]]) - ∗ seal_pred ot (Penc ce) - ∗ seal_pred (ot^+1)%ot (Psign ce) -∗ - interp (LCap E b e (b^+1)%a v). - (* Trusted Compute Custom Predicates *) - Definition tc_enclave_pred tc_data_cap tc_addr : CustomEnclave := - MkCustomEnclave - (trusted_compute_enclave tc_data_cap) - tc_addr - (λ w, False%I) - sealed_42. + Definition tc_enclave_pred + tc_data_cap tc_addr : CustomEnclave := + @MkCustomEnclave Σ + (trusted_compute_enclave tc_data_cap) + tc_addr + (λ w, False%I) + sealed_42. Definition tcenclaves_map tc_data_cap tc_addr : custom_enclaves_map := - {[hash_trusted_compute_enclave := tc_enclave_pred tc_data_cap tc_addr]}. - + {[hash_trusted_compute_enclave tc_addr := tc_enclave_pred tc_data_cap tc_addr]}. Lemma tc_contract tc_data_cap tc_addr : custom_enclave_contract (tcenclaves_map tc_data_cap tc_addr). @@ -377,7 +185,7 @@ Section trusted_compute_example. rewrite map_Forall_insert in Hwf_cemap; last by simplify_map_eq. destruct Hwf_cemap as [ Hwf_hash _ ]. cbn in Hwf_hash. - destruct (decide (I = hash_trusted_compute_enclave)) as [->|] ; last by simplify_map_eq. + destruct (decide (I = hash_trusted_compute_enclave tc_addr)) as [->|] ; last by simplify_map_eq. clear HIhash Hwf_hash. rewrite fixpoint_interp1_eq /=. iIntros (lregs); iNext ; iModIntro. @@ -584,6 +392,80 @@ Section trusted_compute_example. Admitted. + (** Specification init code *) + Lemma trusted_compute_main_init_spec + (b_main : Addr) + (pc_v adv_v : Version) + (assert_lt_offset : Z) + (w0 w1 w2 w3 w4 wadv : LWord) + (tc_addr : Addr) + φ : + + let e_main := (b_main ^+ trusted_compute_main_len)%a in + let a_callback := (b_main ^+ trusted_compute_main_init_len)%a in + let a_data := (b_main ^+ trusted_compute_main_code_len)%a in + + let trusted_compute_main := trusted_compute_main_code assert_lt_offset in + ContiguousRegion b_main trusted_compute_main_len -> + ⊢ (( + codefrag b_main pc_v (trusted_compute_main tc_addr) + + ∗ PC ↦ᵣ LCap RWX b_main e_main b_main pc_v + ∗ r_t0 ↦ᵣ wadv + ∗ r_t1 ↦ᵣ w1 + ∗ r_t2 ↦ᵣ w2 + (* NOTE this post-condition stops after jumping to the adversary *) + ∗ ▷ ( codefrag b_main pc_v (trusted_compute_main tc_addr) + ∗ PC ↦ᵣ updatePcPermL wadv + ∗ r_t0 ↦ᵣ wadv + ∗ r_t1 ↦ᵣ (LCap E b_main e_main a_callback pc_v) + ∗ r_t2 ↦ᵣ LInt 0 + -∗ WP Seq (Instr Executable) {{ φ }})) + -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})%I. + Proof. + + (* We define a local version of solve_addr, which subst and unfold every computed addresses *) + Local Tactic Notation "solve_addr'" := + repeat (lazymatch goal with x := _ |- _ => subst x end) + ; repeat (match goal with + | H: ContiguousRegion _ _ |- _ => + rewrite /ContiguousRegion /trusted_compute_main_len in H + end) + ; rewrite !/trusted_compute_main_code_len /trusted_compute_main_len + /trusted_compute_main_init_len /trusted_compute_main_callback_len + ; solve_addr. + + intros ???? Hregion. + iIntros "(Hcode & HPC & Hr0 & Hr1 & Hr2 & Hφ)". + codefrag_facts "Hcode". + iGo "Hcode". + rewrite decode_encode_perm_inv; by cbn. + rewrite decode_encode_perm_inv. + iGo "Hcode". + iApply (wp_wand with "[-]"); last (iIntros (v) "H"; by iLeft). + iApply "Hφ". + iFrame. + Qed. + + (** Specification callback code *) + + (* Define all the invariants *) + (* Linking table invariant *) + Definition link_tableN := (trusted_computeN.@"link_table"). + Definition link_table_inv + v_link + assert_entry b_assert e_assert v_assert := + na_inv logrel_nais link_tableN + ((assert_entry, v_link) ↦ₐ LCap E b_assert e_assert b_assert v_assert)%I. + + (* Assert invariant *) + Definition assertN := (trusted_computeN.@"assert"). + Definition assert_inv b_a a_flag e_a v_assert := + na_inv logrel_nais assertN (assert_inv b_a a_flag e_a v_assert). + + Definition flag_assertN := (trusted_computeN.@"flag_assert"). + Definition flag_inv a_flag v_flag := + inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z). Lemma trusted_compute_callback_code_spec (b_main adv adv_end: Addr) @@ -623,7 +505,7 @@ Section trusted_compute_example. ∗ interp w0 ⊢ (( - codefrag b_main pc_v trusted_compute_main + codefrag b_main pc_v (trusted_compute_main tc_addr) ∗ ((a_data)%a, pc_v) ↦ₐ link_cap ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LCap RWX b_main e_main a_data pc_v) @@ -637,7 +519,7 @@ Section trusted_compute_example. ∗ na_own logrel_nais ⊤ (* NOTE this post-condition stops after jumping to the adversary *) - ∗ ▷ ( codefrag b_main pc_v trusted_compute_main + ∗ ▷ ( codefrag b_main pc_v (trusted_compute_main tc_addr) ∗ ((a_data)%a, pc_v) ↦ₐ link_cap ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LCap RWX b_main e_main a_data pc_v) @@ -711,7 +593,7 @@ Section trusted_compute_example. 2:{ wp_end; by iRight. } iInstr "Hcode". (* Sub *) - destruct (decide (I = hash_trusted_compute_enclave)) as [-> | HnI] + destruct (decide (I = hash_trusted_compute_enclave tc_addr)) as [-> | HnI] ; cycle 1. { (* Not the right enclave *) iInstr "Hcode". (* Jnz *) @@ -719,8 +601,7 @@ Section trusted_compute_example. iInstr "Hcode". (* Fail *) wp_end; by iRight. } - replace (hash_trusted_compute_enclave - hash_trusted_compute_enclave) - with 0 by lia. + replace ( _ - _) with 0 by lia. iInstr "Hcode". (* Jnz *) iDestruct (interp_valid_sealed with "Hinterp_w0") as (Φ) "Hseal_valid". rewrite /custom_enclave_inv. @@ -824,4 +705,8 @@ Section trusted_compute_example. iApply "Hcont"; iFrame. Admitted. + (* TODO *) + (* Lemma trusted_compute_full_run_spec *) + + End trusted_compute_example. diff --git a/theories/logical_mapsto.v b/theories/logical_mapsto.v index 5130ec2c..6089a265 100644 --- a/theories/logical_mapsto.v +++ b/theories/logical_mapsto.v @@ -76,13 +76,27 @@ Ltac destruct_lword lw := let sd := fresh "sd" in destruct lw as [ z | [p b e a v | p b e a] | o [p b e a v | p b e a]]. -(* Getters lword and laddr *) +(* Setters and Getters lword and laddr *) + +Definition sealable_to_lsealable (sb : Sealable) (v : Version) := + match sb with + | SCap p b e a => LSCap p b e a v + | SSealRange p b e a => LSSealRange p b e a + end. + Definition lsealable_get_sealable (lsb : LSealable) : Sealable := match lsb with | LSCap p b e a v => SCap p b e a | LSSealRange p ob oe oa => SSealRange p ob oe oa end. +Definition word_to_lword (w : Word) (v : Version) := + match w with + | WInt z => LInt z + | WSealable sb => LWSealable (sealable_to_lsealable sb v) + | WSealed ot sb => LWSealed ot (sealable_to_lsealable sb v) + end. + Definition lword_get_word (lw : LWord) : Word := match lw with | LWInt z => WInt z diff --git a/theories/logrel.v b/theories/logrel.v index 4c31ee62..6213d560 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -33,7 +33,7 @@ Class logrel_na_invs Σ := Section logrel. Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ} {nainv: logrel_na_invs Σ} - `{MachineParameters}. + `{MP: MachineParameters}. Notation D := ((leibnizO LWord) -n> iPropO Σ). Notation R := ((leibnizO LReg) -n> iPropO Σ). @@ -1027,3 +1027,101 @@ Section logrel. Qed. End logrel. + +(* A couple of lemmas and definitions for reasoning about sealed capabilities *) +Section sealing_reasoning. + Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ} + {nainv: logrel_na_invs Σ} `{MP: MachineParameters}. + + Definition valid_sealed w o (Φ : LWord -> iProp Σ) := + (∃ sb, ⌜w = LWSealed o sb⌝ ∗ ⌜∀ w : leibnizO LWord, Persistent (Φ w)⌝ + ∗ seal_pred o Φ ∗ Φ (LWSealable sb))%I. + Lemma interp_valid_sealed sb o: + interp (LWSealed o sb) -∗ ∃ Φ, ▷ valid_sealed (LWSealed o sb) o Φ. + Proof. + iIntros "Hsl /=". rewrite fixpoint_interp1_eq /= /valid_sealed. + iDestruct "Hsl" as (P) "(%Hpers & Hpred & HP)". + iExists P, sb; repeat iSplit; [auto | auto | iFrame.. ]. + Qed. + + Lemma seal_pred_valid_sealed_eq τ w Φ Φ' {Hpers : ∀ w, Persistent (Φ w)} : + seal_pred τ Φ -∗ valid_sealed w τ Φ' -∗ (∀ w, ▷ (Φ w ≡ Φ' w)). + Proof. + iIntros "Hsp Hvs". + iDestruct "Hvs" as (sb) "(_ & _ & Hsp' & _)". + iApply (seal_pred_agree with "Hsp Hsp'"). + Qed. + +End sealing_reasoning. + + +Section custom_enclaves. + Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ} + {nainv: logrel_na_invs Σ} `{MP: MachineParameters}. + + Record CustomEnclave := + MkCustomEnclave { + code : list LWord; + code_region : Addr; + Penc : LWord -> iProp Σ; + Psign : LWord -> iProp Σ; + }. + + Definition custom_enclaves_map : Type := + gmap EIdentity CustomEnclave. + + Definition custom_enclaves_map_wf (cenclaves : custom_enclaves_map) := + map_Forall + (fun I ce => I = hash_concat (hash (code_region ce)) (hash (code ce))) + cenclaves. + + Definition custom_enclaveN := (nroot.@"custom_enclave"). + Definition custom_enclave_inv (cenclaves : custom_enclaves_map) := + inv custom_enclaveN + ( + ⌜ custom_enclaves_map_wf cenclaves ⌝ -∗ + □ ∀ (I : EIdentity) (tid : TIndex) (ot : OType) (ce : CustomEnclave), + enclave_all tid I + ∗ ⌜ cenclaves !! I = Some ce ⌝ + ∗ ⌜ has_seal ot tid ⌝ -∗ + if (Z.even (finz.to_z ot)) + then (seal_pred ot (Penc ce) ∗ seal_pred (ot ^+ 1)%ot (Psign ce)) + else (seal_pred (ot ^+ (-1))%ot (Penc ce) ∗ seal_pred ot (Psign ce)) + ). + + (* TODO @June explanation of the contract *) + Definition custom_enclave_contract + (cenclaves : custom_enclaves_map) + := + forall + (I : EIdentity) + (b e a : Addr) (v : Version) + (b' e' a' : Addr) (v' : Version) + (enclave_data : list LWord) + (ot : OType) + (ce : CustomEnclave), + + custom_enclaves_map_wf cenclaves -> + + cenclaves !! I = Some ce -> + (code ce) !! 0%nat = Some (LCap RW b' e' a' v') -> + enclave_data !! 0%nat = Some (LSealRange (true,true) ot (ot^+2)%ot ot) -> + + (ot + 2)%ot = Some (ot ^+ 2)%ot -> (* Well-formness: otype does not overflow *) + (* TODO I think we can derive following from [b',e'] -> .... *) + (b' < e')%a -> (* Well-formness: data region contains at least one *) + (b < e)%a -> (* Well-formness: code region contains at all the code *) + + I = hash_concat (hash b) (hash (tail (code ce))) -> + b = (code_region ce) -> + e = (b ^+ (length (code ce)))%a -> + + na_inv logrel_nais (custom_enclaveN.@I) + ([[ b , e ]] ↦ₐ{ v } [[ (code ce) ]] ∗ + [[ b' , e' ]] ↦ₐ{ v' } [[ enclave_data ]]) + + ∗ seal_pred ot (Penc ce) + ∗ seal_pred (ot^+1)%ot (Psign ce) -∗ + + interp (LCap E b e (b^+1)%a v). +End custom_enclaves. diff --git a/theories/machine_base.v b/theories/machine_base.v index f23ed45a..7c4ddf5d 100644 --- a/theories/machine_base.v +++ b/theories/machine_base.v @@ -471,6 +471,25 @@ Proof. rewrite /isWithin. solve_addr. Qed. +(* TODO move in finz *) +Lemma finz_incr_minus_id + {finz_bound : Z} + (f : finz finz_bound) (z : Z) + (finz_lt : (z tid_of_otype ot = Some tid - | None => False - end. - (* TODO @Denis *) Lemma wp_estoreid_success_unknown E pc_p pc_b pc_e pc_a pc_a' pc_v lw rd rs otype any : decodeInstrWL lw = EStoreId rd rs →