The Study on Formal Verification of OS Kernel
Автор: Zhang Yu, Dong Yunwei, Zhang Zhongqiu, Huo Hong, Zhang Fan
Журнал: International Journal of Wireless and Microwave Technologies(IJWMT) @ijwmt
Статья в выпуске: 3 Vol.1, 2011 года.
Бесплатный доступ
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.
OS kernel, formal verification, theorem proving, model checking
Короткий адрес: https://sciup.org/15012745
IDR: 15012745
Список литературы The Study on Formal Verification of OS Kernel
- RTCA/DO-178B. Software Considerations in Airborne Systems and Equipment Certification[S]. Requirements and Technical Concepts for Aviation (RTCA), Dec. ,1992
- US National Institute of Standards. Common Criteria or IT Security Evaluation, 1999. ISO Standard 15408. http://www.niap-ccevs.org/cc-scheme/
- 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).
- S.Graf and H.Saidi. Construction of abstract state graphs with PVS. CAV 97: Computer-aided Verification, LNCS 1254 , 72-83. 1997.
- 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
- 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
- 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
- C A R Hoare. An axiomatic basis for computer programming [J].Communications of the ACM,1969;12(10):576-580
- Yanfang Ren, Jing Yang, Bingrui Suo,Checking method based on program correctness, Computer Engineering and Design. 2009,30 (17)(in Chinese)
- Y Bertot, P Casteran. Coq'Art:The Calculus of Inductive Constructions[M].Berlin: Springer- Verlag, 2004.
- Thomas A.Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre,Software Verification with BLAST. 10th Int SPIN Workshop (SPIN'2003).
