Computer Science ›› 2017, Vol. 44 ›› Issue (10): 134-141.doi: 10.11896/j.issn.1002-137X.2017.10.026
Previous Articles Next Articles
ZHU Xian-wei, ZHU Zhi-qiang and SUN Lei
[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! |
|