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

摘要：

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

关键词：SV_HMPMD、语义模型、形式化证明、Isabelle/HOL定理证明

所属期刊栏目：44

分类号：TP311(计算技术、计算机技术)

资助基金：国家重点研发计划项目:协同精密定位技术2016YFB0501900;国家重点基础研究发展计划“973”计划基金2012CB315900

在线出版日期：2017-11-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：134-141