A Formally Verified Secure Caching Mechanism on TrustZone-enabled Microcontrollers

Trusted Execution Environments (TEEs) on resource-constrained microcontrollers are an emerging area of interest, yet they present unique security challenges, particularly in managing encrypted code execution through limited secure memory. This paper presents a formal verification approach for Umbra, a TEE framework for ARM TrustZone-M, currently under development, that implements secure caching mechanisms to execute encrypted enclaves from flash memory. We employ model checking tech- niques to formally analyze critical security properties, including data isolation between secure and non-secure worlds, integrity of the Enclave Flash Block Cache (EFBC), and resilience against identified threats such as Direct Memory Access (DMA) handover attacks and timing-based side channels. Our threat model consid- ers privileged attackers in the non-secure world and compromised host operating systems, analyzing vulnerabilities in DMA recon- figuration windows and context switch dependencies. Through formal modeling, we identify replay and timing side-channel attacks; by introducing countermeasures, these guarantees are restored in the model.