From 5e0a493740677f895b5dbb42f9eca8758cf8217d Mon Sep 17 00:00:00 2001 From: Denis Carnier Date: Tue, 9 Jul 2024 13:40:28 +0200 Subject: [PATCH] Some more thoughts on EInit --- theories/cap_lang.v | 17 ++++++++++++----- theories/machine_base.v | 8 ++++---- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/theories/cap_lang.v b/theories/cap_lang.v index ef7d1a5d..12338f64 100644 --- a/theories/cap_lang.v +++ b/theories/cap_lang.v @@ -26,6 +26,10 @@ Definition update_regs (φ: ExecConf) (reg' : Reg) : ExecConf := MkExecConf reg' Definition update_reg (φ: ExecConf) (r: RegName) (w: Word): ExecConf := update_regs φ (<[ r := w ]> (reg φ)). Definition update_mem (φ: ExecConf) (a: Addr) (w: Word): ExecConf := MkExecConf (reg φ) (<[a:=w]>(mem φ)) (etable φ) (enumcur φ). Definition update_etable (φ: ExecConf) (i: TIndex) (eid : EId) (enum : ENum): ExecConf := MkExecConf (reg φ) (mem φ) (<[i := (eid,enum)]>(etable φ)) (enumcur φ). +(* use add_etable or fresh_table_index *) +(* either use a global freshness counter, never reusing indices + or check domain of table and use minimal unused index + or axiomatize a freshness function -- keeps it implementation independent *) Definition update_enumcur (φ: ExecConf) (enumcur : ENum): ExecConf := MkExecConf (reg φ) (mem φ) (etable φ) enumcur. (* Note that the `None` values here also undo any previous changes that were tentatively made in the same step. This is more consistent across the board. *) @@ -416,6 +420,9 @@ Section opsem. Axiom contains_cap : Mem -> Addr -> Addr -> bool. Axiom measure : Mem -> Addr -> Addr -> Z. + Axiom coerce_Z : forall A, finz A -> Z. + Axiom fresh_table_index : ETable -> TIndex. + Definition exec_opt (i: instr) (φ: ExecConf): option Conf := match i with @@ -588,28 +595,28 @@ Section opsem. if decide (readAllowed p' && writeAllowed p') (* need RW for data section *) then let succ_sweep_mem := sweep_addr (mem φ) (reg φ) b in (* sweep the memory excluding the data cap at location b *) let succ_sweep_reg := sweep_reg (mem φ) (reg φ) rs in (* sweep the registers excluding the code cap in register rs *) - let succ_no_caps := negb (contains_cap (mem φ) (b+1) e) in (* ccap does not contain capabilities dcap at addr b *) + let succ_no_caps := negb (contains_cap (mem φ) (b^+1)%a e) in (* ccap does not contain capabilities except dcap at addr b *) (* @TODO no longer needed? *) if (succ_sweep_mem && succ_sweep_reg && succ_no_caps) then let ec := enumcur φ in (* ALLOCATION OF THE ENCLAVE'S SEALS *) (* If IIUC, the EC register acts as a bump allocator for enclave otypes *) (* therefore, to write the seals for the enclave, it is sufficient to use the value of the EC register and (by convention) assume 2 * EC is seal and 2 * EC + 1 is unseal. *) - let seals := (WSealRange (true, true) (2%Z*ec)%f (2*ec+2) (2*ec)) in + let seals := (WSealRange (true, true) (2%Z * ec)%a (2*ec+2) (2*ec)) in let m' := update_mem φ b' seals in (* these seals should be stored at address b' i.e. the base address of the enclave's data section *) let identity := measure (mem φ) (b+1) e in (* calculate hash of ccap *) - let t' := update_etable m' 0 (* @todo: which table index? Is it the same as the eid *) ec identity in + let t' := update_etable m' (fresh_table_index (etable φ)) ec identity in (* @todo: check size bounds on the table etc. *) let ec' := update_enumcur t' (ec + 2) in (* increment enumcur in φ by 2 *) - let r' := update_reg ec' rd (WCap E b e a) in + let r' := update_reg ec' rd (WCap E b e a) in (* @Denis should we use a or b+1 or ? depending on starting address enclave has different behaviour *) updatePC r' (* we should flip argument order so we can just compose these intermediate ExecConfs *) (* denis says: o_entry still needed? Was part of original proposal, re: sealed pairs I believe. *) (* sccap ← (* seal ccap with o_entry *) *) (* sdcap ← (* seal dcap with o_entry *) *) - else (* memory sweep fails *) None + else (* memory sweep fails *) None (* @TODO maybe update Opsem and return 0 in rd to signal failure? *) else (* no RW access for data cap *) None else (* no RX access for code cap *) None diff --git a/theories/machine_base.v b/theories/machine_base.v index 8050be9b..ef274d50 100644 --- a/theories/machine_base.v +++ b/theories/machine_base.v @@ -70,7 +70,6 @@ Definition cst : Z → (Z+RegName)%type := inl. Coercion regn : RegName >-> sum. Coercion cst : Z >-> sum. - (* Registers and memory: maps from register names/addresses to words *) Definition Reg := gmap RegName Word. @@ -81,10 +80,11 @@ Definition TableSize: nat := 128. Global Opaque TableSize. Definition MaxENum: nat := 1024. Global Opaque MaxENum. -Definition TIndex := (finz TableSize). +(* Definition TIndex := (finz TableSize). *) +Definition TIndex := (finz MaxENum). Definition EId := Z. (* For now, we assume the hash to be unbounded *) Definition ENum := (finz MaxENum). (* The max # of supported enclaves *) -Definition ETable := gmap TIndex (EId * ENum). +Definition ETable := gmap TIndex (EId * ENum). (* Check sail impl. of CHERi-TrEE for how to get table index ? They don't have a table but a distinct memory region *) (* EqDecision instances *) @@ -753,7 +753,7 @@ Global Instance word_inhabited: Inhabited Word := populate (WInt 0). Global Instance addr_inhabited: Inhabited Addr := populate (@finz.FinZ MemNum 0%Z eq_refl eq_refl). Global Instance otype_inhabited: Inhabited OType := populate (@finz.FinZ ONum 0%Z eq_refl eq_refl). Global Instance enum_inhabited: Inhabited ENum := populate (@finz.FinZ MaxENum 0%Z eq_refl eq_refl). -Global Instance tindex_inhabited: Inhabited TIndex := populate (@finz.FinZ TableSize 0%Z eq_refl eq_refl). +(* Global Instance tindex_inhabited: Inhabited TIndex := populate (@finz.FinZ TableSize 0%Z eq_refl eq_refl). *) Global Instance etable_inhabited: Inhabited ETable. Proof. solve [typeclasses eauto]. Defined. Global Instance instr_countable : Countable instr.