Skip to content

Commit

Permalink
Fix opsem TEE
Browse files Browse the repository at this point in the history
  • Loading branch information
@JuneRousseau
JuneRousseau committed Dec 12, 2024
1 parent ff51695 commit 379b765
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 35 deletions.
65 changes: 39 additions & 26 deletions theories/cap_lang.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -418,6 +418,14 @@ Section opsem.
fun w => match w with WCap p b e a | WSealed _ (SCap p b e a) => Some (p, b, e, a)
| _ => None end.

Definition get_sealing_cap : Word -> option (SealPerms * OType * OType * OType) :=
fun w => match w with WSealRange p b e a => Some (p, b, e, a)
| _ => None end.

Definition get_sealed_otype : Word -> option OType :=
fun w => match w with WSealed ot _ => Some ot
| _ => None end.

Definition contains_cap (mem : Mem) (b : Addr) (e : Addr) : Prop :=
map_Forall (λ (a : Addr) (wa : Word),
if decide ((a <= b)%a ∧ (b <= e)%a)
Expand Down Expand Up @@ -460,20 +468,20 @@ Section opsem.
end). apply Z.ltb_lt. auto. apply Z.leb_le. auto.
Defined.

Definition seal_of_oa (oa : OType) : option ENum :=
Definition eid_of_otype (oa : OType) : option ENum :=
finz.to_z <$> if (Z.even (finz.to_z oa))
then (finz_div_nat oa 2)
else finz_div_nat (oa^-1)%f 2.

Definition has_seal : Word -> option ENum :=
λ σ, (match σ with
| WSealRange _ _ _ oa => seal_of_oa oa
| _ => None (* rs does not contain seals *)
end).
(* Definition has_seal : Word -> option ENum := *)
(* λ σ, (match σ with *)
(* | WSealRange _ _ _ oa => seal_of_oa oa *)
(* | _ => None (* rs does not contain seals *) *)
(* end). *)

Axiom measure : Mem -> Addr -> Addr -> Z.

