add coq proof

README.md

@@ -6,6 +6,111 @@ This artifact includes the mechanized Coq proofs for the security of RMM/EL3M, t
 
 ## 1. Coq Proofs
 
+We first provide instructions to install Coq proof assistant and check our mechanized proofs by compilation. Then, we summarize the proof sketch.
+
+### 1.1 Coq installation
+
+We use `opam` to install Coq and other dependencies. To install `opam`:
+  ```
+  - Ubuntu:
+    sudo apt install opam
+
+  - Mac OS X:
+    brew install opam
+  ```
+Then, initialize `opam` with the specific version `4.02.0`:
+  ```
+  opam init --compiler 4.02.0
+  ```
+If you already have `opam` installed which has a different version, switch to `4.02.0`:
+  ```
+  opam switch --create 4.02.0
+  ```
+Then, use `opam` to install `coq 8.4.6` and `menhir 20151112`
+```
+opam install coq.8.4.6 menhir.20151112
+```
+Make sure `coqc` is in `PATH`, or add it manually:
+```
+export PATH="path/to/.opam/4.02.0/bin":$PATH
+```
+`.opam/` is usually in user's home directory.
+
+### 1.2 Compile the proofs
+
+Under the root folder of this repo, simply run
+```
+make -j6
+```
+to check all the coq proofs. Use a smaller process number if the compilation runs out of memory. The compilation may take a few hours.
+
+### 1.3 Proof Organization
+
+#### 1.3.1 Layering Refinement Proof
+
+The proof is organized as layers, one folder a layer (e.g. `proof/BaremoreService`). In each layer, we introduce new functions, define specifications for them, and prove the functions' implementation refine their specifications. Although we cannot release the C source code in this artifact, we provide the ASTs compiled from the C source code in each layer's `Code/` folder which are generated by the tool `clightgen` of `CompCert` project. The ASTs play the role of source code in our proof. The specifications of each layer are defined in `Specs/` folder. We do two-step simulation when proving code refines specifications. We first prove that the ASTs refine some intermediate specifications (in `LowSpecs/`), then prove the intermediate specifications refine the final specifications (in `Specs/`). The simulation proofs are in `CodeProof/` (Code Verification) and `RefProof/` (Refinement) respectively.
+
+The definition of the machine states shared by all layers is in [RData](proof/RData.v) and the bottom layer primitives are defined in [AbsAccessor](proof/AbsAccessor/Spec.v). A full list of layers is shown below:
+| #  | **Layer**               | **Source Code**        | **Specification**      | **Intermediate Specification** | **Code Verification**       | **Refinement**           |
+| -- | -----                   | -------------          | -----------------      | -----------            | -------------     | ----------               |
+|1|[BaremoreService](proof/BaremoreService/)|[Code](proof/BaremoreService/Code)|[Specs](proof/BaremoreService/Specs)|[LowSpecs](proof/BaremoreService/LowSpecs)|[CodeProof](proof/BaremoreService/CodeProof/)|[RefProof](proof/BaremoreService/RefProof/)|
+|2|[BaremoreHandler](proof/BaremoreHandler/)|[Code](proof/BaremoreHandler/Code)|[Specs](proof/BaremoreHandler/Specs)|[LowSpecs](proof/BaremoreHandler/LowSpecs)|[CodeProof](proof/BaremoreHandler/CodeProof/)|[RefProof](proof/BaremoreHandler/RefProof/)|
+|3|[BaremoreSMC](proof/BaremoreSMC/)|[Code](proof/BaremoreSMC/Code)|[Specs](proof/BaremoreSMC/Specs)|[LowSpecs](proof/BaremoreSMC/LowSpecs)|[CodeProof](proof/BaremoreSMC/CodeProof/)|[RefProof](proof/BaremoreSMC/RefProof/)|
+|4|[RmiAux](proof/RmiAux/)|[Code](proof/RmiAux/Code)|[Specs](proof/RmiAux/Specs)|[LowSpecs](proof/RmiAux/LowSpecs)|[CodeProof](proof/RmiAux/CodeProof/)|[RefProof](proof/RmiAux/RefProof/)|
+|5|[RmiAux2](proof/RmiAux2/)|[Code](proof/RmiAux2/Code)|[Specs](proof/RmiAux2/Specs)|[LowSpecs](proof/RmiAux2/LowSpecs)|[CodeProof](proof/RmiAux2/CodeProof/)|[RefProof](proof/RmiAux2/RefProof/)|
+|6|[RmiOps](proof/RmiOps/)|[Code](proof/RmiOps/Code)|[Specs](proof/RmiOps/Specs)|[LowSpecs](proof/RmiOps/LowSpecs)|[CodeProof](proof/RmiOps/CodeProof/)|[RefProof](proof/RmiOps/RefProof/)|
+|7|[RmiSMC](proof/RmiSMC/)|[Code](proof/RmiSMC/Code)|[Specs](proof/RmiSMC/Specs)|[LowSpecs](proof/RmiSMC/LowSpecs)|[CodeProof](proof/RmiSMC/CodeProof/)|[RefProof](proof/RmiSMC/RefProof/)|
+|8|[PSCIAux](proof/PSCIAux/)|[Code](proof/PSCIAux/Code)|[Specs](proof/PSCIAux/Specs)|[LowSpecs](proof/PSCIAux/LowSpecs)|[CodeProof](proof/PSCIAux/CodeProof/)|[RefProof](proof/PSCIAux/RefProof/)|
+|9|[PSCIAux2](proof/PSCIAux2/)|[Code](proof/PSCIAux2/Code)|[Specs](proof/PSCIAux2/Specs)|[LowSpecs](proof/PSCIAux2/LowSpecs)|[CodeProof](proof/PSCIAux2/CodeProof/)|[RefProof](proof/PSCIAux2/RefProof/)|
+|10|[PSCI](proof/PSCI/)|[Code](proof/PSCI/Code)|[Specs](proof/PSCI/Specs)|[LowSpecs](proof/PSCI/LowSpecs)|[CodeProof](proof/PSCI/CodeProof/)|[RefProof](proof/PSCI/RefProof/)|
+|11|[PSCIHandler](proof/PSCIHandler/)|[Code](proof/PSCIHandler/Code)|[Specs](proof/PSCIHandler/Specs)|[LowSpecs](proof/PSCIHandler/LowSpecs)|[CodeProof](proof/PSCIHandler/CodeProof/)|[RefProof](proof/PSCIHandler/RefProof/)|
+|12|[RVIC](proof/RVIC/)|[Code](proof/RVIC/Code)|[Specs](proof/RVIC/Specs)|[LowSpecs](proof/RVIC/LowSpecs)|[CodeProof](proof/RVIC/CodeProof/)|[RefProof](proof/RVIC/RefProof/)|
+|13|[RVIC2](proof/RVIC2/)|[Code](proof/RVIC2/Code)|[Specs](proof/RVIC2/Specs)|[LowSpecs](proof/RVIC2/LowSpecs)|[CodeProof](proof/RVIC2/CodeProof/)|[RefProof](proof/RVIC2/RefProof/)|
+|14|[RVIC3](proof/RVIC3/)|[Code](proof/RVIC3/Code)|[Specs](proof/RVIC3/Specs)|[LowSpecs](proof/RVIC3/LowSpecs)|[CodeProof](proof/RVIC3/CodeProof/)|[RefProof](proof/RVIC3/RefProof/)|
+|15|[RVIC4](proof/RVIC4/)|[Code](proof/RVIC4/Code)|[Specs](proof/RVIC4/Specs)|[LowSpecs](proof/RVIC4/LowSpecs)|[CodeProof](proof/RVIC4/CodeProof/)|[RefProof](proof/RVIC4/RefProof/)|
+|16|[PendingCheckAux](proof/PendingCheckAux/)|[Code](proof/PendingCheckAux/Code)|[Specs](proof/PendingCheckAux/Specs)|[LowSpecs](proof/PendingCheckAux/LowSpecs)|[CodeProof](proof/PendingCheckAux/CodeProof/)|[RefProof](proof/PendingCheckAux/RefProof/)|
+|17|[PendingCheck](proof/PendingCheck/)|[Code](proof/PendingCheck/Code)|[Specs](proof/PendingCheck/Specs)|[LowSpecs](proof/PendingCheck/LowSpecs)|[CodeProof](proof/PendingCheck/CodeProof/)|[RefProof](proof/PendingCheck/RefProof/)|
+|18|[CtxtSwitchAux](proof/CtxtSwitchAux/)|[Code](proof/CtxtSwitchAux/Code)|[Specs](proof/CtxtSwitchAux/Specs)|[LowSpecs](proof/CtxtSwitchAux/LowSpecs)|[CodeProof](proof/CtxtSwitchAux/CodeProof/)|[RefProof](proof/CtxtSwitchAux/RefProof/)|
+|19|[CtxtSwitch](proof/CtxtSwitch/)|[Code](proof/CtxtSwitch/Code)|[Specs](proof/CtxtSwitch/Specs)|[LowSpecs](proof/CtxtSwitch/LowSpecs)|[CodeProof](proof/CtxtSwitch/CodeProof/)|[RefProof](proof/CtxtSwitch/RefProof/)|
+|20|[RealmTimerHandler](proof/RealmTimerHandler/)|[Code](proof/RealmTimerHandler/Code)|[Specs](proof/RealmTimerHandler/Specs)|[LowSpecs](proof/RealmTimerHandler/LowSpecs)|[CodeProof](proof/RealmTimerHandler/CodeProof/)|[RefProof](proof/RealmTimerHandler/RefProof/)|
+|21|[RealmSyncHandlerAux](proof/RealmSyncHandlerAux/)|[Code](proof/RealmSyncHandlerAux/Code)|[Specs](proof/RealmSyncHandlerAux/Specs)|[LowSpecs](proof/RealmSyncHandlerAux/LowSpecs)|[CodeProof](proof/RealmSyncHandlerAux/CodeProof/)|[RefProof](proof/RealmSyncHandlerAux/RefProof/)|
+|22|[RealmSyncHandler](proof/RealmSyncHandler/)|[Code](proof/RealmSyncHandler/Code)|[Specs](proof/RealmSyncHandler/Specs)|[LowSpecs](proof/RealmSyncHandler/LowSpecs)|[CodeProof](proof/RealmSyncHandler/CodeProof/)|[RefProof](proof/RealmSyncHandler/RefProof/)|
+|23|[RealmExitHandlerAux](proof/RealmExitHandlerAux/)|[Code](proof/RealmExitHandlerAux/Code)|[Specs](proof/RealmExitHandlerAux/Specs)|[LowSpecs](proof/RealmExitHandlerAux/LowSpecs)|[CodeProof](proof/RealmExitHandlerAux/CodeProof/)|[RefProof](proof/RealmExitHandlerAux/RefProof/)|
+|24|[RealmExitHandler](proof/RealmExitHandler/)|[Code](proof/RealmExitHandler/Code)|[Specs](proof/RealmExitHandler/Specs)|[LowSpecs](proof/RealmExitHandler/LowSpecs)|[CodeProof](proof/RealmExitHandler/CodeProof/)|[RefProof](proof/RealmExitHandler/RefProof/)|
+|25|[RunAux](proof/RunAux/)|[Code](proof/RunAux/Code)|[Specs](proof/RunAux/Specs)|[LowSpecs](proof/RunAux/LowSpecs)|[CodeProof](proof/RunAux/CodeProof/)|[RefProof](proof/RunAux/RefProof/)|
+|26|[RunComplete](proof/RunComplete/)|[Code](proof/RunComplete/Code)|[Specs](proof/RunComplete/Specs)|[LowSpecs](proof/RunComplete/LowSpecs)|[CodeProof](proof/RunComplete/CodeProof/)|[RefProof](proof/RunComplete/RefProof/)|
+|27|[RunLoop](proof/RunLoop/)|[Code](proof/RunLoop/Code)|[Specs](proof/RunLoop/Specs)|[LowSpecs](proof/RunLoop/LowSpecs)|[CodeProof](proof/RunLoop/CodeProof/)|[RefProof](proof/RunLoop/RefProof/)|
+|28|[RunSMC](proof/RunSMC/)|[Code](proof/RunSMC/Code)|[Specs](proof/RunSMC/Specs)|[LowSpecs](proof/RunSMC/LowSpecs)|[CodeProof](proof/RunSMC/CodeProof/)|[RefProof](proof/RunSMC/RefProof/)|
+|29|[TableAux](proof/TableAux/)|[Code](proof/TableAux/Code)|[Specs](proof/TableAux/Specs)|[LowSpecs](proof/TableAux/LowSpecs)|[CodeProof](proof/TableAux/CodeProof/)|[RefProof](proof/TableAux/RefProof/)|
+|30|[TableAux2](proof/TableAux2/)|[Code](proof/TableAux2/Code)|[Specs](proof/TableAux2/Specs)|[LowSpecs](proof/TableAux2/LowSpecs)|[CodeProof](proof/TableAux2/CodeProof/)|[RefProof](proof/TableAux2/RefProof/)|
+|31|[TableAux3](proof/TableAux3/)|[Code](proof/TableAux3/Code)|[Specs](proof/TableAux3/Specs)|[LowSpecs](proof/TableAux3/LowSpecs)|[CodeProof](proof/TableAux3/CodeProof/)|[RefProof](proof/TableAux3/RefProof/)|
+|32|[TableWalk](proof/TableWalk/)|[Code](proof/TableWalk/Code)|[Specs](proof/TableWalk/Specs)|[LowSpecs](proof/TableWalk/LowSpecs)|[CodeProof](proof/TableWalk/CodeProof/)|[RefProof](proof/TableWalk/RefProof/)|
+|33|[TableDataOpsIntro](proof/TableDataOpsIntro/)|[Code](proof/TableDataOpsIntro/Code)|[Specs](proof/TableDataOpsIntro/Specs)|[LowSpecs](proof/TableDataOpsIntro/LowSpecs)|[CodeProof](proof/TableDataOpsIntro/CodeProof/)|[RefProof](proof/TableDataOpsIntro/RefProof/)|
+|34|[TableDataOpsRef1](proof/TableDataOpsRef1/)|[Code](proof/TableDataOpsRef1/Code)|[Specs](proof/TableDataOpsRef1/Specs)|[LowSpecs](proof/TableDataOpsRef1/LowSpecs)|[CodeProof](proof/TableDataOpsRef1/CodeProof/)|[RefProof](proof/TableDataOpsRef1/RefProof/)|
+|35|[TableDataOpsRef2](proof/TableDataOpsRef2/)|[Code](proof/TableDataOpsRef2/Code)|[Specs](proof/TableDataOpsRef2/Specs)|[LowSpecs](proof/TableDataOpsRef2/LowSpecs)|[CodeProof](proof/TableDataOpsRef2/CodeProof/)|[RefProof](proof/TableDataOpsRef2/RefProof/)|
+|36|[TableDataOpsRef3](proof/TableDataOpsRef3/)|[Code](proof/TableDataOpsRef3/Code)|[Specs](proof/TableDataOpsRef3/Specs)|[LowSpecs](proof/TableDataOpsRef3/LowSpecs)|[CodeProof](proof/TableDataOpsRef3/CodeProof/)|[RefProof](proof/TableDataOpsRef3/RefProof/)|
+|37|[TableDataSMC](proof/TableDataSMC/)|[Code](proof/TableDataSMC/Code)|[Specs](proof/TableDataSMC/Specs)|[LowSpecs](proof/TableDataSMC/LowSpecs)|[CodeProof](proof/TableDataSMC/CodeProof/)|[RefProof](proof/TableDataSMC/RefProof/)|
+|38|[SMCHandler](proof/SMCHandler/)|[Code](proof/SMCHandler/Code)|[Specs](proof/SMCHandler/Specs)|[LowSpecs](proof/SMCHandler/LowSpecs)|[CodeProof](proof/SMCHandler/CodeProof/)|[RefProof](proof/SMCHandler/RefProof/)|
+|39|[RMMHandler](proof/RMMHandler/)|[Code](proof/RMMHandler/Code)|[Specs](proof/RMMHandler/Specs)|[LowSpecs](proof/RMMHandler/LowSpecs)|[CodeProof](proof/RMMHandler/CodeProof/)|[RefProof](proof/RMMHandler/RefProof/)|
+
+- Mover Oracle related definitions can be found in [MoverTypes](proof/MoverTypes.v). The proof that refines page table operations into atomic specifications can be found in the consecutive layers [TableDataOpsRef1](proof/TableDataOpsRef1/), [TableDataOpsRef2](proof/TableDataOpsRef2/), [TableDataOpsRef3](proof/TableDataOpsRef3/).
+
+- Most permutation conditions are checked during layer refinement proof, except for MEMORY-ISOLATION condition which is one of the invariant checked in security proof below.
+
+- Assembly code related definitions and proofs are in [Assembly](proof/Assembly/), including:
+  - Assembly language semantics definition [Asm](proof/Assembly/Asm.v)
+  - Coq representation of the proved assembly code [AsmCode](proof/Assembly/AsmCode.v)
+  - The specification of assembly code [AsmSpec](proof/Assembly/AsmSpec.v)
+  - Proving assembly code refines its specification [AsmProof](proof/Assembly/AsmProof.v), [AsmProof2](proof/Assembly/AsmProof2.v).
+
+#### 1.3.2 Security Proof
+
+Above the top layer [RMMHandler](proof/RMMHandler/), we compose the final security proof in [Security](proof/Security/).
+- The Ideal machine's definition can be found in [SecureMachine](proof/Security/SecureMachine.v).
+- The simulation relation between Ideal machine and Real machine can be found in [RefRel](proof/Security/RefRel.v).
+- The proof showing that Realms' and Hypervisors' execution preserves simulation relation can be found in [SecureProofUser](proof/Security/SecureProofUser.v).
+- The proof showing that RMM handler preserves simulation relation can be found in [SecureProofRMM1](proof/Security/SecureProofRMM1.v) and [SecureProofRMM2](proof/Security/SecureProofRMM2.v).
+
 ## 2. Performance Evaluation
 
 ### 2.0 Prelogue