Abstract
We present a specification approach of secured systems as transition systems and security policies as constraints that guard the transitions. In this context, security properties are expressed as invariants. Then we propose an abduction algorithm to generate possible security policies for a given transition-based system. Because abduction is guided by invariants, the generated security policies enforce security properties specified by these invariants. In this framework we are able to tune abduction in two ways in order to: (i) filter out bad security policies and (ii) generate additional possible security policies. Invariant-guided abduction helps designing policies and thus allows using formal methods much earlier in the process of building secured systems. This approach is illustrated on role-based access control systems.
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
Examples of abduction with Coq [2], http://www-sop.inria.fr/everest/Clement.Hurlin/abduction.tgz
The Coq proof assistant, http://coq.inria.fr
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Alrajeh, D., Ray, O., Russo, A., Uchitel, S.: Using abduction and induction for operational requirements elaboration. Journal of Applied Logic 7(3), 275–288 (2009); Special Issue: Abduction and Induction in Artificial Intelligence
Becker, M.Y., Nanz, S.: A logic for state-modifying authorization policies. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 203–218. Springer, Heidelberg (2007)
Becker, M.Y., Nanz, S.: The role of abduction in declarative authorization policies. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol. 4902, pp. 84–99. Springer, Heidelberg (2008)
Bonichon, R., Delahaye, D., Doligez, D.: zenon: An extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007)
Bourdier, T., Cirstea, H., Jaume, M., Kirchner, H.: Formal specification and validation of security policies. Tech. Rep. 00507300, INRIA (2010), http://hal.inria.fr/inria-00507300/
Cox, P.T., Pietrzykowski, T.: A complete, nonredundant algorithm for reversed skolemization. In: Bibel, W., Kowalski, R.A. (eds.) CADE 1980. LNCS, vol. 87, pp. 374–385. Springer, Heidelberg (1980)
Damianou, N.C., Bandara, A.K., Sloman, M.S., Lupu, E.C.: A survey of policy specification approaches. Tech. rep., Imperial College of Science Technology and Medicine (2002)
Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Specifying and reasoning about dynamic access-control policies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 632–646. Springer, Heidelberg (2006)
Ferraiolo, D., Kuhn, D.R., Chandramouli, R.: Role-based access control. Computer security series. Artech House, Boston (2003)
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematical Zeitschrift 39, 176–210 (1934)
Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive logic programming. Journal of Logic and Computation 2(6), 719–770 (1992)
Kakas, A.C., Kowalski, R.A., Toni, F.: The role of abduction in logic programming. Handbook of Logic in Artificial Intelligence and Logic Programming 5, 235–324 (1998)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Lamport, L.: A summary of TLA+ (2000)
Liu, Y.A., Stoller, S.D.: Role-based access control: A corrected and simplified specification. In: Wang, C., King, S., Wachter, R., Herklotz, R., Arney, C., Toth, G., Hislop, D., Heise, S., Combs, T. (eds.) Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats., Wiley, Chichester (2007)
Mayer, M.C., Pirri, F.: First order abduction via tableau and sequent calculi. Logic Journal of the Interest Group in Pure and Applied Logics 1(1), 99–117 (1993)
Merz, S.: The specification language TLA+. Logics of Specificat. Languages, 401–451 (2008)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Paulson, L.C.: A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science 5(3), 73–87 (1999)
Russo, A., Miller, R., Nusheibeh, B., Kramer, J.: An abductive approach for analysing event-based requirements specification. In: Stuckey, P. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 22–37. Springer, Heidelberg (2002)
Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Computer 29(2), 38–47 (1996)
Soler-Toscano, F., Nepomuceno-Fernández, A., Aliseda-Llera, A.: Abduction via C-tableaux and δ-resolution. Journal of Applied Non-Classical Logics 19(2), 211–225 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hurlin, C., Kirchner, H. (2011). Semi-automatic Synthesis of Security Policies by Invariant-Guided Abduction. In: Degano, P., Etalle, S., Guttman, J. (eds) Formal Aspects of Security and Trust. FAST 2010. Lecture Notes in Computer Science, vol 6561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19751-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-19751-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19750-5
Online ISBN: 978-3-642-19751-2
eBook Packages: Computer ScienceComputer Science (R0)