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-4
A 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 implementations 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 verification of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mechanized proofs. The whole framework 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 knowledge, our work is the first to verify the functional correctness of a practical 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 preemptive 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
60 F.Xu et al. in Coq [1].To our knowledge,it is the first verification of (key modules of)a preemptive OS kernel with machine-checkable proofs.The key contribution of the work is to adapt existing theories on interrupt verification [11]and contex- tual refinement of concurrent programs [17,19,24,25],and integrate them into a framework for real-world preemptive OS kernel verification.Specifically,our work makes the following new contributions: First,we formulate and verify the correctness of the APIs of OS ker- nels as contertual refinement between their implementations and specifications. Although refinement approaches have been applied in earlier work on OS kernel verification [4,13,16],we believe our work is the first to explicitly specify and prove contextual refinement for APIs of a preemptive OS kernel,following recent progress on refinement verification of concurrent programs [17,19,24,25].As we explain in Sect.2.2,contextual refinement not only serves as a very strong notion of functional correctness of system APIs,but also allows us to prove properties based on the more abstract API specifications and then carry it down to the level of concrete implementations,which makes the verification much simpler than doing proofs directly at the concrete level. Second,we provide a simple modeling language for specifying kernel prim- itives.The language strives for balance between abstraction and expressiveness for scheduling.On the one hand,we want the specification to abstract away implementation details.On the other hand,it should provide enough details so that many important properties can be specified at the abstract specification level.Our modeling language provides an abstract sched command,allowing us to specify explicitly when the scheduler is invoked in synchronization primi- tives or interrupt handlers.Semantics of sched is parameterized over abstract scheduling policies (e.g.,priority-based or round-robin).Expressiveness about these details are necessary to specify system-wide scheduling properties. Third,we propose a program logic for refinement verification of concurrent kernel programs.The logic supports multi-level nested hardware interrupts and configurable schedulers.It extends concurrent separation logic [21](CSL)with relational assertions that relate program states at the implementation and the specification levels,as in Liang et al.[17,19.It also assigns ownership-transfer semantics to interrupt management operations and verify multi-level hardware interrupts in a realistic setting.Different from traditional Hoare-style program logics,whose soundness ensures the semantic interpretation of Hoare-triples, our logic explicitly establishes contextual refinement,which is more useful for establishing abstractions for system APIs,as explained above. Fourth,our framework is developed for a practical subset of C.It has been successfully applied to verify key APIs of uC/OS-II [2],including the timer inter- rupt handler (and a pseudo interrupt handler to demonstrate the support of multi-level interrupts),the scheduler,the time management,and four synchro- nization mechanisms:message queues,mail boxes,semaphores,and mutexes. It is worth noting that,unlike existing works [4,13,16,27]that are focused on kernels newly developed with verification in mind,we take a commercial system developed by an independent third-party and verify the code with minimum mod- ification,which demonstrates the generality and applicability of our framework
60 F. Xu et al. in Coq [1]. To our knowledge, it is the first verification of (key modules of) a preemptive OS kernel with machine-checkable proofs. The key contribution of the work is to adapt existing theories on interrupt verification [11] and contextual refinement of concurrent programs [17,19,24,25], and integrate them into a framework for real-world preemptive OS kernel verification. Specifically, our work makes the following new contributions: First, we formulate and verify the correctness of the APIs of OS kernels as contextual refinement between their implementations and specifications. Although refinement approaches have been applied in earlier work on OS kernel verification [4,13,16], we believe our work is the first to explicitly specify and prove contextual refinement for APIs of a preemptive OS kernel, following recent progress on refinement verification of concurrent programs [17,19,24,25]. As we explain in Sect. 2.2, contextual refinement not only serves as a very strong notion of functional correctness of system APIs, but also allows us to prove properties based on the more abstract API specifications and then carry it down to the level of concrete implementations, which makes the verification much simpler than doing proofs directly at the concrete level. Second, we provide a simple modeling language for specifying kernel primitives. The language strives for balance between abstraction and expressiveness for scheduling. On the one hand, we want the specification to abstract away implementation details. On the other hand, it should provide enough details so that many important properties can be specified at the abstract specification level. Our modeling language provides an abstract sched command, allowing us to specify explicitly when the scheduler is invoked in synchronization primitives or interrupt handlers. Semantics of sched is parameterized over abstract scheduling policies (e.g., priority-based or round-robin). Expressiveness about these details are necessary to specify system-wide scheduling properties. Third, we propose a program logic for refinement verification of concurrent kernel programs. The logic supports multi-level nested hardware interrupts and configurable schedulers. It extends concurrent separation logic [21] (CSL) with relational assertions that relate program states at the implementation and the specification levels, as in Liang et al. [17,19]. It also assigns ownership-transfer semantics to interrupt management operations and verify multi-level hardware interrupts in a realistic setting. Different from traditional Hoare-style program logics, whose soundness ensures the semantic interpretation of Hoare-triples, our logic explicitly establishes contextual refinement, which is more useful for establishing abstractions for system APIs, as explained above. Fourth, our framework is developed for a practical subset of C. It has been successfully applied to verify key APIs of μC/OS-II [2], including the timer interrupt handler (and a pseudo interrupt handler to demonstrate the support of multi-level interrupts), the scheduler, the time management, and four synchronization mechanisms: message queues, mail boxes, semaphores, and mutexes. It is worth noting that, unlike existing works [4,13,16,27] that are focused on kernels newly developed with verification in mind, we take a commercial system developed by an independent third-party and verify the code with minimum modification, which demonstrates the generality and applicability of our framework
A Practical Verification Framework for Preemptive OS Kernels 61 Fifth,we also specify and verify priority inversion freedom (PIF)of uC/OS-II.PIF is a crucial property for real-time systems and is worth veri- fying in its own right.Moreover,since the specification and verification are done at the level of the abstract model (i.e.,specifications)of the kernel,they also help validate our model of system APIs.As we explain above,many important properties cannot be specified if the model is too weak or overly abstract. Coq proofs and a companion technical report are available at http://staff. ustc.edu.cn/~fuming/research/certiucos. 2 Background and Overview of Our Work 2.1 Preemptive OS Kernels and Interrupts In a preemptive OS kernel,execution of a task inside the kernel can be inter- rupted at any program point (unless interrupts are disabled).Then the control is switched to the interrupt handler.When the handler finishes,it may invoke the scheduler and switch the execution context to a different task,instead of return- ing to the original interrupted task.For instance,with priority-based scheduling, the interrupt handler always switches to the highest priority task at its end. The x86 Interrupt Mechanism.Interrupt handling and management are indis- pensable in preemptive OS kernels.We give an overview of the interrupt mech- anism in x86 systems (based on the Intel 8259 A interrupt controller). The CPU has a flag bit IF indicating whether interrupts are enabled or not. The cli/sti instruction clears/sets the bit to disable/enable interrupts.In 8259 A there is a register isr,each bit of which corresponds to a hardware interrupt and records if the interrupt is being served or not.Different priority levels are assigned to different sources of interrupts,with level-0 being the highest.When an interrupt request comes,we check IF and isr.If the interrupts are enabled and there is currently no interrupt with higher or the same priority being served, the request will be served.The corresponding bit in isr is set to 1 and the control jumps to the corresponding interrupt handler. On the invocations of an interrupt handler,the CPU flags (including IF)are saved on the stack,and interrupts are disabled automatically.If interrupts are enabled again inside the handler,the handler could be further interrupted by requests with higher priorities,causing nested interrupts. The handler returns to the program being interrupted using the iret instruc- tion,which also restores the flags (including IF).Before the handler returns, it needs to execute eoi to send an "end of interrupt"signal to the interrupt controller,which clears the corresponding bit in isr.Note that after eoi but before iret,if interrupts are enabled(IF =1),the handler could be interrupted by interrupts at a lower or the same level. Overview of uC/OS-II.uC/OS-II is a commercial preemptive real-time multi- tasking OS kernel developed by Micrium [2].The kernel has 6000+lines of C code and 300+lines of assembly.It allows a fixed number of tasks,multi-level
A Practical Verification Framework for Preemptive OS Kernels 61 Fifth, we also specify and verify priority inversion freedom (PIF) of μC/OS-II. PIF is a crucial property for real-time systems and is worth verifying in its own right. Moreover, since the specification and verification are done at the level of the abstract model (i.e., specifications) of the kernel, they also help validate our model of system APIs. As we explain above, many important properties cannot be specified if the model is too weak or overly abstract. Coq proofs and a companion technical report are available at http://staff. ustc.edu.cn/∼fuming/research/certiucos. 2 Background and Overview of Our Work 2.1 Preemptive OS Kernels and Interrupts In a preemptive OS kernel, execution of a task inside the kernel can be interrupted at any program point (unless interrupts are disabled). Then the control is switched to the interrupt handler. When the handler finishes, it may invoke the scheduler and switch the execution context to a different task, instead of returning to the original interrupted task. For instance, with priority-based scheduling, the interrupt handler always switches to the highest priority task at its end. The x86 Interrupt Mechanism. Interrupt handling and management are indispensable in preemptive OS kernels. We give an overview of the interrupt mechanism in x86 systems (based on the Intel 8259 A interrupt controller). The CPU has a flag bit IF indicating whether interrupts are enabled or not. The cli/sti instruction clears/sets the bit to disable/enable interrupts. In 8259 A there is a register isr, each bit of which corresponds to a hardware interrupt and records if the interrupt is being served or not. Different priority levels are assigned to different sources of interrupts, with level-0 being the highest. When an interrupt request comes, we check IF and isr. If the interrupts are enabled and there is currently no interrupt with higher or the same priority being served, the request will be served. The corresponding bit in isr is set to 1 and the control jumps to the corresponding interrupt handler. On the invocations of an interrupt handler, the CPU flags (including IF) are saved on the stack, and interrupts are disabled automatically. If interrupts are enabled again inside the handler, the handler could be further interrupted by requests with higher priorities, causing nested interrupts. The handler returns to the program being interrupted using the iret instruction, which also restores the flags (including IF). Before the handler returns, it needs to execute eoi to send an “end of interrupt” signal to the interrupt controller, which clears the corresponding bit in isr. Note that after eoi but before iret, if interrupts are enabled (IF = 1), the handler could be interrupted by interrupts at a lower or the same level. Overview of μC/OS-II. μC/OS-II is a commercial preemptive real-time multitasking OS kernel developed by Micrium [2]. The kernel has 6000+ lines of C code and 300+ lines of assembly. It allows a fixed number of tasks, multi-level
62 F.Xu et al. interrupts,and preemptive priority-based scheduling.The system APIs include "semaphores;event flags;mutual-exclusion semaphores that eliminate unbounded priority inversions;mailbores;message queues;task,time and timer manage- ment;and fired sized memory block management"[2].uC/OS-II is developed for microprocessors and microcontrollers,and it does not support virtual memory. It has been deployed in many real-world safety critical applications,including avionics (e.g.,the Mars Curiosity Rover)and medical equipments. 2.2 Overview of the Verification Framework An OS kernel hides details of the underlying hardware and provides an abstract programming model for application-level programmers.The implementation of the kernel must ensure that behaviors of user applications in the real machine are consistent with their behaviors under the abstract model 14.Thus the OS verification can be reduced to verifying refinement between the concrete and abstract programming models. Contertual Refinement as Correctness.We consider three entities,the applica- tion A,the abstract specifications of the system APIs and interrupt handlers O,and their concrete implementations O.When system calls are made or inter- rupts are handled,routines in O are invoked in the real execution,while in the programmers'mind those in O are invoked instead at the abstract level.Then the correctness of OS kernels requires O refines O under all conterts A: VA.IA[O]IC IAO]] where I-]maps a program P to the set of its observable behaviors.It says that, for all applications,executing the concrete code O does not have more observ- able behaviors than executing the abstract version O.In this paper,observable behaviors are defined as finite prefixes of execution traces consisting of observable events,following Liang et al.[17]. Contextual refinement is a very strong notion of functional correctness of system APIs since it quantifies over all applications.Moreover,it makes verifica- tion of system-wide properties simpler.For instance,if we want to verify certain property about a whole system AO,i.e.,holds over every trace in [AO], we could prove that it holds over every trace in the superset [AO]instead. Proofs at the abstract level could be much simpler than the concrete level. The Whole Verification Framework.Figure 1 shows the structure of our verifi- cation framework.To model OS kernels and applications,we introduce two lan- guages(in block A),the low-level language for the concrete code implementation and the high-level language for the abstract specification.Above them we have a program logic (in block B)that allows us to prove the low-level kernel imple- mentation contextually refines the high-level specifications.The framework also provides a set of Coq tactics (in block C)to automatically generate and prove verification conditions.The uC/OS-II modules certified in this framework are shown in block D.Below we give details of some of the building blocks
62 F. Xu et al. interrupts, and preemptive priority-based scheduling. The system APIs include “semaphores; event flags; mutual-exclusion semaphores that eliminate unbounded priority inversions; mailboxes; message queues; task, time and timer management; and fixed sized memory block management” [2]. μC/OS-II is developed for microprocessors and microcontrollers, and it does not support virtual memory. It has been deployed in many real-world safety critical applications, including avionics (e.g., the Mars Curiosity Rover) and medical equipments. 2.2 Overview of the Verification Framework An OS kernel hides details of the underlying hardware and provides an abstract programming model for application-level programmers. The implementation of the kernel must ensure that behaviors of user applications in the real machine are consistent with their behaviors under the abstract model [14]. Thus the OS verification can be reduced to verifying refinement between the concrete and abstract programming models. Contextual Refinement as Correctness. We consider three entities, the application A, the abstract specifications of the system APIs and interrupt handlers O, and their concrete implementations O. When system calls are made or interrupts are handled, routines in O are invoked in the real execution, while in the programmers’ mind those in O are invoked instead at the abstract level. Then the correctness of OS kernels requires O refines O under all contexts A: ∀A.[[A[O]]] ⊆ [[A[O]]] where [[ ]] maps a program P to the set of its observable behaviors. It says that, for all applications, executing the concrete code O does not have more observable behaviors than executing the abstract version O. In this paper, observable behaviors are defined as finite prefixes of execution traces consisting of observable events, following Liang et al. [17]. Contextual refinement is a very strong notion of functional correctness of system APIs since it quantifies over all applications. Moreover, it makes verification of system-wide properties simpler. For instance, if we want to verify certain property Φ about a whole system A[O], i.e., Φ holds over every trace in [[A[O]]], we could prove that it holds over every trace in the superset [[A[O]]] instead. Proofs at the abstract level could be much simpler than the concrete level. The Whole Verification Framework. Figure 1 shows the structure of our verifi- cation framework. To model OS kernels and applications, we introduce two languages (in block A), the low-level language for the concrete code implementation and the high-level language for the abstract specification. Above them we have a program logic (in block B) that allows us to prove the low-level kernel implementation contextually refines the high-level specifications. The framework also provides a set of Coq tactics (in block C) to automatically generate and prove verification conditions. The μC/OS-II modules certified in this framework are shown in block D. Below we give details of some of the building blocks
A Practical Verification Framework for Preemptive OS Kernels 63 Multi-Level Priority-Based Interrupts Message Queue Mutex Semaphore Mail Box Scheduler (Timer &... Synchronization Mechanisms D.Verifying uC/Os-II Relational Assertions Refinement-Based Program Logic Contextual Refinement Entailment B.Refinement-Based Verification ●】 Forward Reasoning for Refinement-Based The High-Level Language System-Wide Judgements High-Level Small-Step Operational Semantics Properties with Configurable Schedulers Domain-Specific High-Level Abstract C Subset Low-Level Assembly Solvers Statements Primitives Low-Level Small-Step Operational Semantics with Context Switch and Interrupts The Low-Level Language C.Coq Tactics A.Modeling of oS Kernels Verification Framework Fig.1.Structure of the verification framework and uC/OS-II verification 3 Modeling of OS Kernels As explained above,the correctness of OS kernels is formalized based on three entities-user applications A,the concrete implementation O,and the abstract specification O.In this section we introduce the programming (or modeling) languages for the three entities (see block A in Fig.1).Due to space limit,we only show the main language features with simplifications for clear presentation. The details are available at TR and the Cog code [26]. 3.1 The Low-Level Language The low-level language consists of two parts for implementations of user appli- cations and OS kernels,respectively. Application Language.The application language is shown at the top of Fig.2. It is a subset of the C language consisting of function calls,pointer operations (except pointer arithmetics),arrays,structs,bit operations,etc.The application code A maps function names to their function bodies.The command f(e)calls the function f,which could be either an application function in A or an OS API (in O at the low-level or in O at the high-level,as we explain below)
A Practical Verification Framework for Preemptive OS Kernels 63 Fig. 1. Structure of the verification framework and μC/OS-II verification 3 Modeling of OS Kernels As explained above, the correctness of OS kernels is formalized based on three entities — user applications A, the concrete implementation O, and the abstract specification O. In this section we introduce the programming (or modeling) languages for the three entities (see block A in Fig. 1). Due to space limit, we only show the main language features with simplifications for clear presentation. The details are available at TR and the Coq code [26]. 3.1 The Low-Level Language The low-level language consists of two parts for implementations of user applications and OS kernels, respectively. Application Language. The application language is shown at the top of Fig. 2. It is a subset of the C language consisting of function calls, pointer operations (except pointer arithmetics), arrays, structs, bit operations, etc. The application code A maps function names to their function bodies. The command f(¯e) calls the function f, which could be either an application function in A or an OS API (in O at the low-level or in O at the high-level, as we explain below)