VSOS­HAM：基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

南京大学学报(自然科学版) ›› 2017, Vol. 53 ›› Issue (3): 579–.

VSOSHAM：基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

钱振江1，2*，黄　皓2，宋方敏2

出版日期:2017-05-30 发布日期:2017-05-30
作者简介: 1.常熟理工学院计算机科学与工程学院，苏州，215500；2.南京大学软件新技术国家重点实验室，南京，210023
基金资助:
基金项目：国家自然科学基金(61402057)，江苏省科技计划自然科学研究项目(BK20140418)，中国博士后科学基金(2015M571737)，江苏省高校“青蓝工程”优秀青年骨干教师培养对象项目(2017)
收稿日期：2015－09－06
*通讯联系人，Email：zhenjiang.qian@gmail.com

SOSHAM：Research on Isabelle/HOLbased OS kernel hardware abstract model and formal verification method

Qian Zhenjiang1，2*，Huang Hao2，Song Fangmin2

Online:2017-05-30 Published:2017-05-30
About author: 1.School of Computer Science and Engineering，Changshu Institute of Technology，Suzhou，215500，China；
2．State Key Laboratory for Novel Software Technology，Nanjing University，Nanjing，210023，China

摘要/Abstract

摘要： 形式化方法是保证操作系统设计和实现的正确性的可靠方法．操作系统的形式化设计和验证过程仍然是一个极其复杂的过程．由于汇编语言过于底层，对其进行形式化验证的难度较大，如何有效地对汇编语言代码进行建模，便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点．在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法．通过建立操作系统内核硬件抽象模型，形式化地描述指令的操作语义，在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象，建立系统状态空间，结合指令的操作语义的定义来描述系统的状态转换函数．在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型，以实现的可信操作系统VSOS为例，在汇编级对系统设计和实现的正确性进行验证．结果表明，该方法是可行的和高效的．

Abstract: The formal method is a reliable one to ensure the correctness of design and implementation of operating system.The formal design and verification of operating system is still an extremely complex progress.Because of its lowlevel，it is difficult to validate the correctness of the assembly layer.How to effectively model for assembly codes，and easily validate the correctness of the semantics and effectiveness becomes a hot topic in the field of operating system formalization.In this paper，we present the method of formal verification of design and implementation of operating system on the assembly layer.We construct the kernel hardware abstract model of operating system，and describe the operational semantics of instructions.Based on this abstract model，we define the data objects affecting the system state，and establish the system state domain.With the description of operational semantics of instructions，we describe the transition functions of system states.Meanwhile，we define the constructed kernel hardware abstract model of operating system in Isabelle/HOL theorem prover，and take the selfimplemented trusted operating system(VSOS)as the example to validate the correctness of the design and implementation of system on the assembly layer.The result shows that the proposed method is feasible and efficient.

钱振江1，2*，黄　皓2，宋方敏2. VSOSHAM：基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究[J]. 南京大学学报(自然科学版), 2017, 53(3): 579–.

Qian Zhenjiang1，2*，Huang Hao2，Song Fangmin2. SOSHAM：Research on Isabelle/HOLbased OS kernel hardware abstract model and formal verification method[J]. Journal of Nanjing University(Natural Sciences), 2017, 53(3): 579–.

参考文献

[1]　Clarke E M，Grumberg O，Peled D．Model checking.Cambridge：The MIT Press，1999，4－5.
[2] Doron R，Patiizio R，Paola S．Model checking.New York：Wley Encyclopedia of Computer Science and Engineering，2009，1904－1920.
[3] Secure Computing Corporation.DTOS formal security policy model.Technical Report.DTOS CDRL，Secure Computing Corporation，1996.
[4] Bevier W R．KIT：A study in operating system verification.Technical Report.Computational Logic Inc.，Austin，USA，1988.
[5] The Verisoft XT Consortium.The verisoft xt project.http：//www.verisoftxt.de/，2014－11－03.　
[6] Klein G，Andronick J，Elphinstone K，et al.Comprehensive formal verification of an OS microkernel.ACM Transactions on Computer Systems，2014，32(1)：1－70.
[7] Yale Flint Project.Yale Flint Website.http：//flink.cs.yale.edu/，2014－11－03.
[8] Stampoulis A．VeriML：A dependentlytyped，userextensible，and languagecentric approach to proof assistant.Ph.D.Dissertation.New Haven：Yale University，2012.
[9] Li Z P，Zhang Y，Chen Y Y．A shape graph logic and a shape system.Journal of Computer Science and Technology，2013，28(6)：1063－1084.
[10] Liang H J，Feng X Y，Shao Z．Compositional verification of terminationpreserving refinement of concurrent programs.In：The 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science(CSLLICS’14)．New York，USA：ACM，Article No.65，2014.
[11] 钱振江，黄　皓，宋方敏．操作系统形式化设计与安全需求的一致性验证研究．计算机学报，2014，37(5)：1082－1099.(Qian Z J，Huang H，Song F M．Research on consistency verification of formal design and security requirements for operating system.Chinese Journal of Computers，2014，37(5)：1082－1099.)
[12] 钱振江．验证安全操作系统VSOS.软件著作权：2014SR080422.2014－02－17.
[13] Nipkow T，Paulson L C，Wenzel M T．Isabelle/HOL：A proof assistant for higherorder logic.Springer，2002，1－226.
[14] Klein G．Operating System verification － An overview.Sadhana，2009，34(1)：27－69.
[15] Hoare C A R．An axiomatic basis for computer programming.Communications of the ACM，1969，12(10)：576－580.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed