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 techniques 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 considers privileged attackers in the non-secure world and compromised host operating systems, analyzing vulnerabilities in DMA reconfiguration 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.