Abstract
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 compromise 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Archer, M., Leonard, E.I., Pradella, M.: Analyzing Security-Enhanced Linux Policy Specifications. In: Proc. of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY), pp. 158–169 (2003)
Bugliesi, M., Calzavara, S., Focardi, R., Squarcina, M.: Gran: Model Checking Grsecurity RBAC Policies. In: Proc. of the 25th IEEE Computer Security Foundations Symposium (CSF), pp. 126–138 (2012)
Guttman, J.D., Herzog, A.L., Ramsdell, J.D., Skorupka, C.W.: Verifying Information Flow Goals in Security-Enhanced Linux. Journal of Computer Security 13(1), 115–134 (2005)
Jha, S., Li, N., Tripunitara, M.V., Wang, Q., Winsborough, W.H.: Towards Formal Verification of Role-Based Access Control Policies. IEEE Transactions Dependable and Secure Computing 5(4), 242–255 (2008)
Ott, A.: The Role Compatibility Security Model. In: Proc. of the 7th Nordic Workshop on Secure IT Systems, NordSec (2002)
Ott, A.: Mandatory Rule Set Based Access Control in Linux: A Multi-Policy Security Framework and Role Model Solution for Access Control in Networked Linux Systems. PhD thesis, University of Hamburg (2007)
Ott, A., Fischer-Hübner, S.: A Role-Compatibility Model for Secure System Administration, http://www.rsbac.org/doc/media/rc-paper.php
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
Sarna-Starosta, B., Stoller, S.D.: Policy Analysis for Security-Enhanced Linux. In: Proc. of the 2004 Workshop on Issues in the Theory of Security (WITS), pp. 1–12 (2004)
Uzun, E., Atluri, V., Sural, S., Vaidya, J., Parlato, G., Ferrara, A.L., Madhusudan, P.: Analyzing Temporal Role Based Access Control Models. In: Proc. of the 17th ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 177–186 (2012)
Zhang, X., Urban, C., Wu, C.: Priority Inheritance Protocol Proved Correct. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 217–232. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Wu, C., Zhang, X., Urban, C. (2013). A Formal Model and Correctness Proof for an Access Control Policy Framework. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)