Automated Proof of Bell-LaPadula Security Properties
share
Almost fifty years ago, D.E. Bell and L. LaPadula published the first formal model of a secure system, know 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.
READ FULL TEXT