A Formal Approach to Multi-Layered Privileges for Enclaves

—Trusted Execution Environments (TEE) have been widely adopted as a protection approach for security-critical applications. Although feature extensions have been previously proposed to improve the usability of enclaves, their provision patterns are still confronted with security challenges. This paper presents P ALANT ´ IR , a verifiable multi-layered inter-enclave privilege model for secure feature extensions to enclaves. Specifically, a parent-children inter-enclave relationship, with which a parent enclave is granted two privileged permissions, the Execution Control and Spatial Control, over its children enclaves to facilitate secure feature extensions, is introduced. Moreover, by enabling nesting parent-children relationships, P ALANT ´ IR achieves multi-layered privileges (MLP) that allow feature extensions to be placed in various privilege layers following the Principle of Least Privilege. To prove the security of P ALANT ´ IR , we verified that our privilege model does not break or weaken the security guarantees of enclaves by building and verifying a formal model named TAP ∞ . Furthermore, We implemented a prototype of P ALANT ´ IR on P ENGLAI , an open-sourced RISC-V TEE platform. The evaluation demonstrates the promising performance of P ALANT ´ IR in runtime overhead ( < 5%) and startup latencies.