Gran: Model Checking Grsecurity RBAC Policies

—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 abstraction of that semantics providing a bounded approximation, amenable to model checking. We report on the result of the experimenta...

• Type: Journal
• Year: 2012
• Where: CSFW
• Authors: Michele Bugliesi, Stefano Calzavara, Riccardo Focardi, Marco Squarcina
• Keywords: Abstract Semantics, CSFW 2012, Formal Semantics, Role Based Access Control, Security Privacy