$\text{TAP}^{\lambda}$

This document is provided by Anonymous Author @ Apr 29, 2024.

Intro

This model provides an extended Trusted Abstract Platform (TAP) model with the newly proposed Privileged Enclave and Multi-Layered Privilege prototype.

In this project. the Secure Measurement, Integrity, and Confidentiality (which are decompositions of SRE property) are proved to be maintained in the extended model.

Setup

Install Boogie 2.16.0 on your platform (dotnet is recommended), and export boogie to your environment variables.

// Update your apt package.
wget https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
sudo dpkg -i packages-microsoft-prod.deb
rm packages-microsoft-prod.deb

// Install .NET 6.0 & Z3
sudo apt-get update && \ sudo apt-get install -y dotnet-sdk-6.0 aspnetcore-runtime-6.0 z3

// Install boogie 2.16
dotnet tool install --global boogie --version 2.16

// Add Boogie toolchains to your environment variables. (optional)
export PATH=$PATH:$HOME/.dotnet/tools/

Run

$ cd AbstractPlatform
$ make clean && make all

Debug / Develop / Detailed Info

To get elaborated messages about the model, do these things:

Use the make-object with the _dbg postfix.
Do:
```
cd AbstractPlatform   
mkdir dotfiles
make clean && make <whatever-you-like> && make cut
```
The LOWER/UPPERLEVELOPT_DBG flag and cut object in Makefile helps you to generate numerous valuable messages, including intermediate code, backend Z3 SMTs, counterexamples, execution times, and so forth.

arxgy/TAP-lambda

$\text{TAP}^{\lambda}$

Intro

Setup

Run

Debug / Develop / Detailed Info