A formal model and correctness proof for an access control policy framework
Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL titulado A formal model and correctness proof for an access control policy framework.
Sus autores son
- Chunhan Wu (de la PLA University of Science and Technology, China),
- Xingyuan Zhang (de la PLA University of Science and Technology, China) y
- Christian Urban (del King’s College London, UK).
Su resumen es
If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model—a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security com- promise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson’s inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.
El trabajo se presentará en diciembre en el CPP 2013 (3rd Conference on Certified Programs and Proofs.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.