论文标题
自动化的铃lapadula安全属性证明
Automated Proof of Bell-LaPadula Security Properties
论文作者
论文摘要
大约五十年前，D.E。 Bell and L. Lapadula发布了安全系统的第一个正式模型，今天被称为Bell-Lapadula（BLP）模型。 BLP通过一阶逻辑和集合理论描述为状态机。作者还形式化了两个称为安全状况和 * - 范围的状态不变的。贝尔和拉帕杜拉证明了所有国家过渡都保留了这些不变的人。 在本文中，我们提供了所有模型操作的安全状况的全自动证明和 * - 秘诀。模型和证明是在{log}工具中编码的。据我们所知，这是第一次自动化的证据。此外，我们表明{log}模型也是可执行的原型。因此，我们提供了自动验证的BLP可执行原型。
Almost fifty 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.
