Verifying information flow goals in Security-Enhanced Linux

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

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer security 2005-01, Vol.13 (1), p.115-134
Main Authors: Guttman, Joshua D., Herzog, Amy L., Ramsdell, John D., Skorupka, Clement W.
Format: Article
Language:English
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0926-227X
1875-8924
DOI:10.3233/JCS-2005-13105