Principled Symbolic Validation of Enclaves on Low-End Microcontrollers

Recent advancements in trusted execution environments (TEEs) provide strong isolation guarantees for hardware-protected enclaves within a shared address space. The advent of commercial solutions like Intel SGX on high-end processors has spurred a growing open-source ecosystem of enclave shielding runtimes, along with research into symbolic execution tools for detecting elusive interface sanitization bugs. However, despite their inherent similarities and shared vulnerabilities, automated validation of enclaves on low-end embedded platforms remains largely unexplored. This paper ports Pandora, a symbolic execution tool originally designed for principled validation of high-end Intel SGX enclaves, to the Sancus research TEE for 16-bit MSP430 microcontrollers. We introduce a TEE hardware abstraction layer and extend Pandora's symbolic memory model to support non-contiguous Sancus enclaves. Our evaluation across different runtimes and applications within the Sancus ecosystem demonstrates that Pandora autonomously re-discovers vulnerabilities that were manually patched over the last decade. Our work lays the foundation for automated validation of heterogenous enclaves and outlines directions for future work on interruptibility, real-time guarantees, and extensions to alternative MSP430 TEEs.