Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy languages and access control systems, verifying that such systems enforce the desired invariants is recognized as a security problem of crucial importance. In the present paper, we develop a framework for the formal verification of grsecurity, an access control system developed on top of Unix/Linux systems. The verification problem in grsecurity presents much of the complexity of modern RBAC systems, due to the presence of policy state changes that may arise both from explicit administrative primitives supported by grsecurity, and as the result of the interaction with the underlying operating system facilities. We develop a formal semantics for grsecurity’s RBAC system, based on a labelled transition system, and a sound abstraction of that semantics providing a bounded approximation, amenable to model checking. We report on the result of the experimental analysis conducted with gran, the model checker we implemented based on our abstract semantics, on existing public servers running grsecurity to implement their RBAC systems.

Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy languages and access control systems, verifying that such systems enforce the desired invariants is recognized as a security problem of crucial importance. In the present paper, we develop a framework for the formal verification of grsecurity, an access control system developed on top of Unix/Linux systems. The verification problem in grsecurity presents much of the complexity of modern RBAC systems, due to the presence of policy state changes that may arise both from explicit administrative primitives supported by grsecurity, and as the result of the interaction with the underlying operating system facilities. We develop a formal semantics for grsecurity's RBAC system, based on a labelled transition system, and a sound abstraction of that semantics providing a bounded approximation, amenable to model checking. We report on the result of the experimental analysis conducted with gran, the model checker we implemented based on our abstract semantics, on existing public servers running grsecurity to implement their RBAC systems. © 2012, Daniel Hedin.

Gran: model checking grsecurity RBAC policies

BUGLIESI, Michele;CALZAVARA, STEFANO;FOCARDI, Riccardo;SQUARCINA, MARCO
2012

Abstract

Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy languages and access control systems, verifying that such systems enforce the desired invariants is recognized as a security problem of crucial importance. In the present paper, we develop a framework for the formal verification of grsecurity, an access control system developed on top of Unix/Linux systems. The verification problem in grsecurity presents much of the complexity of modern RBAC systems, due to the presence of policy state changes that may arise both from explicit administrative primitives supported by grsecurity, and as the result of the interaction with the underlying operating system facilities. We develop a formal semantics for grsecurity’s RBAC system, based on a labelled transition system, and a sound abstraction of that semantics providing a bounded approximation, amenable to model checking. We report on the result of the experimental analysis conducted with gran, the model checker we implemented based on our abstract semantics, on existing public servers running grsecurity to implement their RBAC systems.
Proceedings 2012 IEEE 25th Computer Security Foundations Symposium CSF 2012
File in questo prodotto:
File Dimensione Formato  
cfs12-gran.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 201.08 kB
Formato Adobe PDF
201.08 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/39019
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 8
social impact