Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy specifications arising from system administrators' needs, formally verifying that access control systems enforce some defined security invariants is a problem of crucial importance. In a previous work which has been accepted for presentation at IEEE CSF 2012, we developed a framework for the formal verification of Grsecurity RBAC, an access control system developed on top of Unix/Linux systems. In this thesis we improve the framework by considering the interaction with the underlying operating system. This refinement allows for a reduction in the number of transitions within the labelled transition systems resulting from policies. Additionally, we deal with the problem of automatic verification of Grsecurity RBAC policies by defining a set of security invariants. Based on our abstract semantics, we implement Granalyze, a model checker that accounts for the verification of real policies. We report on the results of the experimental analysis conducted using the tool on existing public servers running Grsecurity RBAC.

Granalyze: towards the automatic verification of Grsecurity RBAC policies

Squarcina, Marco
2014/2015

Abstract

Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy specifications arising from system administrators' needs, formally verifying that access control systems enforce some defined security invariants is a problem of crucial importance. In a previous work which has been accepted for presentation at IEEE CSF 2012, we developed a framework for the formal verification of Grsecurity RBAC, an access control system developed on top of Unix/Linux systems. In this thesis we improve the framework by considering the interaction with the underlying operating system. This refinement allows for a reduction in the number of transitions within the labelled transition systems resulting from policies. Additionally, we deal with the problem of automatic verification of Grsecurity RBAC policies by defining a set of security invariants. Based on our abstract semantics, we implement Granalyze, a model checker that accounts for the verification of real policies. We report on the results of the experimental analysis conducted using the tool on existing public servers running Grsecurity RBAC.
2014-06-26
File in questo prodotto:
File Dimensione Formato  
814359-1173426.pdf

accesso aperto

Tipologia: Altro materiale allegato
Dimensione 876.18 kB
Formato Adobe PDF
876.18 kB Adobe PDF Visualizza/Apri

I documenti in UNITESI 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: https://hdl.handle.net/20.500.14247/22598