This paper presents a formal model, called SELAC, for analyzing an arbitrary security policy configuration for the SELinux system. A security policy for SELinux is complex and large: it is made by many configuration rules that refer to the access control sub-models implemented in the system. Among the rules composing a security policy configuration, many relationships occur and it is extremely difficult to understand their overall effects in the system. Our aim is to define semantics for the constructs of the SELinux configuration language and to model the relationships occurring among sets of configuration rules. Finally, we develop an algorithm based upon SELAC, which can verify whether, given an arbitrary security policy configuration, a given subject can access a given object in a given mode.
Towards a Formal Model for Security Policies Specification and Validation in the SELinux system / Zanin, G; Mancini, Luigi Vincenzo. - STAMPA. - (2004), pp. 136-145. (Intervento presentato al convegno 9th ACM Symposium on Access control models and technologies tenutosi a IBM, Yorktown Heights, USA nel June 2004) [10.1145/990036.990059].
Towards a Formal Model for Security Policies Specification and Validation in the SELinux system
MANCINI, Luigi Vincenzo
2004
Abstract
This paper presents a formal model, called SELAC, for analyzing an arbitrary security policy configuration for the SELinux system. A security policy for SELinux is complex and large: it is made by many configuration rules that refer to the access control sub-models implemented in the system. Among the rules composing a security policy configuration, many relationships occur and it is extremely difficult to understand their overall effects in the system. Our aim is to define semantics for the constructs of the SELinux configuration language and to model the relationships occurring among sets of configuration rules. Finally, we develop an algorithm based upon SELAC, which can verify whether, given an arbitrary security policy configuration, a given subject can access a given object in a given mode.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.