Automated Proof of Bell–LaPadula Security Properties
作者： Maximiliano Cristiá , Gianfranco Rossi
DOI: 10.1007/S10817-020-09577-6
关键词:
摘要: Almost 50 years ago, D. E. Bell and L. LaPadula published the first formal model of a secure system, known today as Bell–LaPadula (BLP) model. BLP is described state machine by means first-order logic set theory. The authors also formalize two invariants security condition *-property. prove that all transitions preserve these invariants. In this paper we present fully automated proof *-property for operations. proofs are coded in $$\{log\}$$ tool. As far know time such automated. Besides, show an executable prototype. Therefore providing automatically verified prototype BLP.
arxiv.org
springer.com
sci-hub.st 参考文章(28)
Andrzej Stasiak, Zbigniew Zieliński, An Approach to Automated Verification of Multi-Level Security System Models New Results in Dependability and Computer Systems. ,vol. 224, pp. 375- 388 ,(2013) , 10.1007/978-3-319-00945-2_34
Maximiliano Cristiá, Gianfranco Rossi, Claudia Frydman, {log} as a Test Case Generator for the Test Template Framework international conference on software engineering. pp. 229- 243 ,(2013) , 10.1007/978-3-642-40561-7_16
Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov, Formal Verification of OS Security Model with Alloy and Event-B ABZ 2014 Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477. pp. 309- 313 ,(2014) , 10.1007/978-3-662-43652-3_30
Morrie Gasser, Building a Secure Computer System ,(1988)
J.-R. Abrial, The B-Book: Assigning Programs to Meanings ,(1996)
David von Oheimb, Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage Computer Security – ESORICS 2004. pp. 225- 243 ,(2004) , 10.1007/978-3-540-30108-0_14
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin, Verified indifferentiable hashing into elliptic curves Journal of Computer Security. ,vol. 21, pp. 881- 917 ,(2013) , 10.3233/JCS-130476
Steven B. Lipner, The Birth and Death of the Orange Book IEEE Annals of the History of Computing. ,vol. 37, pp. 19- 31 ,(2015) , 10.1109/MAHC.2015.27
Richard Bonichon, David Delahaye, Damien Doligez, Zenon: an extensible automated theorem prover producing checkable proofs international conference on logic programming. ,vol. 4790, pp. 151- 165 ,(2007) , 10.1007/978-3-540-75560-9_13
Ramzi A. Haraty, Mirna Naous, Role-Based Access Control modeling and validation international symposium on computers and communications. pp. 000061- 000066 ,(2013) , 10.1109/ISCC.2013.6754925