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.

Automated Proof of Bell–LaPadula Security Properties / Cristia, M.; Rossi, G.. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - (2020). [10.1007/s10817-020-09577-6]

Automated Proof of Bell–LaPadula Security Properties

Rossi G.
2020-01-01

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.
2020
Automated Proof of Bell–LaPadula Security Properties / Cristia, M.; Rossi, G.. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - (2020). [10.1007/s10817-020-09577-6]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2882868
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact