update

Author: lixupeng

README.md

@@ -152,21 +152,13 @@ and is used throughout the layer refinement proofs.
 
 #### 1.3.3 Top-layer Security
 
-* Security property definition: [SecurityDef][]
-
-* Noninterference tactics: [NoninterferenceAux][]
-
-* Noninterference lemmas
+* Invariant definitions: [Invs][]
 
-  - [NoninterferenceLemma1][]
+* Invariant proof: [InvProofs][]
 
-  - [NoninterferenceLemma2][]
-
-  - [NoninterferenceLemma3][]
-
-* Big-Step Noninterference Theorem
+* Security property definition: [SecurityDef][]
 
-  - [Noninterference][]
+* Noninterference proof: [Noninterference][]
 
 
 ## 2. Performance Evaluation
@@ -634,11 +626,7 @@ To shutdown VMs from the client, run:
 [TrapHandlerProofCode]: proofs/sekvm/sekvm_layers/TrapHandlerProofCode.md
 [TrapHandlerCode]: proofs/sekvm/sekvm_layers/TrapHandlerCode.md
 [TrapHandlerRefine]: proofs/sekvm/sekvm_layers/TrapHandlerRefine.md
-[Invariant]: proofs/sekvm/sekvm_layers/Invariant.md
-[InvariantProof]: proofs/sekvm/sekvm_layers/InvariantProof.md
-[SecurityDef]: proofs/sekvm/sekvm_layers/SecurityDef.md
-[NoninterferenceAux]: proofs/sekvm/sekvm_layers/NoninterferenceAux.md
-[NoninterferenceLemma1]: proofs/sekvm/sekvm_layers/NoninterferenceLemma1.md
-[NoninterferenceLemma2]: proofs/sekvm/sekvm_layers/NoninterferenceLemma2.md
-[NoninterferenceLemma3]: proofs/sekvm/sekvm_layers/NoninterferenceLemma3.md
-[Noninterference]: proofs/sekvm/sekvm_layers/Noninterference.md
+[Invs]: proofs/sekvm/sekvm_layers/SecurityInvs.md
+[InvProofs]: proofs/sekvm/sekvm_layers/SecurityInvProofs.md
+[SecurityDef]: proofs/sekvm/sekvm_layers/SecuritySecurityDef.md
+[Noninterference]: proofs/sekvm/sekvm_layers/SecurityNoninterference.md

proofs/sekvm/sekvm_layers/AbstractMachine.md

@@ -1,4 +1,4 @@
-# AbstractMachine
+# Layer
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/AbstractMachineSpec.md

@@ -1,4 +1,4 @@
-# AbstractMachineSpec
+# Spec
 
 ```coq
 Require Import Coqlib.
@@ -105,14 +105,9 @@ Section AbstractMachineSpec.
     end.
 
   Definition incr_now_spec (lk: Z) (adt: RData): option RData :=
-    (* if adt.(shared).(halt) then Some adt else *)
-    (* if negb adt.(icore) || negb adt.(ihost) then None else *)
-
     match ZMap.get lk adt.(log), adt.(bars) with
     | l, Barriered =>
       let l' := TEVENT adt.(curid) (TTICKET INC_NOW) :: l in
-      (* No need to query oracle when unlocking *)
-      (* (ZMap.get lk adt.(oracle)) adt.(curid) l ++ *)
       Some adt {log: ZMap.set lk (l') adt.(log)}
                {bars: BarrierValid}
     | _, _ => None

proofs/sekvm/sekvm_layers/BootAux.md

@@ -1,4 +1,4 @@
-# BootAux
+# Layer
 
 ```coq
 Require Import Coqlib.
@@ -25,6 +25,7 @@ Require Import liblayers.compat.CompatGenSem.
 
 Require Import MemoryOps.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import BootCore.Spec.
 Require Import NPTOps.Spec.
 Require Import MmioSPTWalk.Spec.

proofs/sekvm/sekvm_layers/BootAuxCode.md

@@ -1,4 +1,4 @@
-# BootAuxCode
+# Code
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/BootAuxProofCode.md

@@ -1,4 +1,4 @@
-# BootAuxProofCode
+# ProofLow
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/BootAuxRefine.md

@@ -1,4 +1,4 @@
-# BootAuxRefine
+# ProofHigh
 
 ```coq
 Require Import Coqlib.
@@ -107,14 +107,6 @@ Section BootAuxProofHigh.
 
     End FreshPrim.
 
-    Section PassthroughPrim.
-
-      Lemma passthrough_correct:
-        sim (crel HDATA LDATA) BootAux_passthrough BootCore.
-        Admitted.
-
-    End PassthroughPrim.
-
   End WITHMEM.
 
 End BootAuxProofHigh.

proofs/sekvm/sekvm_layers/BootAuxSpec.md

@@ -1,4 +1,4 @@
-# BootAuxSpec
+# Spec
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/BootCore.md

@@ -1,4 +1,4 @@
-# BootCore
+# Layer
 
 ```coq
 Require Import Coqlib.
