0tcb / tap

Directory Structure

The are three top-level directories:

• AbstractPlatform (The TAP)
• Sanctum (Sanctum Model)
• SGX (SGX model).

Setup

First, you will need to install boogie. You'll also need to set the BOOGIE environment variable to point to the boogie executable on your system. For example, I set it as follows:

$ export BOOGIE="mono ~/research/verification/boogie/Binaries/Boogie.exe"

Abstract Trusted Platform

The trusted abstract platform (TAP) is in AbstractPlatform.

Running The TAP Proofs

$ cd AbstractPlatform
$ make

Don't forget to set $BOOGIE

Refinement Proofs

The code is in SanctumRefinementProof.bpl and SGXRefinementProof.bpl.

Running the Refinement Proofs.

Just run make!

Sanctum Model

Sanctum contains all of the Sanctum model.

• Sanctum/Common defines common, types, constants and functions.
• Sanctum/Host/OS.bpl contains functions that would be implemented in the operating system.
• Sanctum/MMU contains the MMU. See below for details.
• Sanctum/Sanctum contains the Sanctum model and non-interference proofs.

Executing the Proofs

To run all proofs for the Sanctum model (including the MMU proof), just run make in Sanctum.

$ cd Sanctum
$ make

Running all the proofs may take several minutes. (There are a couple of extra proofs that aren't mentioned in the paper here.)

SGX Model

The SGX model is in SGX. There is nothing to run here.

tap's Issues

make error

Hello, when I run make in AbstractPlatform, I encounter the following error messages.

"/z3opt:smt.RELEVANCY=0 /z3opt:smt.CASE_SPLIT=0 /errorLimit:1 /xml:build/CPU.xml Types.bpl ../Common/Types.bpl ../Common/Common.bpl ../Common/Cache.bpl CPU.bpl CPUImpl.bpl
/bin/sh: 1: /z3opt:smt.RELEVANCY=0: not found
Makefile:39: recipe for target 'build/CPU.xml' failed
make: *** [build/CPU.xml] Error 127"

How could address this problem?

I set $BOOGIE and I use Boogie with version 2.3.0.61016 which works well with other bpl files.

Code about the adversary model

I have no problem now

make error for SGX folder and AbstractPlatform folder

Hello, I am trying to execute makefile in SGX folder, but I meet this error:

yue@ubuntu:~/TAP$ cd SGX
yue@ubuntu:~/TAP/SGX$ export BOOGIE="mono ~/boogie/Binaries/Boogie.exe"
yue@ubuntu:~/TAP/SGX$ ls
Hardware Makefile Proof.bpl
yue@ubuntu:~/TAP/SGX$ make

mono ~/boogie/Binaries/Boogie.exe /xml:build/SGXProof.xml /z3opt:smt.RELEVANCY=0 /z3opt:smt.CASE_SPLIT=0 /errorLimit:1 Hardware/sgx.bpl Proof.bpl
[ERROR] FATAL UNHANDLED EXCEPTION: System.IO.DirectoryNotFoundException: Could not find a part of the path "/home/yue/TAP/SGX/build/SGXProof.xml".
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.Boolean anonymous, System.IO.FileOptions options) [0x00164] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.IO.FileOptions options) [0x00000] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.Boolean useAsync) [0x00000] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at (wrapper remoting-invoke-with-check) System.IO.FileStream..ctor(string,System.IO.FileMode,System.IO.FileAccess,System.IO.FileShare,int,bool)
  at System.Xml.XmlWriterSettings.CreateWriter (System.String outputFileName) [0x00051] in <4a776760e559455ead15edf260db6599>:0 
  at System.Xml.XmlWriter.Create (System.String outputFileName, System.Xml.XmlWriterSettings settings) [0x0000a] in <4a776760e559455ead15edf260db6599>:0 
  at Microsoft.Boogie.XmlSink.Open () [0x0002d] in <b8387f4c32184b3fb265854e480fe328>:0 
  at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) [0x00081] in <eedaca8a21cb4887bb5e5eb3b461f942>:0 
Makefile:8: recipe for target 'build/SGXProof.xml' failed
make: *** [build/SGXProof.xml] Error 1
yue@ubuntu:~/TAP/SGX$ mono ~/boogie/Binaries/Boogie.exe
*** Error: No input files were specified.

Similarly, I get an error when I try to execute makefile in AbstractPlatform folder, which shows as below:

yue@ubuntu:~/TAP/AbstractPlatform$ make

mono ~/boogie/Binaries/Boogie.exe /z3opt:smt.RELEVANCY=0 /z3opt:smt.CASE_SPLIT=0 /errorLimit:1  /xml:build/CacheConfidentialityProof.xml Types.bpl ../Common/Types.bpl ../Common/Common.bpl ../Common/Cache.bpl CPU.bpl ConfidentialityProof.bpl ProofCommon.bpl CacheConfidentialityProof.bpl
Boogie program verifier version 2.4.1.10503, Copyright (c) 2003-2014, Microsoft.
*** Error: '/z3opt:smt.RELEVANCY=0': Filename extension '.relevancy=0' is not supported. Input files must be BoogiePL programs (.bpl).
Makefile:48: recipe for target 'build/CacheConfidentialityProof.xml' failed
make: *** [build/CacheConfidentialityProof.xml] Error 

I would appreciate it if you could give me any hints about the solutions to these bugs.
Thanks for your attention.