Formal Modeling and Security Analysis for Intra-level Privilege Separation.

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. In this paper, we introduce a general and extensible formal framework based on a privilege-centric model (PCM) and define the security properties that should be satisfied by intra-level privilege separation. We then instantiate two models using the B-method: Nested Kernel and Hilps, which utilize x86 WP and AArch64 TxSZ mechanisms, respectively. Their security is verified by model checking in ProB. The machine-checked analysis shows that our approach can not only effectively detect design errors and attacks, but also guide future system design.