Computer Science ›› 2017, Vol. 44 ›› Issue (10): 134-141.doi: 10.11896/j.issn.1002-137X.2017.10.026

Previous Articles     Next Articles

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

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   
No Suggested Reading articles found!