Bell-LaPadula安全性质的自动化证明
软件工程
2020-07-17 v3
摘要
大约五十年前，D.E. Bell与L. LaPadula发表了首个安全系统的形式化模型，即现今所知的Bell-LaPadula(BLP)模型。BLP借助一阶逻辑与集合论被描述为一台状态机。作者还形式化了两个称为安全条件与*-性质的状态不变量。Bell与LaPadula证明了所有状态转移均保持这些不变量。本文中，我们给出对所有模型操作的安全条件与*-性质的完全自动化证明。该模型与证明在{log}工具中编码。据我们所知，这是此类证明首次实现自动化。此外，我们展示了{log}模型同时也是一个可执行的原型。因此我们提供了一个经自动验证的BLP可执行原型。
引用
@article{arxiv.2001.10512,
title = {Automated Proof of Bell-LaPadula Security Properties},
author = {Maximiliano Cristia and Gianfranco Rossi},
journal= {arXiv preprint arXiv:2001.10512},
year = {2020}
}