Artifact Readme

The artifact includes the evaluation artifacts of Spoq3, which contains the verification targets: TF-A, RMM, SeKVM, and Komodo. The artifact is packaged in a docker image for easy setup and reproducibility.

Get Started

• Download the docker image file provided in the repo 'spoq2_artifact.tar'
• Run the following command to load image and start a container:

  docker load -i spoq2_artifact.tar
  docker run -it spoq2 bash
  

File Structure

/opt/spoq2/src/: The source code of Spoq2.

/opt/spoq2/spoq2-artifacts/: The evaluation artifacts of Spoq2, including TF-A, RMM, SeKVM, and Komodo.

/opt/spoq2/spoq2-artifacts/tfa/: The evaluation artifact of TF-A.

/opt/spoq2/spoq2-artifacts/rmm-pa/: The evaluation artifact of RMM.

/opt/spoq2/spoq2-artifacts/sekvm-6.1/: The evaluation artifact of SeKVM.

/opt/spoq2/spoq2-artifacts/tpot/komodo-serval: The evaluation artifact of Komodo.

The evaluation files include the configuration files of the verification targets: TF-A, RMM, SeKVM, Komodo, and the scripts to run the end-to-end verification.

Run the verification End-to-End

Run TF-A verification

• Navigate to the target directory, e.g., cd /opt/spoq2/spoq2-artifacts/tfa/
• Run the script run.py to start the verification:

  python3 run.py
  

• The verification results will be printed in the terminal.

Run RMM verification

• Navigate to the target directory, e.g., cd /opt/spoq2/spoq2-artifacts/rmm-pa/
• Run the script run.py to start the verification:

  python3 run.py
  

• The verification results will be printed in the terminal.

Run SeKVM verification

• Navigate to the target directory, e.g., cd /opt/spoq2/spoq2-artifacts/sekvm-6.1/
• Run the script run.py to start the verification:

  python3 run.py
  

• The verification results will be printed in the terminal.

Run Komodo verification

• Navigate to the target directory, e.g., cd /opt/spoq2/spoq2-artifacts/tpot/komodo-serval/
• Run the script run.py to start the verification:

  python3 run.py
  

• The verification results will be printed in the terminal.

Reproducing Results in Table 2

The run.py scripts in each artifact directory are configured to reproduce the results in Table 2 of the paper by default. It will print the verification time for security proof and safety proofs separately.

Ablation Studies

To disable optimizations, we include flags for the script to indicate which optimizations to disable.

To run the ablation studies, use the command python3 run.py --variant <n>, where n is from 1 to 6, representing different ablation settings as follows:

--variant 1: All optimizations enabled (default setting).

--variant 2: Disable COI optimization.

--variant 3: Disable Path Pruning Mentioned in Section 5.2.

--variant 4: Diable Clauses Pruning Mentioned in Section 5.3.

--variant 5: Disable Caches.

--variant 6: Disable All Optimizations.

Reproducing Ablation Results in Figure 10

We have prepared a script that run all of the ablation settings and collect results automatically. To run the script, use the following command at /opt/spoq2/spoq2-artifacts/ level: ./ablations.sh. The script will run all ablation settings and collect the results in a CSV file and finally generate a comparison figure.