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 your opam 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 your system PATH, or add it manually:
export PATH="path/to/.opam/4.02.0/bin":$PATH
.opam/ is usually in your home folder.
In the root folder of this repo, simply run
make -j6
to check all the coq proof. Use a smaller process number if the compilation runs out of memory. The compilation may take a few hours.
The proofs are organized as below:
root/
theorem2/ --- Theorem 2: when the kernel runs in isolation
theorem4/ --- Theorem 4: when the kernel runs with user codes
sekvm/
wDRF/ --- Proofs that SeKVM satisfies the wDRF conditions
Security/ --- Security proof of SeKVM
{PTAlloc,PTWalk,...}/ --- Security-preserving layers
certikos/ --- CertiKOS proof framework (pre-compiled binary)