Systematic Policy Analysis for High-Assurance Services in SELinux

Identifying and protecting the trusted computing base (TCB) of a system is an important task to provide high- assurance services since a set of trusted subjects should be legitimately articulated for target applications. In this paper, we present a formal policy analysis framework to identify TCB with the consideration of specific security goals. We also attempt to model information flows between domains in SELinux policies and detect security violations among information flows using colored Petri nets.