[1] Clarke E M, Grumberg O, Peled D. Model Checking[M]. Cambridge, USA: The MIT Press, 1999. [2] Guenthner F. Handbook of Philosophical Logic[M]. Berlin, Germany: Springer, 2007. [3] 周巢尘. 形式语义学引论[M]. 长沙: 湖南科学技术出版社, 1985. [4] Tanenbaum A S. The Minix Project[EB/OL]. [2011-03-12]. http:// www.minix3.org/. [5] Rashid R, Julin D, Orr D, et al. Mach: A System Software Kernel[C]//Proc. of COMPCON’89. San Francisco, USA: [s. n.], 1989: 176-189. [6] Liedtke J. On μ-kernel Construction[C]//Proc. of SOSP’95. New York, USA: ACM Press, 1995: 237-250. [7] D?renb?cher J. Vamos Microkernel: Formal Models and Verifica- tion[EB/OL]. [2011-03-12]. http://www.cse.unsw.edu.au/~formal methods/events/svws-06/VAMOS_Microkernel.pdf. [8] Geeknet, Inc. Root Exploit for NVIDIA Closed-source Linux Driver[EB/OL]. [2011-03-12]. http://it.slashdot.org/article.pl?sid= 06/10/16/2038253. [9] SecurityFocus. Vulnerabilities Web Site[EB/OL]. [2011-03-12]. http://www.securityfocus.com/vulnerabilities. [10] DiBona C, Ockman S, Stone M. Open Sources: Voices from the Open Source Revolution[M]. Sebastopol, USA: O’Reilly Media, Inc., 2008. [11] Leslie B, Chubb P, Fitzroy-Dale N, et al. User-level Device Drivers: Achieved Performance[J]. Journal of Computer Science and Technology, 2005, 20(5): 654-664. [12] McCarty B. SELinux: NSA’s Open Source Security Enhanced Linux[M]. Sebastopo, USA: O’Reilly Media, Inc., 2004. [13] 卿斯汉, 朱继峰. 安胜安全操作系统的隐蔽通道分析[J]. 软件学报, 2004, 15(9): 1385-1392. [14] 卿斯汉. 高安全等级安全操作系统的隐蔽通道分析[J]. 软件学报, 2004, 15(12): 1837-1849. [15] Walker B J, Kemmerer R A, Popek G J. Specification and Verification of the UCLA Unix Security Kernel[J]. Communications of the ACM, 1980, 23(2): 118-131. [16] SRI International. SRI Project[EB/OL]. [2011-03-12]. http://www. sri.com. [17] Robinson L, Roubine O. Special: A Specification and Assertion Language[M]. [S. l.]: Stanford Research Institute, 1977. [18] Secure Computing Corp. DTOS Formal Security Policy Model[EB/OL]. (1996-09-26). http://www.cs.utah.edu/flux/fluke/ html/dtos/HTML/final-docs/fspm.pdf. [19] Bevier W R. A Verified Operating System Kernel[D]. Austin, USA: University of Texas, 1987. [20] Shapiro J S, Smith J M, Farber D J. EROS: A Fast Capability System[C]//Proc. of SOSP’99. New York, USA: ACM Press, 1999: 170-185. [21] Shapiro J S, Sridhar S, Doerrie M S. BitC Language Specifica- tion[EB/OL]. [2011-03-12]. http://coyotos.org/docs/bitc/spec.html. [22] The EROS Group. Coyotos Project[EB/OL]. [2011-03-12]. http:// www.coyotos.org. [23] Hohmuth M, Tews H, Stephens S G. Applying Source-code Verification to a Microkernel: the VFiasco Project[C]//Proc. of the 10th Workshop on ACM SIGOPS. New York, USA: ACM Press, 2002. [24] Owre S, Rushby J M, Shankar N. PVS: A Prototype Verification System[C]//Proc. of CADE’92. [S. l.]: Springer, 1992. [25] Tews H, Weber T, V?lp M, et al. Nova Micro-hypervisor Verification Formal, Machine-checked Verification of One Module of the Kernel Source Code[D]. Nijmegen, Holland: Radboud University, 2008. [26] ROBIN Consortium. Robin Project[EB/OL]. [2011-03-12]. http:// robin.tudos.org. [28] Tews H. Micro Hypervisor Verification: Possible Approaches and Relevant Properties[EB/OL]. [2011-03-12]. http://robin.tudos.org/ publications/hyperveri.pdf. [28] Liedtke J, Dannowski U, Elphinstone K, et al. The l4ka Vision[EB/OL]. [2011-03-12]. http://www.cis.upenn.edu/~ahae/ papers/L4Ka.pdf. [29] Nipkow T, Paulson L C. Isabelle/HOL: A Proof Assistant for Higher-order Logic[M]. Berlin, Germany: Springer, 2002. [30] Tuch H, Klein G. Verifying the L4 Virtual Memory Subsystem[C]// Proc. of NICTA Formal Methods Workshop on Operating Systems Verification. Sydney, Australia: [s. n.], 2004: 73-97. [31] Elkaduwe D, Klein G, Elphinstone K. Verified Protection Model of the SeL4 Microkernel[EB/OL]. [2011-03-12]. http://ertos.nicta. com.au/publications/papers/Elkaduwe_GE_07.pdf. [32] Flint Group. Yale Flint Project[EB/OL]. [2011-03-12]. http://flint. cs.yale.edu/. [33] Stampoulis A, Shao Z. VeriML: Typed Computation of Logical Terms Inside a Language with Effects[C]//Proc. of ICFP’10. New York, USA: ACM Press, 2010. [34] Robinson A, Voronkov A. Handbook of Automated Reasoning[M]. Amsterdam, Holland: Elsevier, 1999. [35] Feng Xinyu. An Open Framework for Certified System Software[D]. New Haven, USA: Yale University, 2007. [36] Shao Z, Ford B. Advanced Development of Certified OS Kernels[D]. New Haven, USA: Yale University, 2010. [37] The Verisoft XT Consortium. The Verisoft XT Project[EB/OL]. [2011-03-12]. http://www.verisoftxt.de/. [38] Beyer S, Jacobi C, Kroening D, et al. Putting it All Together: Formal Verification of the VAMP[J]. International Journal on Software Tools for Technology Transfer, 2006, 8(4-5): 411-430. [39] Hillebrand M A, Rieden T I, Paul W J. Dealing with I/O Devices in the Context of Pervasive System Verification[C]//Proc. of International Conference on Computer Design. Las Vegas, USA: CSREA Press, 2005: 309-316. [40] Alkassar E, Hillebrand M, Rusev S K R, et al. Formal Device and Programming Model for a Serial Interface[C]//Proc. of VERIFY’04. Bremen, Germany: [s. n.], 2004: 4-20. [41] Rieden T I, Tsyban A. CVM: a Verified Framework for Microkernel Programmers[C]//Proc. of SSV’08. Amsterdam, Holland: Elsevier Science Publishers, 2008: 151-168. [42] Starostin A, Tsyban A. Correct Microkernel Primitives[C]//Proc. of SSV’08. Amsterdam, Holland: Elsevier Science Publishers, 2008: 169-185. [43] Bogan S. Formal Specification of a Simple Operating System[D]. Saarbrücken, Germany: Saarland University, 2008. [44] Beuster G, Henrich N, Wagner M. Real World Verification Experiences from the Verisoft Email Client[C]//Proc. of ESCoR’06. Seattle, USA: [s. n.], 2006: 112-115.
|