Abstract
We address the issue of formally validating the deployment of access control security policies. We show how the use of a formal expression of the security requirements, related to a given system, ensures the deployment of an anomaly free abstract security policy. We also describe how to develop appropriate algorithms by using a theorem proving approach with a modeling language allowing the specification of the system, of the link between the system and the policy, and of certain target security properties. The result is a set of proved algorithms that constitute the certified technique for a reliable security policy deployment.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abou el Kalam, A., Baida, R.E., Balbiani, P., Benferhat, S., Cuppens, F., Deswarte, Y., Miège, A., Saurel, C., Trouessin, G.: Organization Based Access Control. In: IEEE 4th Intl. Workshop on Policies for Distributed Systems and Networks, Lake Come, Italy, pp. 120–131 (2003)
Abrial, J.R.: The B-Book — Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.R., Cansell, D., Méry, D.: Formal Derivation of Spanning Trees Algorithms. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457–476. Springer, Heidelberg (2003)
Autrel, F., Cuppens, F., Cuppens-Boulahia, N., Coma, C.: MotOrBAC 2: A security policy tool. In: SAR-SSI 2008, Loctudy, France (2008)
Bartal, Y., Mayer, A., Nissim, K., Wool, A.: Firmato: A novel firewall management toolkit. In: IEEE Symposium on Security and Privacy, pp. 17–31 (1999)
Benaissa, N., Cansell, D., Méry, D.: Integration of Security Policy into System Modeling. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 232–247. Springer, Heidelberg (2006)
Capretta, V., Stepien, B., Felty, A., Matwin, S.: Formal correctness of conflict detection for firewalls. In: ACM workshop on Formal methods in security engineering, FMSE 2007, Virginia, USA, pp. 22–30 (2007)
Casassa Mont, M., Baldwin, A., Goh, C.: POWER prototype: towards integrated policy-based management. In: Network Operations and Management Symposium, USA, pp. 789–802 (2000)
Cuppens, F., Cuppens-Boulahia, N., Ben Ghorbel, M.: High level conflict management strategies in advanced access control models. Electronic Notes in Theoretical Computer Science (ENTCS) 186, 3–26 (2007)
Damianou, N., Dulay, N., Lupu, E., Sloman, M.: The ponder policy specification language. In: Sloman, M., Lobo, J., Lupu, E.C. (eds.) POLICY 2001. LNCS, vol. 1995, pp. 18–38. Springer, Heidelberg (2001)
Fraer, R.: Minimum Spanning Tree. In: FACIT 1999, pp. 79–114. Springer, Heidelberg (1999)
Fu, Z., Wu, S.F., Huang, H., Loh, K., Gong, F., Baldine, I., Xu, C.: IPSec/VPN Security Policy: Correctness, Conflict Detection and Resolution. In: Policy 2001 Workshop, Bristol, UK, pp. 39–56 (2001)
Garcia-Alfaro, J., Cuppens, N., Cuppens, F.: Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies. International Journal of Information Security 7(2), 103–122 (2008)
Jürjens, J.: Secure Systems Development with UML. Springer, New York (2004)
Jürjens, J., Schreck, J., Bartmann, P.: Model-based security analysis for mobile communications. In: 30th international conference on Software engineering, Leipzig, Germany, pp. 683–692 (2008)
Laborde, R., Kamel, M., Barrere, F., Benzekri, A.: Implementation of a Formal Security Policy Refinement Process in WBEM Architecture. Journal of Network and Systems Management 15(2) (2007)
Ioannidis, S., Bellovin, S.M., Ioannidis, J., Keromitis, A.D., Anagnostakis, K., Smith, J.M.: Virtual Private Services: Coordinated Policy Enforcement for Distributed Applications. International Journal of Network Security 4(1), 69–80 (2007)
Ponsini, O., Fédèle, C., Kounalis, E.: Rewriting of imperative programs into logical equations. In: Sci. Comput. Program., vol. 54, pp. 363–401. Elsevier North-Holland, Inc., Amsterdam (2005)
Preda, S., Cuppens, F., Cuppens-Boulahia, N., Alfaro, J.G., Toutain, L., Elrakaiby, Y.: A Semantic Context Aware Security Policy Deployment. In: ACM Symposium on Information, Computer and Communication Security (ASIACCS 2009), Sydney, Australia (March 2009)
Sandhu, R., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-Based Access Control Models. IEEE Computer 29(2), 38–47 (1996)
Unal, D., Ufuk Çaglayan, M.: Theorem proving for modeling and conflict checking of authorization policies. In: Proceedings of the International Symposium on Computer Networks, ISCN, Istanbul, Turkey (2006)
ACI DESIRS project: DÉveloppement de Systèmes Informatiques par Raffinement des contraintes Sécuritaires
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Preda, S., Cuppens-Boulahia, N., Cuppens, F., Garcia-Alfaro, J., Toutain, L. (2010). Model-Driven Security Policy Deployment: Property Oriented Approach. In: Massacci, F., Wallach, D., Zannone, N. (eds) Engineering Secure Software and Systems. ESSoS 2010. Lecture Notes in Computer Science, vol 5965. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11747-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-11747-3_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11746-6
Online ISBN: 978-3-642-11747-3
eBook Packages: Computer ScienceComputer Science (R0)