Xen混合多策略模型的设计与形式化验证

Design and Formal Verification of Xen Hybrid Multi-police Model

Xen作为一种虚拟化工具因开源、高效等特点而受到越来越多的关注。作为Xen安全的基础,XSM决定了其安全性。原生XSM没有对系统资源进行安全分级,并且以虚拟机为管理对象使得Dom0作为一个唯一管理域不符合最小特权,文中设计了一种混合多策略模型SV_HMPMD。在该模型中,针对BLP引入多级安全标签,从而增加BLP的实用性,并通过DTE和RBAC对特权进行更细致的划分,从而对Dom0特权进行合理限制。提出了一种分层模型,利用该模型对混合模型进行形式化的描述。运用系统不变量构造访问规则的安全属性需求,通过Isabelle/HOL对模型设计与安全需求的一致性进行验证。

As a popular open-source virtualization tools,XEN has attracted more and more attention.XSM,as a Xen security model,determins its security.Native XSM does not carry on safe differentiated control design to system source and uses Dom0 as unique virtual machines administrative domain that does not meet minimum privileges.According to these questions,we designed a hybrid multi-police model named SV_HMPMD.In order to improve BLP＇s practicability,the model introduces multi-level security labels.In order to divide the privilege in detail,we combined DTE with RBAC.We designed a hierarchical model that describes SV_HMPMD by formal methods for xsm to verify the consistency between achievements and security requirements by the tools named Isabelle/HOL.