Definition eid_of_enum (etable : ETable) (enum : ENum) : option EId :=
Definition id_of_eid (etable : ETable) (enum : ENum) : option EId :=
map_fold
(λ idx p oi,
match oi with
Expand All @@ -483,7 +491,7 @@ Section opsem.
None
etable.

Definition tindex_of_eid (etable : ETable) (eid : EId) : option TIndex :=
Definition tindex_of_id (etable : ETable) (eid : EId) : option TIndex :=
map_fold
(λ idx p oi,
match oi with
Expand Down Expand Up @@ -698,28 +706,26 @@ Section opsem.
|>> updatePC

(* enclave deinitialization *)
| EDeInit rd rs =>
σ ← (reg φ) !! rs; (* σ should be a seal/unseal pair *)
eid ← has_seal σ;
i ← tindex_of_eid (etable φ) eid;
| EDeInit rs =>
wσ ← (reg φ) !! rs; (* σ should be a seal/unseal pair *)
'(p,σb,σe,σa) ← get_sealing_cap wσ;
when ((bool_decide (p = (true,true))) && (σe =? σb^+2)%ot) then
eid ← eid_of_otype σb;
i ← tindex_of_id (etable φ) eid;

(* UPDATE THE MACHINE STATE *)
φ |>> remove_from_etable i
|>> update_reg rd (WInt 1) (* write 1 (success) to rd reg *) (* Denis says: no longer needed since machine either fails or ends up in this state *)
|>> updatePC

(* enclave local attestation *)
| EStoreId rd rs1 rs2 =>
σ ← (reg φ) !! rs1;
enum ← has_seal σ;
id ← eid_of_enum (etable φ) enum;
wrs2 ← (reg φ) !! rs2;
'(p, b, e, a) ← get_wcap wrs2;
| EStoreId rd rs =>
wσ ← (reg φ) !! rs;
σa ← get_sealed_otype wσ;
eid ← eid_of_otype σa;
id ← id_of_eid (etable φ) eid;

(* UPDATE THE MACHINE STATE *)
when (writeAllowed p && withinBounds b e a) then
φ |>> update_mem a (WInt id)
|>> update_reg rd (WInt 1)
φ |>> update_reg rd (WInt id)
|>> updatePC

(* memory sweep *)
Expand Down Expand Up @@ -995,13 +1001,20 @@ Section opsem.
; cbn in *
; case_match).
all: repeat destruct (finz.of_z _); cbn in *
; repeat destruct (has_seal _); cbn in *
; repeat destruct (tindex_of_eid _); cbn in *
; repeat destruct (eid_of_enum _); cbn in *
; repeat destruct (get_wcap_scap _); cbn in *.
; repeat destruct (get_sealing_cap _); cbn in *
; repeat destruct (get_sealed_otype _); cbn in *
; repeat destruct (tindex_of_id _); cbn in *
; repeat destruct (eid_of_otype _); cbn in *
; repeat destruct (get_wcap_scap _); cbn in *
; repeat destruct (id_of_eid _); cbn in *.
all: repeat destruct p.
all: try apply updatePC_some in Heqo as [φ' Heqo]; eauto.
all: simplify_eq; try by exfalso.
all: repeat destruct (eid_of_otype _); cbn in *
; repeat destruct (tindex_of_id _); cbn in *.
all: destruct (_ && _).
all: try apply updatePC_some in Heqo as [φ' Heqo]; eauto.
all: simplify_eq; try by exfalso.
Qed.

End opsem.
Expand Down
18 changes: 9 additions & 9 deletions theories/machine_base.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,9 +57,9 @@ Inductive instr: Type :=
| GetOType (dst r: RegName)
| Seal (dst r1 r2: RegName)
| UnSeal (dst r1 r2: RegName)
| EInit (dst r: RegName)
| EDeInit (dst r: RegName)
| EStoreId (dst r1 r2: RegName)
| EInit (dst src: RegName)
| EDeInit (r: RegName)
| EStoreId (dst src: RegName)
| IsUnique (dst src: RegName)
| Fail
| Halt.
Expand Down Expand Up @@ -782,9 +782,9 @@ Proof.
| GetWType dst r => GenNode 16 [GenLeaf (inl dst); GenLeaf (inl r)]
| Seal dst r1 r2 => GenNode 17 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)]
| UnSeal dst r1 r2 => GenNode 18 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)]
| EInit dst r => GenNode 19 [GenLeaf (inl dst); GenLeaf (inl r)]
| EDeInit dst r => GenNode 20 [GenLeaf (inl dst); GenLeaf (inl r)]
| EStoreId dst r1 r2 => GenNode 21 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)]
| EInit dst src => GenNode 19 [GenLeaf (inl dst); GenLeaf (inl src)]
| EDeInit r => GenNode 20 [GenLeaf (inl r)]
| EStoreId dst src => GenNode 21 [GenLeaf (inl dst); GenLeaf (inl src)]
| IsUnique dst src => GenNode 22 [GenLeaf (inl dst); GenLeaf (inl src)]
| Fail => GenNode 23 []
| Halt => GenNode 24 []
Expand All @@ -810,9 +810,9 @@ Proof.
| GenNode 16 [GenLeaf (inl dst); GenLeaf (inl r)] => GetWType dst r
| GenNode 17 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)] => Seal dst r1 r2
| GenNode 18 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)] => UnSeal dst r1 r2
| GenNode 19 [GenLeaf (inl dst); GenLeaf (inl r)] => EInit dst r
| GenNode 20 [GenLeaf (inl dst); GenLeaf (inl r)] => EDeInit dst r
| GenNode 21 [GenLeaf (inl dst); GenLeaf (inl r1); GenLeaf (inl r2)] => EStoreId dst r1 r2
| GenNode 19 [GenLeaf (inl dst); GenLeaf (inl src)] => EInit dst src
| GenNode 20 [GenLeaf (inl r)] => EDeInit r
| GenNode 21 [GenLeaf (inl dst); GenLeaf (inl src)] => EStoreId dst src
| GenNode 22 [GenLeaf (inl dst); GenLeaf (inl src)] => IsUnique dst src
| GenNode 23 [] => Fail
| GenNode 24 [] => Halt
Expand Down

0 comments on commit 379b765

Please sign in to comment.