Model Checking Distributed Mandatory Access Control Policies
Model Checking Distributed Mandatory Access Control Policies
复制标题
DOI：
10.1145/2785966
复制
发表时间：
2015-12
期刊：
影响因子：
--
通讯作者：
P. Alexander;Lee Pike;P. Loscocco;George Coker
中科院分区：
文献类型：
--
作者：
P. Alexander;Lee Pike;P. Loscocco;George Coker
这项工作检查了模型检查技术的使用，以验证交互虚拟机集合的系统级安全属性。具体来说，我们将研究如何在单个虚拟机和管理程序中实现本地访问控制策略，以满足全局访问控制约束。SAL模型检查器用于对一组有状态域进行建模和验证，这些域具有受保护的资源和试图从其他域访问所需资源的本地MAC策略。对模型进行了描述，并给出了验证条件。控制状态空间爆炸的需要被激发，并且探索了编写定理和限制域的技术。最后，对分析结果和分析复杂度进行了检验。
This work examines the use of model checking techniques to verify system-level security properties of a collection of interacting virtual machines. Specifically, we examine how local access control policies implemented in individual virtual machines and a hypervisor can be shown to satisfy global access control constraints. The SAL model checker is used to model and verify a collection of stateful domains with protected resources and local MAC policies attempting to access needed resources from other domains. The model is described along with verification conditions. The need to control state-space explosion is motivated and techniques for writing theorems and limiting domains explored. Finally, analysis results are examined along with analysis complexity.