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)
64 F.Xu et al. (AErpr) e ::nlxl sel&ele.id ele]l... (AppStmts)d ::e=elf(e)d;d|while (e)dl if (e)d else dreturn el... (App Code）A={fhwd,.…,fndn (LPrim) ::switch z|encrt|excrt eoi iext... (LStmts) s ::dts;s while (e)s... (ItrpCode)0 ::[so,...,sN-1] (ProgUnit)n::={f1s1,...,fnsn} (LOSCode)O ::(na,ni,0) (LProg) P:=(A,O) (BitVal) b,ie∈{0,1} (ISRReg)isr ::[bo,...,bN-1] (CrtStk) cs ::nil ie::cs (ItrpStk)is ::nil k::is (ItrpTaskSt)::=(ie,is,cs) (ItpS0π={t161,·,tnw6n} Fig.2.The language for applications and kernel implementation Note that the correctness of OS kernels are independent of the implemen- tation language of A.Here we pick the C language for A to simplify the for- malization because the applications and the kernel are now implemented in the same language and we do not have to consider the interaction between different languages when defining the whole system (AO])behaviors. Low-Level Language for OS Kernels.The middle of Fig.2 shows the low-level language for the concrete implementation of OS kernels.Usually the kernels are implemented in C with inline assembly.However,giving semantics directly to C with inline assembly requires us to expose stacks and registers,which make the semantics overly complex.To avoid this problem,we extend the C statements with assembly primitives t to encapsulate the assembly code.Semantics of these primitives will be given below. switch x switches to the target task z.encrt enters a critical region by disabling interrupts.It also saves the old IF onto the stack to allow nested critical regions.Note we use ie to model the IF flag and abstract away other bits in the hardware EFLAGS register.excrt exits the current critical region by popping the stack to recover ie.Since we hide stacks in our state model,we use an abstract stack cs to save the historical ie bits (see Fig.2,which is explained below).eoi k clears the k-th bit in isr,indicating that the k-th interrupt is no longer in service.iext enables interrupts and returns to the interrupted program. The kernel implementation O consists of the system API implementation na, the internal functions ni and the interrupt handlers 0.The internal functions are called only by code in na or 0.6 is a sequence of N interrupt handlers,where N is the maximum number of interrupts we support.The handler with the lower identifier has the higher priority.Then a complete low-level program P is defined as a pair of the application code A and the kernel code O. Operational Semantics.The language is concurrent,with multiple continuations (i.e.,control stacks)in the state,each corresponding to a task.All tasks share
64 F. Xu et al. (AExpr) e ::= n | x | ∗ e | &e | e.id | e[e] | ... (AppStmts) d ::= e=e | f(¯e)| d; d | while (e) d | if (e) d else d | return e | ... (AppCode) A ::= {f1 d1,...,fn dn} (LPrim) ι ::= switch x | encrt | excrt | eoi k | iext | ... (LStmts) s ::= d |ι| s; s | while (e) s | ... (ItrpCode) θ ::= [s0,...,sN−1] (ProgUnit) η ::= {f1 s1,...,fn sn} (LOSCode) O ::= (ηa, ηi, θ) (LProg) P ::= (A, O) (BitVal) b, ie ∈ {0, 1} (ISRReg) isr ::= [b0,...,bN−1] (CrtStk) cs ::= nil | ie::cs (ItrpStk) is ::= nil | k ::is (ItrpTaskSt) δ ::= (ie, is, cs) (ItrpSt) π ::= {t1 δ1,...,tn δn} Fig. 2. The language for applications and kernel implementation Note that the correctness of OS kernels are independent of the implementation language of A. Here we pick the C language for A to simplify the formalization because the applications and the kernel are now implemented in the same language and we do not have to consider the interaction between different languages when defining the whole system (A[O]) behaviors. Low-Level Language for OS Kernels. The middle of Fig. 2 shows the low-level language for the concrete implementation of OS kernels. Usually the kernels are implemented in C with inline assembly. However, giving semantics directly to C with inline assembly requires us to expose stacks and registers, which make the semantics overly complex. To avoid this problem, we extend the C statements with assembly primitives ι to encapsulate the assembly code. Semantics of these primitives will be given below. switch x switches to the target task x. encrt enters a critical region by disabling interrupts. It also saves the old IF onto the stack to allow nested critical regions. Note we use ie to model the IF flag and abstract away other bits in the hardware EFLAGS register. excrt exits the current critical region by popping the stack to recover ie. Since we hide stacks in our state model, we use an abstract stack cs to save the historical ie bits (see Fig. 2, which is explained below). eoi k clears the k-th bit in isr, indicating that the k-th interrupt is no longer in service. iext enables interrupts and returns to the interrupted program. The kernel implementation O consists of the system API implementation ηa, the internal functions ηi and the interrupt handlers θ. The internal functions are called only by code in ηa or θ. θ is a sequence of N interrupt handlers, where N is the maximum number of interrupts we support. The handler with the lower identifier has the higher priority. Then a complete low-level program P is defined as a pair of the application code A and the kernel code O. Operational Semantics. The language is concurrent, with multiple continuations (i.e., control stacks) in the state, each corresponding to a task. All tasks share
A Practical Verification Framework for Preemptive OS Kernels 65 memory,but each has its own local variables and local interrupt states(see 6 in Fig.2,which is explained below).We also separate the program state (including memory and variables)into two disjoint parts,one for the application code A and the other for the kernel code O.The only way for A to access kernel states is to call system APIs in O,and O cannot access application states. We give small-step operational semantics to the language.For each step,the processor picks the continuation of the current task and executes its current command or expression.To model concurrency and interrupts,both commands and expressions could be executed in multiple steps,where each step corresponds to the granularity of a single machine instruction (as in CompCertTSO [22],but we use the sequential consistent model instead of the x86-TSO memory model). The assembly implementation of the context switch routine is abstracted into the primitive switch r.It switches the execution from the current task to the target task z,where x stores the task identifier. The other assembly primitives t are all related to interrupts management and handling.To model their semantics,we introduce interrupt states in the state model,as shown at the bottom of Fig.2.The global register isr is shared by all tasks.It models the isr register in the 8259 A interrupt controller,as explained in Sect.2.1.In addition,there are local interrupt states 6 for each task.It contains a local copy ie of the IF flag in the EFLAGS register (see Sect.2.1)recording whether interrupts are enabled,a stack cs consisting of the historical values of ie to support nested critical regions,and another stack is recording the sequence of interrupts that interrupt the execution of the task.The stack isis auxiliary data introduced mainly for verification purposes.records the 6 of each task. encrt enters a critical region by disabling interrupts (ie.,clearing the ie bit using cli).It also saves the old ie onto the cs stack.excrt exits the critical region by popping off the top value on cs and using it to restore ie (executing sti if the value is 1). Interrupt requests may arrive non-deterministically after each step if ie=1. A level-k request is served only if there is no request at higher or the same level being served (i.e.,Vk'.k'<k-isr()=0).Then the processor clears ie,sets isr(k)to 1,pushes the number k onto the logical stack is,saves the execution context and the local variables onto the abstract control stack (i.e., the continuation),and finally jumps to the interrupt handler 0(k). eoi k clears the k-th bit in isr,indicating that the k-th interrupt is no longer in service.iext is an abstraction of the iret instruction.It resets the ie bit to 1 to enable interrupts,pops out the topmost interrupt number on the is stack, and returns to the interrupted program. 3.2 The High-Level Specification Language Viewing from the aspect of application programmers,we model the OS kernel as an extended C language with multi-tasking and system calls.As explained above,the C language is used to implement user applications A,and the system calls invoke an abstract version of system routines in O,which are implemented using a simple specification language.Correspondingly,the low-level concrete
A Practical Verification Framework for Preemptive OS Kernels 65 memory, but each has its own local variables and local interrupt states (see δ in Fig. 2, which is explained below). We also separate the program state (including memory and variables) into two disjoint parts, one for the application code A and the other for the kernel code O. The only way for A to access kernel states is to call system APIs in O, and O cannot access application states. We give small-step operational semantics to the language. For each step, the processor picks the continuation of the current task and executes its current command or expression. To model concurrency and interrupts, both commands and expressions could be executed in multiple steps, where each step corresponds to the granularity of a single machine instruction (as in CompCertTSO [22], but we use the sequential consistent model instead of the x86-TSO memory model). The assembly implementation of the context switch routine is abstracted into the primitive switch x. It switches the execution from the current task to the target task x, where x stores the task identifier. The other assembly primitives ι are all related to interrupts management and handling. To model their semantics, we introduce interrupt states in the state model, as shown at the bottom of Fig. 2. The global register isr is shared by all tasks. It models the isr register in the 8259 A interrupt controller, as explained in Sect. 2.1. In addition, there are local interrupt states δ for each task. It contains a local copy ie of the IF flag in the EFLAGS register (see Sect. 2.1) recording whether interrupts are enabled, a stack cs consisting of the historical values of ie to support nested critical regions, and another stack is recording the sequence of interrupts that interrupt the execution of the task. The stack is is auxiliary data introduced mainly for verification purposes. π records the δ of each task. encrt enters a critical region by disabling interrupts (i.e., clearing the ie bit using cli). It also saves the old ie onto the cs stack. excrt exits the critical region by popping off the top value on cs and using it to restore ie (executing sti if the value is 1). Interrupt requests may arrive non-deterministically after each step if ie = 1. A level-k request is served only if there is no request at higher or the same level being served (i.e., ∀k .k ≤ k → isr(k ) = 0). Then the processor clears ie, sets isr(k) to 1, pushes the number k onto the logical stack is, saves the execution context and the local variables onto the abstract control stack (i.e., the continuation), and finally jumps to the interrupt handler θ(k). eoi k clears the k-th bit in isr, indicating that the k-th interrupt is no longer in service. iext is an abstraction of the iret instruction. It resets the ie bit to 1 to enable interrupts, pops out the topmost interrupt number on the is stack, and returns to the interrupted program. 3.2 The High-Level Specification Language Viewing from the aspect of application programmers, we model the OS kernel as an extended C language with multi-tasking and system calls. As explained above, the C language is used to implement user applications A, and the system calls invoke an abstract version of system routines in O, which are implemented using a simple specification language. Correspondingly, the low-level concrete
66 F.Xu et al. (HStmts)s::=schedy(assert b|end 1;2$1+ (HAPISet)::={f11,...,fnsn} (HEvtSet)::so,...,N-1] (HSched)x∈HAbSt--TaskId→Prop (TaskId④t∈Nat (HOSCode)::=(p,E,x) (HProg)P::=(A,O) (HAbsSt∑：={a121,.,an2n} (HDataNm)a ::tcbls ctid... (HData) 2=alt|.… (HStatus)ts::=rdy... (HTCBLs)a ::=t(pri,ts1,...),...,tn(prn;tsn,...)} Fig.3.High-level spec.language and abstract states representation of kernel states is modeled as algebraic abstract states at the high level.This section presents the high-level language and its semantics. As shown in Fig.3,the whole high-level program P consists of the application code A and the abstract specification of the kernel O.The application code A is the same as in the low-level language (see Fig.2).O contains the specifications for kernel APIs,e for interrupt handlers,and x for the scheduler. Programmers at this level have no control over interrupts (e.g.,enabling or disabling interrupts).Always enabled,interrupts are modeled implicitly as abstract external events that may occur non-deterministically at any program points.At the high level an incoming level-k event is always handled by executing e(k),i.e.the k-th handler specified in s. The system APIs and interrupt handlers are specified as an abstract state- ment s,which forms a simple but expressive specification language.sched does scheduling.Its semantics is determined by the abstract scheduler specification X.As defined in Fig.3,x is a binary relation between abstract states and task identifiers.That is,given an abstract state (defined at the bottom of Fig.3),x finds a related task identifier as the next task to execute.Note that x is a relation instead of a function,therefore the abstract scheduler could be non-deterministic. Since x is provided as part of the kernel specification,the semantics of sched in our language is configurable.Specifying details of the scheduling policies(instead of using a more abstract non-deterministic scheduler that may pick any task) allows us to specify and verify scheduling properties such as PIF at the high level. ()is a meta-level relation(defined in Coq)that takes as arguments and maps an abstract state to another.It can be instantiated to specify any atomic transitions over abstract states.assert b asserts that the predicate b holds over the current abstract state.end represents the end of abstract APIs or interrupt handlers.s1;s2 and s1+s2 are statements for sequential composition and non- deterministic choices respectively. Abstract States.The kernel state is represented as the abstract state at the high level.As defined at the bottom of Fig.3,is a mapping from names a to the abstract data Here tcbls is the name for the high-level abstract TCB list a,which maps task identifiers to abstract tasks,including the priority pr
66 F. Xu et al. (HStmts) ::= sched | γ(¯v)| assert | end | 1; 2 | 1+ 2 (HAPISet) ϕ ::= {f1 1,...,fn n} (HEvtSet) ε ::= [ 0,..., N−1] (HSched) χ ∈ HAbsSt → TaskId → Prop (TaskId) t ∈ Nat (HOSCode) O ::= (ϕ, ε, χ) (HProg) P ::= (A, O) (HAbsSt) Σ ::= { 1 Ω1,..., n Ωn} (HDataNm) ::= tcbls| ctid | ... (HData) Ω ::= α |t| ... (HStatus) ts ::= rdy | ... (HTCBLs) α ::= {t1 (pr1, ts1,...),. . ., tn (prn, tsn,...)} Fig. 3. High-level spec. language and abstract states representation of kernel states is modeled as algebraic abstract states at the high level. This section presents the high-level language and its semantics. As shown in Fig. 3, the whole high-level program P consists of the application code A and the abstract specification of the kernel O. The application code A is the same as in the low-level language (see Fig. 2). O contains the specifications ϕ for kernel APIs, ε for interrupt handlers, and χ for the scheduler. Programmers at this level have no control over interrupts (e.g., enabling or disabling interrupts). Always enabled, interrupts are modeled implicitly as abstract external events that may occur non-deterministically at any program points. At the high level an incoming level-k event is always handled by executing ε(k), i.e. the k-th handler specified in ε. The system APIs and interrupt handlers are specified as an abstract statement s, which forms a simple but expressive specification language. sched does scheduling. Its semantics is determined by the abstract scheduler specification χ. As defined in Fig. 3, χ is a binary relation between abstract states and task identifiers. That is, given an abstract state Σ (defined at the bottom of Fig. 3), χ finds a related task identifier as the next task to execute. Note that χ is a relation instead of a function, therefore the abstract scheduler could be non-deterministic. Since χ is provided as part of the kernel specification, the semantics of sched in our language is configurable. Specifying details of the scheduling policies (instead of using a more abstract non-deterministic scheduler that may pick any task) allows us to specify and verify scheduling properties such as PIF at the high level. γ(¯v) is a meta-level relation (defined in Coq) that takes ¯v as arguments and maps an abstract state to another. It can be instantiated to specify any atomic transitions over abstract states. assert b asserts that the predicate b holds over the current abstract state. end represents the end of abstract APIs or interrupt handlers. s1; s2 and s1+s2 are statements for sequential composition and nondeterministic choices respectively. Abstract States. The kernel state is represented as the abstract state Σ at the high level. As defined at the bottom of Fig. 3, Σ is a mapping from names a to the abstract data Ω. Here tcbls is the name for the high-level abstract TCB list α, which maps task identifiers to abstract tasks, including the priority pr
A Practical Verification Framework for Preemptive OS Kernels 67 (a natural number),the task status (ready,waiting,etc.and so on,depending on the low-level implementations.ctid is the name for the current task identifier t. Erample of High-Level Specifications.We use saly (Yerr(ticks)+ (ly(ticks);sched))to specify the system API "void OSTimeDly(Int16u ticks)", which delays the current task for the specified number of system ticks.The atomic operation Yerr(ticks)specifies the error case when ticks =0.ly(ticks) defines the atomic behavior of updating the status of the current task from “ready”to“waiting”with the duration set to ticks when ticks>O,and the following sched switches to another ready task,following the scheduling policy specified by the abstract scheduler x.Note that the exclusive conditions over ticks in err(ticks)and dly(ticks)make the non-deterministic choice statement deterministic.We omit the definitions of err(ticks)and dly(ticks)here. As another example,below we show the abstract scheduler specification Xuc/os-I for uC/OS-II.It requires that the selected task be ready and have the highest priority among all the ready tasks. Xuc/os-II,t.3a,pr.(tcbls)=a Aa(t)=(pr,rdy) t',pr'.(t≠t'Aa(t)=(pr',rdy)→pr'<pr 3.3 OS Correctness As we explain in Sect.2.2,the correctness of OS kernels can be defined in terms of contextual refinement.Below we give its formal definition. Definition 3.1 (OS Correctness).Oiff VA,W,W.Match(v,W,W)=((A,O),W)((A,0),W) where∈LOSFullSt→HAbsSt→Prop and Match(,(T,△，A,t),(T,△，) (t∈dom(T)A(中A)A(t=(ctid)A(dom(T)=dom((tcbls)】 The low-level kernel code O refines its high-level abstract specifications O with constraints over initial kernel states,denoted as OO,if and only if for any client code A,low-level state W and high-level state W,if W and W satisfy certain consistency constraint (w.r.t.)then the set of observable behaviors of the low-level configuration ((A,O),W)is a subset of ((A,O),W) (i.e.,(P,W)(P,W),following the event trace refinement in [17]). Due to space limit,we elide the definitions of W and W in Sects.3.1 and 3.2.The low-level whole program state W is in the form of (T,A,A,t),where the task pool T maps task identifiers to their continuations,A is the client state, A is the low-level kernel state,and t is the identifier of the current task.The high-level program state W is in the form of(T,△，)，where∑is an abstraction of the low-level kernel state A and the current task id t. The constraint Match requires that:(1)initially W and W have the same task pool T and client state A;(2)the current task t is in T;(3)the low-level
A Practical Verification Framework for Preemptive OS Kernels 67 (a natural number), the task status (ready, waiting, etc.) and so on, depending on the low-level implementations. ctid is the name for the current task identifier t. Example of High-Level Specifications. We use sdly def = (γerr(ticks) + (γdly(ticks); sched)) to specify the system API “void OSTimeDly(Int16u ticks)”, which delays the current task for the specified number of system ticks. The atomic operation γerr(ticks) specifies the error case when ticks = 0. γdly(ticks) defines the atomic behavior of updating the status of the current task from “ready” to “waiting” with the duration set to ticks when ticks > 0, and the following sched switches to another ready task, following the scheduling policy specified by the abstract scheduler χ. Note that the exclusive conditions over ticks in γerr(ticks) and γdly(ticks) make the non-deterministic choice statement deterministic. We omit the definitions of γerr(ticks) and γdly(ticks) here. As another example, below we show the abstract scheduler specification χμC/OS-II for μC/OS-II. It requires that the selected task be ready and have the highest priority among all the ready tasks. χμC/OS-II def = λΣ, t.∃α, pr.Σ(tcbls) = α ∧ α(t)=(pr,rdy)∧ ∀t , pr .(t=t ∧α(t )=(pr ,rdy))→pr ≺pr 3.3 OS Correctness As we explain in Sect. 2.2, the correctness of OS kernels can be defined in terms of contextual refinement. Below we give its formal definition. Definition 3.1 (OS Correctness). O ψ O iff ∀A, W,W. Match(ψ, W,W) =⇒ ((A, O), W) ((A, O),W) where ψ ∈ LOSFullSt → HAbsSt → Prop and Match(ψ,(T, Δ, Λ, t),(T, Δ, Σ)) def = (t ∈ dom(T))∧(ψΛΣ)∧(t=Σ(ctid))∧(dom(T)=dom(Σ(tcbls))) The low-level kernel code O refines its high-level abstract specifications O with constraints ψ over initial kernel states, denoted as O ψ O, if and only if for any client code A, low-level state W and high-level state W, if W and W satisfy certain consistency constraint (w.r.t. ψ), then the set of observable behaviors of the low-level configuration ((A, O), W) is a subset of ((A, O),W) (i.e., (P,W) (P,W), following the event trace refinement in [17]). Due to space limit, we elide the definitions of W and W in Sects. 3.1 and 3.2. The low-level whole program state W is in the form of (T, Δ, Λ, t), where the task pool T maps task identifiers to their continuations, Δ is the client state, Λ is the low-level kernel state, and t is the identifier of the current task. The high-level program state W is in the form of (T, Δ, Σ), where Σ is an abstraction of the low-level kernel state Λ and the current task id t. The constraint Match requires that: (1) initially W and W have the same task pool T and client state Δ; (2) the current task t is in T; (3) the low-level
68 F.Xu et al. inc(){ int done=0,tmp; while(!done){ [ent =N) N.cnt N {cnt CNT A [I (CNT++)]) 1nc(); inc(); ine(); tmp=cnt; done=cas(&cnt,tmp,tmp+1) (cnt =N+1} {3N.cnt N} {cnt CNT A [end] (a)Implementation of inc (b)Wrong spec. (c)Weak spec. (d)Refinement spec. Fig.4.Specification of concurrent programs kernel state A and the high-level abstract state satisfy v;(4)the current task at the low level and the high level are the same;and (5)the set of tasks in the abstract TCB list should be the same as those in the low-level task pool. 4。 Relational Program Logic for Refinement Verification In this section,we present a CSL-style relational program logic for refinement verification.The logic uses relational assertions to prove refinement between an implementation and its specification.It also follows the ownership-transfer semantics in CSL to reason about multi-level hardware interrupts. Refinement of Concurrent Programs,and Relational Reasoning.For concurrent programs,refinement establishes stronger functional correctness than traditional Hoare triples.As an example,the function inc shown in Fig.4(a)increments the counter cnt.It may be called simultaneously by concurrent tasks.Figure 4(b) gives pre-/post-conditions to specify inc,which would be valid in a sequen- tial setting and is sufficient to describe the functionality.However,they cannot be used in a concurrent setting because they are not stable with respect to concurrent behaviors of other tasks.To make them stable,we may need the specifications in Fig.4(c),which is too weak to capture the functionality. Figure4(d)gives a relational specifications to show that inc refines an abstract operation (CNT++)[19],where (C)represents an atomic operation C. The relational assertions specify three important entities,the concrete state (cnt),the abstract state (CNT)and the abstract operation ((CNT++))that the program refines (which could be non-atomic in general [19]).The precondition requires that initially cnt has the consistent value with its abstract counterpart CNT,and the abstract operation that inc needs to refine is (CNT++).The post- condition ensures cnt and CNT remain consistent and the remaining abstract operation that needs to be refined is end (i.e.,(CNT++)has been accomplished). Our refinement proofs for OS kernels follow the same kind of relational rea- soning,where the assertions now relate the concrete kernel state,the abstract kernel state ()and the abstract statement (s). Assertions.Below is the assertion language,and its semantics is given in Fig.5. (Asrt)p,q,r :empl empEISR(isr)IE(ie)IS(is)|CS(cs)xt |a一2l[|p*PPAP|. (Inv)I::po,...,PN]
68 F. Xu et al. Fig. 4. Specification of concurrent programs kernel state Λ and the high-level abstract state satisfy ψ; (4) the current task at the low level and the high level are the same; and (5) the set of tasks in the abstract TCB list should be the same as those in the low-level task pool. 4 Relational Program Logic for Refinement Verification In this section, we present a CSL-style relational program logic for refinement verification. The logic uses relational assertions to prove refinement between an implementation and its specification. It also follows the ownership-transfer semantics in CSL to reason about multi-level hardware interrupts. Refinement of Concurrent Programs, and Relational Reasoning. For concurrent programs, refinement establishes stronger functional correctness than traditional Hoare triples. As an example, the function inc shown in Fig. 4(a) increments the counter cnt. It may be called simultaneously by concurrent tasks. Figure 4(b) gives pre-/post-conditions to specify inc, which would be valid in a sequential setting and is sufficient to describe the functionality. However, they cannot be used in a concurrent setting because they are not stable with respect to concurrent behaviors of other tasks. To make them stable, we may need the specifications in Fig. 4(c), which is too weak to capture the functionality. Figure 4(d) gives a relational specifications to show that inc refines an abstract operation CNT++ [19], where C represents an atomic operation C. The relational assertions specify three important entities, the concrete state (cnt), the abstract state (CNT) and the abstract operation ( CNT++ ) that the program refines (which could be non-atomic in general [19]). The precondition requires that initially cnt has the consistent value with its abstract counterpart CNT, and the abstract operation that inc needs to refine is CNT++ . The postcondition ensures cnt and CNT remain consistent and the remaining abstract operation that needs to be refined is end (i.e., CNT++ has been accomplished). Our refinement proofs for OS kernels follow the same kind of relational reasoning, where the assertions now relate the concrete kernel state, the abstract kernel state (Σ) and the abstract statement (s). Assertions. Below is the assertion language, and its semantics is given in Fig. 5. (Asrt) p, q, r :: = emp | empE | x −→v | ISR(isr)| IE(ie)| IS(is)| CS(cs)| k | χt | Ω | [||] | p ∗ p | p ∧ p | ... (Inv) I :: = [p0,...,pN ]