计算机科学 ›› 2017, Vol. 44 ›› Issue (10): 134-141.doi: 10.11896/j.issn.1002-137X.2017.10.026

• 信息安全 • 上一篇    下一篇

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

祝现威,朱智强,孙磊   

  1. 中国人民解放军信息工程大学密码工程学院 郑州450004,中国人民解放军信息工程大学密码工程学院 郑州450004,中国人民解放军信息工程大学密码工程学院 郑州450004
  • 出版日期:2018-12-01 发布日期:2018-12-01
  • 基金资助:
    本文受国家重点研发计划项目:协同精密定位技术(2016YFB0501900),国家重点基础研究发展计划(“973”计划)基金(2012CB315900)资助

Design and Formal Verification of Xen Hybrid Multi-police Model

ZHU Xian-wei, ZHU Zhi-qiang and SUN Lei   

  • Online:2018-12-01 Published:2018-12-01

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

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

Abstract: 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.

Key words: SV_HMPMD,Semantic model,Formal proof,Theorem proving of Isabelle/HOL

[1] SAILER R,VALDEZ E,JAEGER T,et al.sHype:Secure hypervisor approach to trusted virtualized systems[J].IBM Research Report Rc,2005,9(2):331-352.
[2] REITAS L,MCDERMOTT J.Formal methods for security in the Xenon hypervisor[J].International Journal on Software Tools for Technology Transfer,2011,13(5):463-489.
[3] RUTKOWSKA J,WOJTCZUK R.Qubes OS Architecture.Version 0.3.http://www.qubes-os.org/attachment/wiki/QubesArchtecture/arch-spec-0.3.pdf.
[4] RUTKOWSKA J,WOJTCZUK R.Qubes OS Architecture.http://burrough.org/Documents/Qubes_OS_Architecture.pdf.
[5] WENG C L,LUO Y,LI M,et al.A BLP-Based Access Control Mechanism for the Virtual Machine System[C]∥ International Conference for Young Computer Scientists(Icycs 2008).Zhangjiajie,Hunan,China,2008:2278-2282.
[6] MA M,TANG Z,LI R F,et al.Improved BLP Model Based on CRFs[J].Computer Science,2015,2(8):138-144.(in Chinese) 马萌,唐卓,李仁发,等.基于条件随机场的改进型BLP访问控制模型[J].计算机科学,2015,42(8):138-144.
[7] KUHN R.Role Based Access Control on MLS Systems without Kernel Changed[C]∥Proceedings of the ACM Workshop on Role Based Access Control.ACM,1998.
[8] WEI M L,ZHANG M Q,TANG J,et al.Formal Modeling of Complex Network Security Based on MAS[J].Computer Science,2015,42(3):102-105.(in Chinese) 危美林,张明清,唐俊,等.基于MAS的复杂网络安全形式化建模[J].计算机科学,2015,42(3):102-105.
[9] QIAN Z J,LIU W,HUANG H.OSOSM:Operating System Object Semantics Model and Formal Verification[J].Journal of Computer Research and Development,2012,9(12):2702-2712.(in Chinese) 钱振江,刘苇,黄皓.操作系统对象语义模型(OSOSM)及形式化验证[J].计算机研究与发展,2012,49(12):2702-2712.
[10] 屈延文.形式语义学基础与形式说明[M].北京:科学出版社,2009.
[11] CˇAR O,POPESCU A.A Consistent Foundation for Isabelle/HOL[C]∥ ITP.2015:234-252.
[12] ELPHINSTONE K,HEIESER G.From L3 to seL4 what have we learnt in 20 years of L4 microkernels?[C]∥ Twenty-Fourth ACM Symposium on Operating Systems Principles.2013:133-150.
[13] NIPKOW T,PAULSON L C,WENZEL M.Isabelle/HOL:aproof assistant for higher-order logic[M].Springer Science & Business Media,2002.
[14] KINGHT G.LinSec-Linux Security Protection System[EB/OL].http://www.linsec.org/doc/final.pdf.
[15] 佩莱德.软件可靠性方法[M].北京:机械工业出版社,2012.
[16] CALZAVARA S,RABITTI A,BUGLIESI M.Formal Verification of Liferay RBAC[M]∥Engineering Secure Software and Systems.Springer International Publishing,2015:1-16.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75, 88 .
[2] 夏庆勋,庄毅. 一种基于局部性原理的远程验证机制[J]. 计算机科学, 2018, 45(4): 148 -151, 162 .
[3] 厉柏伸,李领治,孙涌,朱艳琴. 基于伪梯度提升决策树的内网防御算法[J]. 计算机科学, 2018, 45(4): 157 -162 .
[4] 王欢,张云峰,张艳. 一种基于CFDs规则的修复序列快速判定方法[J]. 计算机科学, 2018, 45(3): 311 -316 .
[5] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[6] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[7] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[8] 刘琴. 计算机取证过程中基于约束的数据质量问题研究[J]. 计算机科学, 2018, 45(4): 169 -172 .
[9] 钟菲,杨斌. 基于主成分分析网络的车牌检测方法[J]. 计算机科学, 2018, 45(3): 268 -273 .
[10] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99, 116 .