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 pa- per, we present a formal policy analysis framework to iden- tify TCB with the consideration of specific security goals. We also attempt to model information flows between do- mains in SELinux policies and detect security violations among information flows using Colored Petri Nets.