操作系统形式化设计与验证综述

doi:10.3969/j.issn.1000-3428.2012.11.072

计算机工程 ›› 2012, Vol. 38 ›› Issue (11): 234-238. doi: 10.3969/j.issn.1000-3428.2012.11.072

操作系统形式化设计与验证综述

钱振江^a,b，刘苇^a,b，黄皓^a,b

(南京大学 a. 软件新技术国家重点实验室；b. 计算机科学与技术系，南京 210046)

收稿日期:2011-10-15 出版日期:2012-06-05 发布日期:2012-06-05
作者简介:钱振江(1982－)，男，讲师、博士研究生，主研方向：操作系统安全，形式化验证，嵌入式系统；刘苇，硕士研究生；黄皓，教授、博士、博士生导师
基金资助:
国家“863”计划基金资助项目“分布式可信计算系统研究”(2007AA01Z409)；国家自然科学基金资助项目(60721002)；江苏省科技支撑计划基金资助项目“可信操作系统新技术研发”(BE2008124)

Survey of Formal Design and Verification for Operating System

QIAN Zhen-jiang ^a,b, LIU Wei ^a,b, HUANG Hao ^a,b

(a. State Key Laboratory for Novel Software Technology; b. Department of Computer Science and Technology, Nanjing University, Nanjing 210046, China)

Received:2011-10-15 Online:2012-06-05 Published:2012-06-05

摘要/Abstract

摘要： 对操作系统的形式化设计和验证的概念进行介绍，描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构，调查多个设计和验证项目，阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上，分析和展望操作系统形式化设计和验证的发展趋势，从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路。

关键词: 操作系统, 形式化设计, 形式化验证, 定理证明, 系统安全, 框架设计

Abstract: This paper introduces the concepts of formal design and verification for the Operating System(OS), and elaborates the framework and foundational methods of formal design and verification. It compares and analyzes the monolithic kernel and micro kernel architectures of the OS. Meanwhile, it investigates multiple design and verification projects in depth, focusing on the verification objectives, the methodology, the advantages and limitations, and the progression. It summarizes the state of the art, analyzes and outlooks the trends of the formal design and verification for the OS. What is more, from the aspects of model design, verification tools, code implementation and verification reuse, it advances the ideas of formal design and verification.

Key words: Operating System(OS), formal design, formal verification, theorem proving, system security, architecture design

中图分类号:

TP316

钱振江, 刘苇, 黄皓. 操作系统形式化设计与验证综述[J]. 计算机工程, 2012, 38(11): 234-238.

JIAN Zhen-Jiang, LIU Wei, HUANG Hao. Survey of Formal Design and Verification for Operating System[J]. Computer Engineering, 2012, 38(11): 234-238.

http://www.ecice06.com/CN/Y2012/V38/I11/234

参考文献

[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.

选择文件类型/文献管理软件名称

选择包含的内容

操作系统形式化设计与验证综述

Survey of Formal Design and Verification for Operating System

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	王法臻, 崔少辉, 王成. 基于Linux的PXIe可重构仪器设备驱动程序开发[J]. 计算机工程, 2021, 47(4): 166-172.
[2]	夏锐, 钱振江, 刘苇. 一种基于Isabelle/HOL的安全通信协议验证方法[J]. 计算机工程, 2021, 47(1): 146-153.
[3]	欧阳恒一, 熊焰, 黄文超. 一种代币智能合约的形式化建模与验证方法[J]. 计算机工程, 2020, 46(10): 41-45,51.
[4]	欧阳湘臻, 朱怡安, 李联, 史先琛. 一种安全关键的嵌入式实时操作系统内核设计[J]. 计算机工程, 2019, 45(7): 78-85.
[5]	何相甫, 范志辉, 王辉, 翟智博, 李静. IPv6与ZigBee互联网关的设计与实现[J]. 计算机工程, 2019, 45(7): 154-158.
[6]	孟子琪,张倩颖,施智平,关永. 基于可信执行环境的嵌入式双操作系统架构研究[J]. 计算机工程, 2019, 45(4): 6-12.
[7]	钟建, 徐扬, 陈树伟, 何星星. 一阶逻辑中基于稳定度的项评估方法[J]. 计算机工程, 2019, 45(11): 183-190,197.
[8]	林荣峰, 施健, 朱晏庆, 沈怡颹, 周宇. 基于STP方法的SCADE模型形式化验证框架[J]. 计算机工程, 2019, 45(10): 70-77.
[9]	祁龙云, 吕小亮, 路红, 黄皓. 汇编级顺序语句块的自动形式化规约及其验证[J]. 计算机工程, 2019, 45(10): 64-69,77.
[10]	李堃,张雪松. STP安全通信协议设计与形式化验证[J]. 计算机工程, 2018, 44(12): 120-128.
[11]	朱怡安,黄林林,李联,罗殊彦. 多核平台下分区操作系统的安全关键任务调度方法[J]. 计算机工程, 2017, 43(12): 38-44.
[12]	张锋,朱振荣,史胜伟. 一种高速免驱USB加密卡的设计与实现[J]. 计算机工程, 2017, 43(11): 292-296,302.
[13]	李青,朱晓冉,郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1): 79-85.
[14]	彭展,梁根,周炳. 电信服务系统特征交互的Z规格及验证[J]. 计算机工程, 2016, 42(8): 19-23.
[15]	杨世瀚,吴尽昭,丁广泓,秦董洪. 模拟与混合信号电路的形式化验证[J]. 计算机工程, 2016, 42(8): 34-38,45.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

操作系统形式化设计与验证综述

Survey of Formal Design and Verification for Operating System

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价