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 PALANTR, 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, PALANTR achieves multilayered privileges (MLP) that allow feature extensions to be placed in various privilege layers following the Principle of Least Privilege.To prove the security of PALANTR, 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 PALANTR on PENGLAI, an open-sourced RISC-V TEE platform.The evaluation demonstrates the promising performance of PALANTR in runtime overhead (< 5%) and startup latencies.