Paper Info
Title
End-to-End Automated Verification for OS Kernels
Abstract
Formal verification has been recognized as an essential part in improving the correctness and soundness of OS kernels. The verification of OS kernels faces many challenges. For example, the formal proof always comes with difficulties and non-trivial cost. Researchers often have to verify the OS kernel in high level programming languages and ignore low level languages. In this paper, we propose a framework for verifying the whole OS kernel with a low proof burden. We claim it as an end-to-end automated verification framework for the purposes of: (1) verifying the OS kernel that consists of assembler and C languages by formally modeling assembler programs in C level; (2) reasoning the verification with no manual proofs on the basis of SMT. We successfully apply the framework to automatic verifying a commercial operating system µC/OS-II in different hardware architecture, including all the 74 system calls and the core written in mixed-language (i.e., assembler and C). Our framework helps to catch several overflows and type mismatch vulnerabilities of µC/OS-II kernel.
Year
DOI
Venue
2018
10.1109/APSEC.2018.00028
2018 25th Asia-Pacific Software Engineering Conference (APSEC)
Keywords
Field
DocType
Kernel,High level languages,Cognition,C languages,Contracts,Data structures
Computer science,End-to-end principle,Real-time computing,Operating system
Conference
ISSN
ISBN
Citations 
1530-1362
978-1-7281-1970-0
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Jizheng Ding100.34
Xiaoran Zhu201.35
Jian Guo322.06