Verifying information flow goals in Security-Enhanced Linux

Issue title: WITS'03

Guest editors: Roberto Gorrieri

Article type: Research Article

Authors: Guttman, Joshua D. | Herzog, Amy L. | Ramsdell, John D. | Skorupka, Clement W.

Affiliations: The MITRE Corporation, USA. E-mail: guttman@mitre.org, aherzog@mitre.org, ramsdell@mitre.org, ragnor@mitre.org

Abstract: In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.

Keywords: Operating system security, information flow, Security-Enhanced Linux, temporal logic, model checking

DOI: 10.3233/JCS-2005-13105

Journal: Journal of Computer Security, vol. 13, no. 1, pp. 115-134, 2005