Skip to main content
SpringerLink
Log in

Compliance Verification Algorithm for Computer Systems Security Policies

  • Conference paper
  • First Online:
E-Technologies: Embracing the Internet of Things (MCETECH 2017)

Part of the book series: Lecture Notes in Business Information Processing ((LNBIP,volume 289))

Included in the following conference series:

  • 924 Accesses

Abstract

This paper proposes an algebraic formalism and a dedicated logic for computer systems and security policies specifications. A tableau-based proof system is then developed for assessing whether policies are satisfied for a given model of a computer system. A practical example and an implementation within a theorem prover show the effectiveness of our specification and verification technique.

This research is supported by a research grant from the Natural Science and Engineering Council of Canada, NSERC.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FoSSaCS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998). doi:10.1007/BFb0053547

    Chapter  Google Scholar 

  2. Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: POPL 2000: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 365, p. 377 (2000)

    Google Scholar 

  3. Cardelli, L., Gordon, A.D.: Ambient logic. Mathematical Structures in Computer Science (2006)

    Google Scholar 

  4. Hirschkoff, D., Lozes, E., Sangiorgi, D.: On the expressiveness of the ambient logic. Logical Methods Comput. Sci. 2(2), 1–35 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  5. Basin, D., Klaedtke, F., Müller, S.: Monitoring security policies with metric first-order temporal logic. In: Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, SACMAT 2010, pp. 23–34. ACM, New York (2010)

    Google Scholar 

  6. Degano, P., Levi, F., Bodei, C.: Safe ambients: control flow analysis and security. In: Jifeng, H., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 199–214. Springer, Heidelberg (2000). doi:10.1007/3-540-44464-5_15

    Chapter  Google Scholar 

  7. Levi, F., Sangiorgi, D.: Mobile safe ambients. ACM Trans. Program. Lang. Syst. 25(1), 1–69 (2003)

    Article  Google Scholar 

  8. Braghin, C., Cortesi, A., Focardi, R.: Control flow analysis of mobile ambients with security boundaries. In: Jacobs, B., Rensink, A. (eds.) FMOODS 2002. ITIFIP, vol. 81, pp. 197–212. Springer, Boston, MA (2002). doi:10.1007/978-0-387-35496-5_14

    Chapter  Google Scholar 

  9. Ferrari, G., Moggi, E., Pugliese, R.: Guardians for ambient-based monitoring. In: F-WAN: Foundations of Wide Area Network Computing, vol. 66 (2002)

    Google Scholar 

  10. Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, New York (1990)

    Book  MATH  Google Scholar 

  11. Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Logic 163(3), 291–313 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  12. Cleaveland, R.: Tableau-based model checking in the propositional mu-calculus. Acta Informatica 27(8), 725–747 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  13. Paulson, L.C.: The isabelle reference manual (2008)

    Google Scholar 

  14. Abate, P., Goré, R.: The tableaux work bench. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol. 2796, pp. 230–236. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45206-5_18

    Chapter  Google Scholar 

  15. Cerro, L.F., Fauthoux, D., Gasquet, O., Herzig, A., Longin, D., Massacci, F.: Lotrec: the generic tableau prover for modal and description logics. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 453–458. Springer, Heidelberg (2001). doi:10.1007/3-540-45744-5_38

    Chapter  Google Scholar 

  16. Gasquet, O., Herzig, A., Longin, D., Sahade, M.: LoTREC: logical tableaux research engineering companion. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS, vol. 3702, pp. 318–322. Springer, Heidelberg (2005). doi:10.1007/11554554_25

    Chapter  Google Scholar 

  17. Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)

    Article  Google Scholar 

  18. Hamlen, K.W., Morrisett, G., Schneider, F.B.: Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst. (TOPLAS) 28(1), 175–205 (2006)

    Article  Google Scholar 

  19. Bauer, L., Ligatti, J., Walker, D.: A language and system for enforcing run-time security policies. Technical report TR-699-04, Princeton University (2004)

    Google Scholar 

  20. Basin, D., Jugé, V., Klaedtke, F., Zălinescu, E.: Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur. 16(1), 3:1–3:26 (2013)

    Article  MATH  Google Scholar 

  21. Hamlen, K.: Security policy enforcement by automated program-rewriting. Ph.D. thesis, Cornell University, Ithaca, NY, USA (2006). AAI3227141

    Google Scholar 

  22. Langar, M., Mejri, M., Adi, K.: Formal enforcement of security policies on concurrent systems. J. Symbolic Comput. 3, 997–1016 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  23. Khoury, R., Tawbi, N.: Equivalence-preserving corrective enforcement of security properties. Int. J. Inf. Comput. Secur. 7(2/3/4), 113–139 (2015)

    Google Scholar 

  24. Sui, G., Mejri, M.: Security enforcement by rewriting: an algebraic approach. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds.) FPS 2015. LNCS, vol. 9482, pp. 311–321. Springer, Cham (2016). doi:10.1007/978-3-319-30303-1_22

    Chapter  Google Scholar 

  25. Adi, K., Debbabi, M., Mejri, M.: A new logic for electronic commerce protocols. Int. J. Theor. Comput. Sci. (TCS) 291, 223–283 (2003)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Security Research Laboratory, Université du Québec en Outaouais, Gatineau, Canada

    Liviu Pene & Kamel Adi

  2. Laboratoire d’Informatique Médicale, Université de Bejaia, Bejaia, Algeria

    Lamia Hamza

Authors
  1. Liviu Pene
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lamia Hamza
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kamel Adi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Liviu Pene .

Editor information

Editors and Affiliations

  1. Université de Montréal, Montreal, Québec, Canada

    Esma Aïmeur

  2. University of Ottawa, Ottawa, Ontario, Canada

    Umar Ruhi

  3. Carleton University, Ottawa, Ontario, Canada

    Michael Weiss

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Pene, L., Hamza, L., Adi, K. (2017). Compliance Verification Algorithm for Computer Systems Security Policies. In: Aïmeur, E., Ruhi, U., Weiss, M. (eds) E-Technologies: Embracing the Internet of Things . MCETECH 2017. Lecture Notes in Business Information Processing, vol 289. Springer, Cham. https://doi.org/10.1007/978-3-319-59041-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-59041-7_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-59040-0

  • Online ISBN: 978-3-319-59041-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation