International Journal of Computer Network and Information Security (IJCNIS)
IJCNIS Vol. 2, No. 2, 8 Dec. 2010
Cover page and Table of Contents: PDF (size: 240KB)
Author(s)
Yu Zhang
1,*
Yunwei Dong
1
Huo Hong
1
Fan Zhang
1
Index Terms
Formal verification, theorem proving, model checking, system code
Abstract
With the increasing pressure on non-function attributes (security, safety and reliability) requirements of an operation system, high–confidence operation system is becoming more important. Formal verification is the only known way to guarantee that a system is free of programming errors. We research on formal verification of operation system kernel in system code 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 code 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
Yu Zhang, Yunwei Dong, Huo Hong, Fan Zhang, "Code Formal Verification of Operation System", International Journal of Computer Network and Information Security(IJCNIS), vol.2, no.2, pp.10-18, 2010. DOI:10.5815/ijcnis.2010.02.02
Reference
[1] G. Klein. Operating system verification — an overview. Sadhana, 34(1):27–69, Feb 2009.
[2] H. Tuch, G. Klein, and G. Heiser. OS verification —now! In 10th HotOS, pages 7–12. USENIX, Jun 2005.
[3] RTCA/DO-178B. Software Considerations in Airborne Systems and Equipment Certification[S]. Requirements and Technical Concepts for Aviation (RTCA), Dec,1992.
[4] US National Institute of Standards. Common Criteria or IT Security Evaluation, 1999. ISO Standard 15408. http://www.niap-ccevs.org/cc-scheme/.
[5] Georg Rock, Gunter Lassmann, Mathias Schwan, Lassaad Cheikhrouhou. Verisoft-Secure Biometric Identification System.Springer Verlag Berlin Heidellberg.2008.
[6] Schirmer N. A verification environment for sequential imperative programs in Isabelle/HOL. In: F Baader, A Voronkov, (eds), 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR04), Vol. 3452 of Lecture Notes in Computer Science, Springer-Verlag 398–414. 2004.
[7] L.C.Paulson, Isabelle:A Generic Theorem Prover. LNCS 828, 1994.
[8] 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).
[9] Harvey Tuch, Gerwin Klein and Michael Norrish. Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007.
[10] S.Graf and H.Saidi. Construction of abstract state graphs with PVS. CAV 97: Computer-aided Verification, LNCS 1254, 72-83. 1997.
[11] E.M.Clarke, O.Grumberg, S.Jha, Y.Lu and H.Veith. Counterexample-guided abstraction refinement. In Preceedings of CAV. Springer LNCS 1855, 154-169. 2000.
[12] 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.
[13] 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.
[14] 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.
[15] C A R Hoare. An axiomatic basis for computer programming [J].Communications of the ACM,1969;12(10):576-580.
[16] Yanfang Ren, Jing Yang, Bingrui Suo,Checking method based on program correctness, Computer Engineering and Design. 2009,30 (17)(in Chinese).
[17] Y Bertot, P Casteran. Coq'Art:The Calculus of Inductive Constructions[M].Berlin: Springer- Verlag, 2004.
[18] Thomas A.Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre,Software Verification with BLAST. 10th Int SPIN Workshop (SPIN'2003).
[19] G.J.Holzmann, The Spin Model Checker. IEEE Transactions on Software Engineering 23(5), 279-295 (1997).
[20] R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple onthe-fly automatic verification of linear temporal logic. In IFIP/WG 6.1, 1995.
[21] Salamah Salamah, Ann Q. Gates, Steve Roach Gates, A.Q. ; Roach, S. Improving Pattern-Based LTL Formulas for Automata Model Checking. Fifth International Conference on Information Technology: New Generations.2008.
[22] Jean J.Labrosse, Micro -The Real-Time Kernel Second Edition. CMP Books, 2005.6.