[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
***Wednesday, March 10, 2004***  NOTE CORRECTED DATE
306 Egan  Hall, Northeastern University
    (building 60 on http://www.campusmap.neu.edu/)  
1145-145. Bring your lunch.

Joshua Guttman

Mitre Corporation

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

(Workshop on Issues in the Theory of Security, April '03, and
Journal of Computer Security, Forthcoming.) 

Joint work with Amy L. Herzog and John D. Ramsdell .

Upcoming Events:

Volunteers are needed for 3/17 et seq

--Mitch