A Practical Verification Framework for Preemptive OS Kernels Fengwei Xul.2,Ming Ful2(),Xinyu Feng1.2,Xiaoran Zhangl.2,Hui Zhang1.2, and Zhaohui Lil.2 1 School of Computer Science and Technology, University of Science and Technology of China, Hefei,China fuming@ustc.edu.cn en 2 Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou,China Abstract.We propose a practical verification framework for preemptive OS kernels.The framework models the correctness of API implementa- tions in OS kernels as contextual refinement of their abstract specifi- cations.It provides a specification language for defining the high-level abstract model of OS kernels,a program logic for refinement verifica- tion of concurrent kernel code with multi-level hardware interrupts,and automated tactics for developing mechanized proofs.The whole frame- work is developed for a practical subset of the C language.We have successfully applied it to verify key modules of a commercial preemptive OS uC/OS-II [2],including the scheduler,interrupt handlers,message queues,and mutexes etc.We also verify the priority-inversion-freedom (PIF)in uC/OS-II.All the proofs are mechanized in Coq.To our knowl- edge,our work is the first to verify the functional correctness of a prac- tical preemptive OS kernel with machine-checkable proofs. 1 Introduction Verifying OS kernels has long been recognized as an important but also extremely challenging task.There have been exciting efforts for OS kernel verification [4,13,16,27]in recent years,but most of them have no or limited support of kernel-level preemption,which allows tasks to be preempted even in kernel mode. This limitation restricts their applicability to real-time systems,where preemp- tive multitasking is indispensable to achieve real-time guarantees. Preemptive kernels require explicit invocation of schedulers inside interrupt handlers and careful interrupt management in the kernel code,which make the kernel highly concurrent and complex.In this paper we propose a verification framework for preemptive OS kernels,and show its application in verifying key modules of uC/OS-II [2],a commercial preemptive real-time multitasking kernel for microprocessors and microcontrollers.The verification is fully mechanized This work is supported in part by grants from National Natural Science Foundation of China(NSFC)under Grant Nos.61103023,61229201,61379039 and 91318301. C Springer International Publishing Switzerland 2016 S.Chaudhuri and A.Farzan (Eds.):CAV 2016,Part II,LNCS 9780,pp.59-79,2016. D0:10.1007/978-3-319-41540-6-4A Practical Verification Framework for Preemptive OS Kernels Fengwei Xu1,2, Ming Fu1,2(B), Xinyu Feng1,2, Xiaoran Zhang1,2, Hui Zhang1,2, and Zhaohui Li1,2 1 School of Computer Science and Technology, University of Science and Technology of China, Hefei, China fuming@ustc.edu.cn 2 Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, China Abstract. We propose a practical verification framework for preemptive OS kernels. The framework models the correctness of API implementa￾tions in OS kernels as contextual refinement of their abstract specifi- cations. It provides a specification language for defining the high-level abstract model of OS kernels, a program logic for refinement verifica￾tion of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mechanized proofs. The whole frame￾work is developed for a practical subset of the C language. We have successfully applied it to verify key modules of a commercial preemptive OS μC/OS-II [2], including the scheduler, interrupt handlers, message queues, and mutexes etc. We also verify the priority-inversion-freedom (PIF) in μC/OS-II. All the proofs are mechanized in Coq. To our knowl￾edge, our work is the first to verify the functional correctness of a prac￾tical preemptive OS kernel with machine-checkable proofs. 1 Introduction Verifying OS kernels has long been recognized as an important but also extremely challenging task. There have been exciting efforts for OS kernel verification [4,13,16,27] in recent years, but most of them have no or limited support of kernel-level preemption, which allows tasks to be preempted even in kernel mode. This limitation restricts their applicability to real-time systems, where preemp￾tive multitasking is indispensable to achieve real-time guarantees. Preemptive kernels require explicit invocation of schedulers inside interrupt handlers and careful interrupt management in the kernel code, which make the kernel highly concurrent and complex. In this paper we propose a verification framework for preemptive OS kernels, and show its application in verifying key modules of μC/OS-II [2], a commercial preemptive real-time multitasking kernel for microprocessors and microcontrollers. The verification is fully mechanized This work is supported in part by grants from National Natural Science Foundation of China (NSFC) under Grant Nos. 61103023, 61229201, 61379039 and 91318301. c Springer International Publishing Switzerland 2016 S. Chaudhuri and A. Farzan (Eds.): CAV 2016, Part II, LNCS 9780, pp. 59–79, 2016. DOI: 10.1007/978-3-319-41540-6 4