@@ -25,6 +25,7 @@ Require Import liblayers.compat.CompatGenSem.
 
 Require Import MemoryOps.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import BootCore.Spec.
 Require Import NPTOps.Spec.
 Require Import MmioSPTWalk.Spec.

proofs/sekvm/sekvm_layers/BootCoreCode.md

@@ -1,4 +1,4 @@
-# BootCoreCode
+# Code
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/BootCoreProofCode.md

@@ -1,4 +1,4 @@
-# BootCoreProofCode
+# ProofLow
 
 ```coq
 Require Import Coqlib.
@@ -46,6 +46,7 @@ Require Import liblayers.logic.LayerLogicImpl.
 Require Import Ctypes.
 
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import BootCore.Code.
 Require Import VMPower.Layer.
 Require Import Ident.

proofs/sekvm/sekvm_layers/BootCoreRefine.md

@@ -1,4 +1,4 @@
-# BootCoreRefine
+# ProofHigh
 
 ```coq
 Require Import Coqlib.
@@ -32,6 +32,7 @@ Require Import liblayers.compat.CompatGenSem.
 
 Require Import BootCore.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import RData.
 Require Import Constants.
 Require Import VMPower.Layer.
@@ -162,14 +163,6 @@ Section BootCoreProofHigh.
 
     End FreshPrim.
 
-    Section PassthroughPrim.
-
-      Lemma passthrough_correct:
-        sim (crel HDATA LDATA) BootCore_passthrough VMPower.
-        Admitted.
-
-    End PassthroughPrim.
-
   End WITHMEM.
 
 End BootCoreProofHigh.

proofs/sekvm/sekvm_layers/BootCoreSpec.md

@@ -1,4 +1,4 @@
-# BootCoreSpec
+# Spec
 
 ```coq
 Require Import Coqlib.
@@ -21,6 +21,7 @@ Require Import liblayers.compat.CompatLayers.
 Require Import liblayers.compat.CompatGenSem.
 
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import VMPower.Layer.
 Require Import RData.
 Require Import Constants.

proofs/sekvm/sekvm_layers/BootOps.md

@@ -1,4 +1,4 @@
-# BootOps
+# Layer
 
 ```coq
 Require Import Coqlib.
@@ -25,6 +25,7 @@ Require Import liblayers.compat.CompatGenSem.
 
 Require Import MemoryOps.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import BootOps.Spec.
 Require Import MmioSPTWalk.Spec.
 Require Import RData.

proofs/sekvm/sekvm_layers/BootOpsCode.md

@@ -1,4 +1,4 @@
-# BootOpsCode
+# Code
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/BootOpsProofCode.md

@@ -1,4 +1,4 @@
-# BootOpsProofCode
+# ProofLow
 
 ```coq
 Require Import Coqlib.
@@ -47,6 +47,7 @@ Require Import Ctypes.
 
 Require Import NPTOps.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import MemManager.Spec.
 Require Import Ident.
 Require Import BootAux.Spec.

proofs/sekvm/sekvm_layers/BootOpsRefine.md

@@ -1,4 +1,4 @@
-# BootOpsRefine
+# ProofHigh
 
 ```coq
 Require Import Coqlib.
@@ -37,6 +37,7 @@ Require Import HypsecCommLib.
 Require Import BootOps.Spec.
 Require Import BootOps.Layer.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import MemManager.Spec.
 Require Import NPTOps.Spec.
 Require Import MmioSPTOps.Spec.

proofs/sekvm/sekvm_layers/BootOpsSpec.md

@@ -1,4 +1,4 @@
-# BootOpsSpec
+# Spec
 
 ```coq
 Require Import Coqlib.
@@ -22,6 +22,7 @@ Require Import liblayers.compat.CompatGenSem.
 
 Require Import NPTOps.Spec.
 Require Import AbstractMachine.Spec.
+Require Import Locks.Spec.
 Require Import MemManager.Spec.
 Require Import BootAux.Spec.
 Require Import MmioSPTOps.Spec.

proofs/sekvm/sekvm_layers/CtxtSwitch.md

@@ -1,4 +1,4 @@
-# CtxtSwitch
+# Layer
 
 ```coq
 Require Import Coqlib.

proofs/sekvm/sekvm_layers/CtxtSwitchCode.md

@@ -1,4 +1,4 @@
-# CtxtSwitchCode
+# Code
 
 ```coq
 Require Import Coqlib.