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 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.

1 Introduction

Determining whether a system can be trusted or not is a critical problem in systems and network management. Particularly for security reasons, a local or remote system administrator typically needs to verify if a system meets information security objectives, such as integrity, confidentiality, and availability requirements. For example, in order to deploy applications in distributed and collaborative computing environments, one machine may need to check if another machine currently runs a known good version of an application software on a well-configured, trusted operating system. Otherwise, a remote machine may run buggy or malicious application codes, or may be improperly configured such that the trusted application can be corrupted by untrustful programs or users. Supporting such an important assurance feature with comprehensive security analysis is necessary to trust a target system based on its current security configurations and policies.