nach oben

Tipp

Automated Proof of Bell–LaPadula Security Properties

verfasst von: Maximiliano Cristiá, Gianfranco Rossi

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2021

Einloggen, um Zugang zu erhalten

Abstract

Almost 50 years ago, D. E. Bell and L. LaPadula published the first formal model of a secure system, known today as the Bell–LaPadula (BLP) model. BLP is described as a state machine by means of first-order logic and set theory. The authors also formalize two state invariants known as security condition and *-property. Bell and LaPadula prove that all the state transitions preserve these invariants. In this paper we present a fully automated proof of the security condition and the *-property for all the model operations. The model and the proofs are coded in the \(\{log\}\) tool. As far as we know this is the first time such proofs are automated. Besides, we show that the \(\{log\}\) model is also an executable prototype. Therefore we are providing an automatically verified executable prototype of BLP.

Nächster Artikel A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

This number is obtained on a Latitude E7470 (06DC) with a 4 core Intel(R) Core™ i7-6600U CPU at 2.60GHz with 8 Gb of main memory. The software components are the following: Linux Ubuntu 18.04.3 (LTS) 64-bit with kernel 4.15.0-70-generic, and \(\{log\}\) 4.9.6-18b over SWI-Prolog (multi-threaded, 64 bits, version 7.6.4).

Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996) CrossRef

Anderson, J.P.: Computer security technology planning study. Techreport ESD-TR-73-51, Vol II, Deputy for Command and Management Systems, HQ Electronic Systems Division (AFSC) (1972). http://seclab.cs.ucdavis.edu/projects/history/papers/ande72.pdf

Barthe, G., Betarte, G., Campo, J.D., Luna, C.: System-level non-interference of constant-time cryptography. Part I: model. J. Autom. Reason. 63(1), 1–51 (2019). https://doi.org/10.1007/s10817-017-9441-5 MathSciNetCrossRefMATH

Barthe, G., Grégoire, B., Heraud, S., Olmedo, F., Béguelin, S.Z.: Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21(6), 881–917 (2013). https://doi.org/10.3233/JCS-130476 CrossRefMATH

Basin, D.A., Cremers, C., Meadows, C.A.: Model checking security protocols. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 727–762. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-10575-8_22 CrossRefMATH

Bell, D.E., LaPadula, L.: Secure Computer Systems: Mathematical Foundations. MTR 2547, The MITRE Corporation, McLean (1973)

Bell, D.E., LaPadula, L.: Secure Computer Systems: Mathematical Model. ESD-TR 73-278, The MITRE Corporation, McLean (1973)

Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007, Yerevan, Armenia, October 15–19, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4790, pp. 151–165. Springer (2007). https://doi.org/10.1007/978-3-540-75560-9_13

Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.8.1. LogiCal Project, Palaiseau, France (2018)

10.

Cristiá, M.: Formal verification of an extension of a secure, compatible UNIX file system. In: Anales de la XXIX Conferencia Latinoamericana de Informática. CLEI, La Paz, Bolivia (2003)

11.

Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) Automated Deduction—CADE 26—26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185–201. Springer (2017). https://doi.org/10.1007/978-3-319-63046-5_12

12.

Cristiá, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science—17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29–November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333–349. Springer (2018). https://doi.org/10.1007/978-3-030-02149-8_20

13.

Cristiá, M., Rossi, G.: Automated reasoning with restricted intensional sets (2019). CoRR arXiv:1910.09118

14.

Cristiá, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295–330 (2020). https://doi.org/10.1007/s10817-019-09520-4 MathSciNetCrossRefMATH

15.

Cristiá, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229–243. Springer, Berlin (2013)

16.

Dénès, M., Hritcu, C., Lampropoulos, L., Paraskevopoulou, Z., Pierce, B.C.: Quickchick: property-based testing for Coq. In: The Coq Workshop (2014)

17.

Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V.: Formal verification of OS security model with alloy and event-b. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z—4th International Conference, ABZ 2014, Toulouse, France, June 2–6, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8477, pp. 309–313. Springer (2014). https://doi.org/10.1007/978-3-662-43652-3_30

18.

Doligez, D., Jaume, M., Rioboo, R.: Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the focalize environment. In: Maffeis, S., Rezk, T. (eds.) Proceedings of the 2012 Workshop on Programming Languages and Analysis for Security, PLAS 2012, Beijing, China, 15 June, 2012, p. 9. ACM (2012). https://doi.org/10.1145/2336717.2336726

19.

Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861–931 (2000) CrossRef

20.

Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log Program. 6(6), 645–701 (2006). https://doi.org/10.1017/S1471068406002730 MathSciNetCrossRefMATH

21.

Gasser, M.: Building a Secure Computer System. Van Nostrand Reinhold Co., New York (1988)

22.

Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26–28, 1982, pp. 11–20. IEEE Computer Society (1982). https://doi.org/10.1109/SP.1982.10014

23.

Haraty, R.A., Naous, M.: Role-based access control modeling and validation. In: 2013 IEEE Symposium on Computers and Communications, ISCC 2013, Split, Croatia, 7–10 July, 2013, pp. 61–66. IEEE Computer Society (2013). https://doi.org/10.1109/ISCC.2013.6754925

24.

Lipner, S.B.: The birth and death of the orange book. IEEE Ann. Hist. Comput. 37(2), 19–31 (2015). https://doi.org/10.1109/MAHC.2015.27 CrossRef

25.

McLean, J.: A comment on the ’basic security theorem’ of bell and lapadula. Inf. Process. Lett. 20(2), 67–70 (1985). https://doi.org/10.1016/0020-0190(85)90065-1 MathSciNetCrossRef

26.

McLean, J.: Twenty years of formal methods. In: 1999 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 9–12, 1999, pp. 115–116. IEEE Computer Society (1999). https://doi.org/10.1109/SECPRI.1999.766907

27.

Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: sel4: From general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19–22, 2013, pp. 415–429. IEEE Computer Society (2013). https://doi.org/10.1109/SP.2013.35

28.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002). https://doi.org/10.1007/3-540-45949-9

29.

Rossi, G.: \(\{log\}\) (2008). http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html

30.

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5–19 (2006). https://doi.org/10.1109/JSAC.2002.806121 CrossRef

31.

Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets—An Introduction to SETL. Texts and Monographs in Computer Science. Springer, Berlin (1986). https://doi.org/10.1007/978-1-4613-9575-1 CrossRefMATH

32.

Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992) MATH

33.

Stasiak, A., Zielinski, Z.: An approach to automated verification of multi-level security system models. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds.) New Results in Dependability and Computer Systems—Proceedings of the 8th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, September 9–13, 2013, Brunów, Poland. Advances in Intelligent Systems and Computing, vol. 224, pp. 375–388. Springer (2013). https://doi.org/10.1007/978-3-319-00945-2_34

34.

von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) 9th European Symposium on Research Computer Security—ESORICS 2004, Sophia Antipolis, France, September 13–15, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3193, pp. 225–243. Springer (2004). https://doi.org/10.1007/978-3-540-30108-0_14

Titel: Automated Proof of Bell–LaPadula Security Properties
verfasst von: Maximiliano Cristiá
Gianfranco Rossi
Publikationsdatum: 27.07.2020
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-020-09577-6

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Automated Proof of Bell–LaPadula Security Properties

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner