你好,游客 登录
背景:
阅读新闻

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

[日期:2017-10-23] 来源:计算机科学  作者:祝现威 朱智强 孙磊 [字体: ]

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

祝现威 朱智强 孙磊

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


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

 

推荐 打印 | 录入:Cstor | 阅读:
相关新闻      
本文评论   
评论声明
  • 尊重网上道德,遵守中华人民共和国的各项有关法律法规
  • 承担一切因您的行为而直接或间接导致的民事或刑事法律责任
  • 本站管理人员有权保留或删除其管辖留言中的任意内容
  • 本站有权在网站内转载或引用您的评论
  • 参与本评论即表明您已经阅读并接受上述条款