Formal Modeling and Security Analysis for Intra-level Privilege Separation
Yinggang Guo, Zicheng Wang, Bingnan Zhong, Qingkai Zeng · 2022
Privileged system software such as mainstream operating system kernels and hypervisors have an ongoing stream of vulnerabilities. Even the inflated secure world in Trusted Execution Environment (TEE) is no longer secure in complex real-world scenarios. Since higher privilege levels cannot always be stacked to provide protection, intra-level privilege separation has become a powerful way to build trustworthy systems. However, existing intra-level privilege separation systems lack sound security analysis and cannot give formal guarantees.