Sample Enclave Programs for the MSP430-Sancus TEE

This directory contains the unit tests and evaluation case studies for the Pandora port to the Sancus research TEE for embedded 16-bit MSP430 microcontrollers. The hardware-abstraction layer and SancusSDK enclave loader have been integrated into the upstream Pandora repository.

More details can be found in Gert-Jan Goossens's Msc thesis and our SysTEX'25 paper:

@inproceedings{goossens2025principled,
    title     = {Principled Symbolic Validation of Enclaves on Low-End Microcontrollers},
    author    = {Goossens, Gert-Jan and Van Bulck, Jo},
    booktitle = {8th Workshop on System Software for Trusted Execution {(SysTEX)}},
    publisher = {{IEEE}},
    month     = Jun,
    year      = 2025,
}

Directory Structure

• cfsan: Hand-crafted assembly test enclaves for control-flow sanitization vulnerabilities (cf. paper §A.1)
• ptrsan: Hand-crafted assembly test enclaves for pointer sanitization vulnerabilities (cf. paper §A.2)
• full_encl: Sample enclaves written in C, including compiler-generated runtime entry/exit stubs (cf. paper §4.2)
• t2w: Reproduction of known vulnerabilities in Sancus applications and support libraries, discovered in the prior Tale of 2 Worlds paper (cf. paper §4.3)

Reproduction

Dependencies

Detailed instructions for installing Pandora and all its dependencies in a Python virtual environment are provided below. This guide assumes you have a machine with the following specifications:

• Python v3.12 or higher
• x86-64 architecture: The msp430-objdump binary binary shipped with Pandora is currently only included for Intel/AMD x86. Replacing this binary with a compatible ARM binary was not tested, but should in principle be sufficient to support running Pandora-MSP430 on ARM hosts.

Note (Pandora/angr versions). The evaluation in the SysTEX'25 paper was tested to work with pandora (commit 34ded2e) and angr-platforms (commit ee1b6d9).

Symbolic Validation

💡 Symbolic validation of the test cases is ensured in the CI/CD pipeline (see GitHub Actions output).

Support for symbolically validating Sancus enclaves has been fully upstreamed in the Pandora repository.

All directories contain, the source code (main.c, foo.S), compiled binary (main.elf), and relevant HTML reports generated by Pandora.

Proceed as follows to run Pandora on the example enclaves yourself:

# clone upstream repos
$ git clone https://github.com/pandora-tee/pandora && cd pandora
$ git clone https://github.com/angr/angr-platforms

# create Python virtual environment
$ sudo python3 -m venv venv && source ./venv/bin/activate

# install dependencies in virtual environment
(venv) $ python3 -m pip install -r requirements.txt && cd angr-platforms && python3 -m pip install . && cd ..

# now run pandora on a selected Sancus testcase
(venv) $ ./pandora.py run -n 30 -p ptr,cf --pandora-option PANDORA_EXPLORE_STACK_DEPTH=1500 /path/to/pandora-examples/sancus/testcase/main.elf

After Pandora successfully finished, you should see a summary in the console and human-readable HTML reports in the current directory.

Compiling and Running

⚠️ This step is not needed to reproduce the results in the paper, as we provide precompiled binaries in this repository.

💡 Compilation of the test cases is ensured in the CI/CD pipeline (see GitHub Actions output).

If desired, the test cases can be compiled using the Sancus compiler and ran in the cycle-accurate, openMSP430-based Sancus simulator.