Zhang Yufeng; Dong Yunwei; Zhang Zhongqiu; Huo Hong; Zhang Fan

The Study on Formal Verification of OS Kernel

Full Text (PDF, 103KB), PP.62-69

Views: 0 Downloads: 0

Author(s)

Zhang Yufeng ^1,* Dong Yunwei ¹ Zhang Zhongqiu ¹ Huo Hong ¹ Zhang Fan ¹

1. Northwestern Polytechnical University, Xi’an, China

* Corresponding author.

DOI: https://doi.org/10.5815/ijwmt.2011.03.10

Received: 15 Feb. 2011 / Revised: 24 Mar. 2011 / Accepted: 10 May 2011 / Published: 15 Jun. 2011

Index Terms

OS kernel, formal verification, theorem proving, model checking

Abstract

There is increasing pressure on providing a high degree of assurance of operation system’s security and functionality. Formal verification is the only known way to guarantee that a system is free of programming errors. We study on formal verification of operation system kernel in system implementation level and take theorem proving and model checking as the main technical methods to resolve the key techniques of verifying operation system kernel in C implementation level. We present a case study to the verification of real-world C systems code derived from an implementation of μC/OS – II in the end.

Cite This Paper

Zhang Yu,Dong Yunwei,Zhang Zhongqiu,Huo Hong,Zhang Fan,"The Study on Formal Verification of OS Kernel", IJWMT, vol.1, no.3, pp.62-69, 2011. DOI: 10.5815/ijwmt.2011.03.10

Reference

[1] RTCA/DO-178B. Software Considerations in Airborne Systems and Equipment Certification[S]. Requirements and Technical Concepts for Aviation (RTCA), Dec. ,1992

[2] US National Institute of Standards. Common Criteria or IT Security Evaluation, 1999. ISO Standard 15408. http://www.niap-ccevs.org/cc-scheme/

[3] Gerwin Klein, June Andronick, Kevin Elphinstone, et al. seL4: Formal verification of an OS kernel. Communications of the ACM, 53(6), 107–115, (June, 2010).

[4] S.Graf and H.Saidi. Construction of abstract state graphs with PVS. CAV 97: Computer-aided Verification, LNCS 1254 , 72-83. 1997.

[5] Necula1 G. Proof-carrying code [C]. In: Proc of the 24th ACM SIGPLAN-SIGACT Symp on Principles of Programming Language (POPL’97) .New York : ACM Press , 1997.106 -119

[6] Apple A W. Foundational proof-carrying code[C]. Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science. Baston, Massachusetts. USA,2001:247-258

[7] Dachuan Yu , N A Hamid , Zhong Shao. Building certified libraries for PCC: Dynamic storage allocation [J ]. Science of Computer Program , 2004 , 50 (1-3) : 101 – 127

[8] C A R Hoare. An axiomatic basis for computer programming [J].Communications of the ACM,1969;12(10):576-580

[9] Yanfang Ren, Jing Yang, Bingrui Suo,Checking method based on program correctness, Computer Engineering and Design. 2009,30 (17)(in Chinese)

[10] Y Bertot, P Casteran. Coq'Art:The Calculus of Inductive Constructions[M].Berlin: Springer- Verlag, 2004.

[11] Thomas A.Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre,Software Verification with BLAST. 10th Int SPIN Workshop (SPIN'2003).

International Journal of Wireless and Microwave Technologies (IJWMT)