From Qualitative to Quantitative Enforcement of Security Policy

  • Fabio Martinelli
  • Ilaria Matteucci
  • Charles Morisset
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7531)


The problem of enforcing a security policy has been particularly well studied over the last decade, following Schneider’s seminal work on security automata. We first present in this paper this problem through its qualitative aspect, where one tries to specify and to define a “good” runtime monitor. In particular, we recall that under some conditions, a monitor can be automatically synthesized, using partial model checking. We then introduce some of the quantitative challenges of runtime enforcement, which focus on the problem of defining what does it mean for a monitor to be better than another one, and we sketch several directions that could be explored to tackle this issue.


Security Policy Enforcement Mechanism Process Algebra Controller Operator Execution Trace 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andersen, H.R.: Partial model checking. In: LICS 1995: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p. 398. IEEE Computer Society (1995)Google Scholar
  2. 2.
    Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theoretical Computer Science 303(1), 7–34 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Badouel, E., Caillaud, B., Darondeau, P.: Distributing finite automata through petri net synthesis. Journal on Formal Aspects of Computing 13, 447–470 (2002)zbMATHCrossRefGoogle Scholar
  4. 4.
    Bartoletti, M., Degano, P., Ferrari, G.-L.: Checking Risky Events Is Enough for Local Policies. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol. 3701, pp. 97–112. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Basin, D., Jugé, V., Klaedtke, F., Zălinescu, E.: Enforceable Security Policies Revisited. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 309–328. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  6. 6.
    Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Proceedings of the FLoC 2002 Workshop on Foundations of Computer Security, July 25-26, pp. 95–104. DIKU Technical Report, Copenhagen (2002)Google Scholar
  7. 7.
    Bauer, L., Ligatti, J., Walker, D.: Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security 4(1-2) (2005)Google Scholar
  8. 8.
    Bielova, N., Massacci, F.: Predictability of Enforcement. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 73–86. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Brewer, D.F.C., Nash, M.J.: The Chinese Wall Security Policy. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 329–339 (May 1989)Google Scholar
  10. 10.
    Bruns, G., Huth, M.: Access-control policies via Belnap logic: Effective and efficient composition and analysis. In: Proceedings of the CSF 2008, pp. 163–176. IEEE Computer Society (2008)Google Scholar
  11. 11.
    Bruns, G., Sutherland, I.: Model Checking and Fault Tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 45–59. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  12. 12.
    Cheng, P.-C., Rohatgi, P., Keser, C., Karger, P.A., Wagner, G.M., Reninger, A.S.: Fuzzy multi-level security: An experiment on quantified risk-adaptive access control. In: Proceedings of Security and Privacy 2007, pp. 222–230. IEEE (2007)Google Scholar
  13. 13.
    Costa, G., Matteucci, I.: Gate automata-driven run-time enforcement. Computers & Mathematics with Applications 63(2), 518–524 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Drábik, P., Martinelli, F., Morisset, C.: Cost-aware runtime enforcement of security policies. In: Proceedings of the Security and Trust Management 2012. LNCS (to appear, 2012)Google Scholar
  15. 15.
    Drábik, P., Martinelli, F., Morisset, C.: A quantitative approach for the inexact enforcement of security policies. In: Proceedings of the Information Security Conference 2012. LNCS (to appear, 2012)Google Scholar
  16. 16.
    Ferraiolo, D.F., Kuhn, D.R.: Role-based access control. In: Proceedings of the 15th National Computer Security Conference, pp. 554–563 (1992)Google Scholar
  17. 17.
    Jøsang, A.: Conditional reasoning with subjective logic. Multiple-Valued Logic and Soft Computing 15(1), 5–38 (2009)MathSciNetGoogle Scholar
  18. 18.
    Krautsevich, L., Lazouski, A., Martinelli, F., Mori, P., Yautsiukhin, A.: Usage Control, Risk and Trust. In: Katsikas, S., Lopez, J., Soriano, M. (eds.) TrustBus 2010. LNCS, vol. 6264, pp. 1–12. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Krautsevich, L., Martinelli, F., Morisset, C., Yautsiukhin, A.: Risk-Based Auto-delegation for Probabilistic Availability. In: Garcia-Alfaro, J., Navarro-Arribas, G., Cuppens-Boulahia, N., de Capitani di Vimercati, S. (eds.) DPM 2011 and SETOP 2011. LNCS, vol. 7122, pp. 206–220. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open Systems in Reactive Environments: Control and Synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 92. Springer, Heidelberg (2000), CrossRefGoogle Scholar
  21. 21.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (extended abstract),
  22. 22.
    Martinelli, F.: Analysis of security protocols as open systems. Theoretical Computer Science 290(1), 1057–1106 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  23. 23.
    Martinelli, F., Matteucci, I.: A framework for automatic generation of security controller. STVR Journal (2010)Google Scholar
  24. 24.
    Martinelli, F., Matteucci, I.: Partial model checking, process algebra operators and satisfiability procedures for (automatically) enforcing security properties. Technical report, IIT-CNR. Presented at the International Workshop on Foundations of Computer Security, FCS 2005 (2005)Google Scholar
  25. 25.
    Martinelli, F.: Towards an Integrated Formal Analysis for Security and Trust. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 115–130. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  26. 26.
    Martinelli, F., Matteucci, I.: Through modeling to synthesis of security automata. Electr. Notes Theor. Comput. Sci. 179, 31–46 (2007)CrossRefGoogle Scholar
  27. 27.
    Martinelli, F., Morisset, C.: Quantitative access control with partially-observable markov decision processes. In: Proceedings of CODASPY 2012, pp. 169–180. ACM, New York (2012), Google Scholar
  28. 28.
    Merlin, P., Bochmann, G.V.: On the Construction of Submodule Specification and Communication Protocols. ACM Transactions on Programming Languages and Systems 5, 1–25 (1983)zbMATHCrossRefGoogle Scholar
  29. 29.
    Molloy, I., Dickens, L., Morisset, C., Cheng, P.-C., Lobo, J., Russo, A.: Risk-based security decisions under uncertainty. In: Proceedings of CODASPY 2012, pp. 157–168. ACM, New York (2012), Google Scholar
  30. 30.
    Moses, T.: eXtensible Access Control Markup Language TC v2.0 (XACML) (February 2005),
  31. 31.
    Ni, Q., Bertino, E., Lobo, J.: D-algebra for composing access control policy decisions. In: Li, W., Susilo, W., Tupakula, U.K., Safavi-Naini, R., Varadharajan, V. (eds.) ASIACCS, pp. 298–309. ACM (2009)Google Scholar
  32. 32.
    Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security 3(1), 30–50 (2000)CrossRefGoogle Scholar
  33. 33.
    Street, R.S., Emerson, E.A.: An automata theoretic procedure for the propositional μ-calculus. Information and Computation 81(3), 249–264 (1989)MathSciNetCrossRefGoogle Scholar
  34. 34.
    Walukiewicz, I.: A Complete Deductive System for the μ-Calculus. Ph.D. thesis, Institute of Informatics, Warsaw University (June 1993)Google Scholar
  35. 35.
    Wong-Toi, H., Dill, D.L.: Synthesizing Processes and Schedulers from Temporal Specifications. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 272–281. Springer, Heidelberg (1991)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Fabio Martinelli
    • 1
  • Ilaria Matteucci
    • 1
  • Charles Morisset
    • 1
  1. 1.IIT-CNR, Security GroupPisaItaly

Personalised recommendations