Formal verification of a task scheduler for embedded operating systems

Abstract

A task scheduler plays an important role in Embedded Operating Systems (EOS). In order to ensure the scheduling properties of an EOS, it is important to verify the implementation of its task scheduler. However, the implementation of a task scheduler requires the manipulation of machine registers directly and uses very complex C pointer structures to manage the task related data. Thus, we need a verification system that can formally describe both C pointer programs and embedded code pointers (e.g., update the stack register) naturally. Based on the Verified Software Toolchain and the CompCert ARM assembly syntax and semantics, we utilize the Coq proof assistant to develop formal reasoning support for the verification of a low-level task scheduler. Our verification system has the capability to verify both C and ARM assembly language; it supports the separation of logical abstractions and specific implementations. More importantly, all the verification can be done in a unified modular verification framework, which minimizes semantic gaps at specification interfaces.

Keywords

Task scheduler program verification embedded operating system formal methods

1 Introduction

An embedded operating system (EOS) is responsible for all the software and hardware resource allocation, task scheduling, control, and coordination of concurrent activities of the embedded system. A task scheduler is an indispensable component of the EOS. The verification of its functional correctness is essential in building a foundationally verified EOS.

The formal specification and verification of a task scheduler is difficult because a scheduler is written in low-level languages (e.g., C and assembly) and uses very complex data structures to manage the task related data (e.g., task queue of a double-linked list). What’s more, the task context switching can manipulate return code pointers directly. Before a context switch finally returns to the calling task (named as task A), the control has been transferred to a different task (named as task B). This results in two fundamental questions. First, how to build the specification of the context switching subroutine without knowing in advance the task it may switch to? Second, should we view task B as part of the context switch or not?

To deal with these challenges, various approaches for verifying task/thread scheduler have been proposed. Yu et al. [1] who demonstrate modular verification of a thread context switching at different abstract levels. However, their verification system has not connected with a trusted compiler. Hence, this work cannot guarantee that the assembly execution of the certified program is correct. Ferreira et al. [2] automatically verify the task scheduler component of the FreeRTOS using the verification system Hip/SLEEK. However, they have not mentioned how to verify the context switching code, because the Hip/SLEEK system cannot build specifications for assembly instructions. Ni et al. [3] use a very general and expressive logic system to certify a thread scheduler. Despite its generality, their method yields complex specifications that are hard to understand.

Another related verification work is the Australian NICTA Lab’s verification of the seL4 microkernel operating system [4 –6]. However, they use a monolithic verification framework, which does not readily support embedded code pointers. Finally, a closely related work is reported in [7], where the authors discuss how to end-to-end verify security properties of the OpenSSL HMAC using the VST and the CompCert compiler. Similarly, their work does not involve the verification of assembly code.

We propose a verification system to formally specify and mechanically verify the correctness of the EOS task scheduler. Our paper makes the following contributions: 1) We present a verification system to verify program modules at different abstraction levels. 2)We show how our verification system can be used to verify both C and assembly code in a unified modular verification framework. 3) We show how our verification system can be used to link multiple verified modules into one large verified module.

The remainder of the paper is organized as follows. In Section 2, we give an overview of the EOS task scheduler that we utilize as an example. In Section 3, we discuss the details of our verification system and framework. In Section 4, we specify and verify an example EOS task scheduler to demonstrate the usability and practicality of our verification system and framework. Finally, Section 5 outlines our conclusions.

2 EOS task scheduler

In the EOS, a task is defined as an executing program. In the presence of multiple tasks, the task scheduler decides which task to execute at any specific time. In this section, we present the scheduling process of an example EOS scheduler using a simple example with two tasks, as shown in Fig. 1. To simplify the presentation, we assume the scheduler has pushed the current running task into a ready queue and is going to select the next task to execute.

Fig.1

Illustrative example: Scheduling between two tasks.

The taskResched function selects the highest priority ready task to execute. First, it uses the function getCurtid to get the current task id (curtid). Then, it uses the function setCurtid to update the current task id as ntid. Finally, the Scheduler calls the function ctxSwitch to jump to the next task and finish the scheduling process. If there are two tasks, A and B (see Fig. 1), task A sets a global variable curtid to ntid and then switches to task B. task B resets the variable curtid to ntid and switches back to task A. In addition, there is also a global variable array named CtxtPool that contains the machine context structures of tasks.

In general, context switching is used for saving the context of a task being suspended and restoring the context of a task being resumed. The C interface of the ctxSwitch subroutine, which implements the task context switching is: $void ctxSwitch (unit 32_t oldtid, unit 32_t newtid)$

Here, oldtid and newtid are indices of the array CtxtPool. The oldtid points to the structure that saves the current machine context, and the newtid points to the machine context structure to be loaded. Because the subroutine needs access to the machine registers directly, the subroutine is usually implemented in assembly language. Figure 2 presents an ARM implementation of the subroutine.

Fig.2

ARM implementation of the task context switching subroutine.

The function saves all the machine registers except R0-R3 into the old context and loads the new context into the machine registers. Note that the return address register RA is also modified. Hence, when the function returns, it jumps to the target task to execute instead of the current task.

3 Verification system and framework

In this section we introduce our verification system and present the formal details of our modular verification framework. This presentation covers the specification language for C and ARM assembly, and the compositional verification rules of the verification framework.

3.1 Verification system

Our verification system is aimed at the compositional verification of functional correctness for EOSs. The overall structure of the verification system is shown in Fig. 3. At the top of this figure are the API specification and the Functional specifications components. The API specification establishes the adoption of user defined separation logic predicates; these predicates are used for proving the functional correctness of C programs with pointer data structures. The API specs are written in separation logic that is supported by the Verified Software Toolchain (VST) [8]. The Functional specification is the user defined functional program that implements the abstract algorithms of the C or assembly programs. After the consistency proof between the API and functional specifications, we achieve the following objective during the proof of a parent program: a parent program can directly call its subroutines’ functional specifications without knowledge of the underlying concrete implementation. For example, if we prove the function taskResched (the parent program, see Fig. 1), we can call the functional specifications of the function ctxSwitch (the subroutine program) without knowledge of its concrete implementation. Therefore, the return code pointer (pc and RA, see Fig. 2) is not data at the high level (the parent program). At the low level (the subroutine program), we only need to ensure that the subroutine ctxSwitch loads new values from and saves machine registers into correct addresses. Finally, we use a verified compiler (e.g., CompCert [9]) that can correctly compile C programs into assembly, which guarantees that our model of the whole-system assembly execution is correct. In this way, we can verify program modules at different abstraction levels using different verification logic, which reduces the verification complexity and increases the scalability of the verification system. In what follows, we illustrate our modular verification framework that is compatible with the verification system.

Fig.3

Overview of the verification system.

3.2 Modular verification framework

A modular verification framework should have at least two capabilities: first, support the formal definition of modules at different abstract levels; second, support linking all of the verified modules together. Formally, the definition of an abstract module that provides the first capability is presented below.

Definition 1 (abstract module). An abstract module is an abstract state machine $M = (\sum, Δ, OS)$ , and consists of the following parts:

∑ ={ s₁, s₂, . . . , s_n } is a set of all possible states in a module,

Δ ={ l₁, l₂, . . . , l_m } is a set of names of all operations that the module supports,

OS ∈ { l (p, g) } ^* is a set of operational semantics as a finite map from operation identifiers to operation specifications over the state ^∑, where p ∈ ∑ → Prop is a state predicate and g ∈ ∑ → ∑Prop is state relation.

Up to this point, we have defined the abstract state machine for an abstract module, but it does not have any notion of program computation. To make it practical, we use Clight [10] as a meta-language to define the concepts of the C programs. The syntax and semantics definition of the Clight meta-language are given in Fig. 4.

Fig.4

Syntax and semantics of the meta-language for C language.

The syntax of Clight features global variables, local variables, and temporary variables. Expressions include comparison, offset, and the other pointer arithmetic. Statements support assignment, function call and return, and structured control (sequence, branch, and loops). The meaning of executing a program is given by the statement semantics in Fig. 4. It means that from the module environment $M$ , the specifications of the called function $L$ , the input arguments ins, and the state s, the execution of $𝕊$ terminates and yields results res, and state s′. Compared with Clight, our modular verification framework permits calls to the specifications $L$ .

The ARM assembly subset specified in the CompCert is used as a meta-language to define the concepts of assembly code, as shown in Table 1. CompCert ARM assembly is modeled as a state machine with a register set and a memory state. We extend the machine state with an abstract state, which makes the assembly specifications syntactically indistinguishable from the C functional specifications. As a result, we can verify both C and assembly code within a unified framework.

Table 1

Syntax and semantics of the meta-language for ARM assembly language

Syntax
ri::=IR0 \|IR1 \|IR2\| ... \|IR13 \|IR14	Integer registers
rf::=FR0 \|IFR1 \|FR2 \| ... \|FR14 \|FR15	Float registers
r ∈ preg::=ri \| rf\| PC	ARM register set
so::=$n\| (ri)n\| ...	Immediate addressing Register addressing
I::=Pmov r1 so \| Pldr r1 r2 so \| Pstr r1 r2 so \| ... \| Pmla r1 so \| Ploadsymbol \| Pbreg cond lbl	ARM instruction set
Operational semantics
Pmov	Assignment
Pldr	Read the data from memory into register
Pstr	Save the data in the register into the memory
Pmla	Multiply and add
Ploadsymbol	Read the data from the specified memory address
Pbreg	Assign a value to the PC register

In order to facilitate multi-module verification, we present the semantics of a verified module that allows us to verify new modules based on verified modules. Formally, we have the following definition.

Definition 2 (Semantics of a Verified Module). Let $M$ be an abstract module, let $ℂ^{M}$ be the statement heap of $M$ , let $L_{1}$ be the specifications of the called function by $ℂ^{M}$ , let $L_{2}$ be the specifications of $ℂ^{M}$ , and let $R$ be the refinement relation [11] between $L_{1}$ and $L_{2}$ . The semantics of a verified module are defined by the following rule: $\frac{\forall f \in dom (ℂ^{M}) . M, L_{1} ⊢_{R} ℂ^{M} (f) : L_{2} (f)}{M, L_{1} ⊢_{R} C^{M} : L_{2}}$

The concept of a verified module $M, L_{1} ⊢ C^{M} : L_{2}$ means that, using the refinement relation $R$ , every function in $ℂ^{M}$ faithfully implements $L_{2}$ . The module $M$ also defines a set of specifications $L_{1}$ , i.e., functions that are called by the module, but are not in the module.

Permitting calls to the specifications of $L_{1}$ presents challenges,, as we have to ensure that the functions in the module $N$ (assuming $N, L ⊢_{S} C^{N} : L_{1}$ , let $L_{1}$ be the specifications of module $N$ ) do not break the specifications $L_{2}$ that are adhered to by the module $M$ Those functionsin the module $N$ require weaker specifications that may violate the stronger specifications required by the module $M$ We solve this problem with the operation of layering [12, 13], which describes how to verify a system with multiple layers without breaking already satisfied invariants due to arbitrary module interactions or dependencies. Intuitively, layering permits the function of $M$ to use the functions defined in $N$ , but conversely the function of $N$ cannot access the functions of $M$ . After layering, we can compositionally verify a system using the vertical and horizontal composition rules. Formally, we present the following compositional rules. $\frac{N, L ⊢_{S} C^{N} : L_{1} M, L_{1} ⊢_{R} C^{M} : L_{2}}{M \otimes N, L ⊢_{S \circ R} C^{M \otimes N} : L_{2}}$

Vertical Composition $\frac{N, L ⊢_{R} C^{N} : L_{1} M, L_{1} ⊢_{R} C^{M} : L_{2}}{M \otimes N, L ⊢_{R} C^{M \otimes N} : L_{1} \otimes L_{2}}$

Horizontal Composition

The above vertical composition rule describes one-abstract-level incremental verification. By successive applications of this rule, we can verify a system with multiple abstraction levels. The above horizontal composition rule describes the combination of many verified modules at the same abstract level into a single, larger verified module.

4 Case study: Modular verification of the EOS task scheduler

In this section, we present how to verify programs at different abstraction levels under a unified framework. The verification is presented in three parts: defining the API specifications; defining the functional specifications; and linking together the verified modules.

Figure 5 shows the process of building a verified module. We introduce the language-specific predicate $VC (M, L_{1} ⊢ C^{M} (f) : L_{1}^{'} (f))$ to assert that the statement $ℂ^{M} (f)$ faithfully implements the specification $L_{1}^{'} (f)$ based on the specifications $L_{1}$ . We first prove that $M, L_{1} ⊢ C^{M} : L_{1}^{'}$ holds. We then prove $L_{2} \underset{R}{⊒} L_{1}^{'}$ , which means that each functional specification $L_{2} (f)$ is an abstraction of its corresponding API specification $L_{1}^{'} (f)$ via a refinement relation $R$ . Finally, we obtain the verified module $M, L_{1} ⊢_{R} C^{M} : L_{2}$ . Figures 6 –10 show how we use our modular verification framework to verify the EOS task scheduler in Coq.

Fig.5

Building a verified module.

Fig.6

Concrete (C) vs. abstract (Coq) model of the curtidmodule.

Fig.7

API vs functional specification (Coq) of the setCurtid function.

Fig.8

Assembly model and functional specification (Coq) of the ctxswitch module.

Fig.9

Abstract Model (Coq) of the scheduler module.

Fig.10

API vs functional specification (Coq) of the taskResched function.

4.1 API specifications

The API specification defines the API behavior of each function: the data structures it operates on, its preconditions (what it assumes about the input data structures available in parameters and global variables), and the postcondition (what is guaranteed about its return value and changes to data structures).

Here, we show the API specification for the function setCurtid. The source code and specification are provided in Figs. 6 (left) and 7 (top), respectively. The DECLARE clause describes the name of the function; contents within the PRE and POST are the C input parameters and return type, respectively. The precondition and postcondition consist of PROP () LOCAL () SEP (), where PROP is used to present pure propositions (e.g., invariants of the current program), LOCAL is used for local/global variable bindings, and SEP is used to present separation logic predicates that describe the contents of memory. The variables under the WITH clause can be referred to by the precondition and postcondition.

In our setCurtid_API_spec, shown in Fig. 7(top), the first variable listed in this WITH clause is the global variable curtid. It defines an address in memory. The “Vundef” means that we do not care what the value is. The second variable listed in this WITH clause is an integer value tid; we use (vint (Int repr tid)) to define the memory address of the ntid. The precondition contains an uninitialized value (Vundef) at the address curtid. In the postcondition, we find that at the address curtid, the value has become an initialized value (tid). For functional correctness proofs of C functions, we use the VST to prove that each function’s body faithfully implements its API specification.

4.2 Functional specifications

In order to separate logic reasoning from low-level data operations verification, we introduce more abstract functional specifications. As shown in the right of Fig. 6 and the top of Fig. 8, the abstract states and functions of the C and assembly programs can be formalized in Coq as the mathematical variables and functions. For example, we introduce an abstract state of type CtxtPool (Fig. 8) where we represent a C structure array as a Coq finite map (ZMap.t). After transforming the concrete memory state into an abstract Coq data type, we implement the abstract functions for the operations of the abstract Coq data structures. For example, based on CompCert’s ARM assembly syntax and semantics, we developed an assembly execution function asm_exec (at the bottom of Fig. 8) that receives two parameters: one is the abstract state and the other is the assembly instruction list.

Now, all the states and functions have been formalized. We then start to prove the following two goals: functional correctness $(M, L_{1} ⊢ ℂ^{M} : L_{1}^{'})$ and refinement $(L_{2} \underset{R}{⊒} L_{1}^{'})$ . The functional correctness proof is straightforward for Verifiable C because the code logic of this part is simple, and the separation logic is well-suited for describing low-level data operations. However, the refinement proof is more challenging. Here, we design a refinement relation $R$ that relates the concrete memory states in API specifications with their corresponding abstract states in functional specifications. The refinement proof for $L_{2} \underset{R}{⊒} L_{1}^{'}$ involves the efforts to prove that this relation $R$ is preserved by all of the functions in both $L_{1}^{'}$ and $L_{2}$ . More specifically, we relate the abstract state and the concrete state by requiring that for every item in the abstract, the same item can be found at the appropriate place in the concrete. For example, a relation of the curtid module between the abstract and the concrete can be defined as the following predicate:

$\begin{matrix} Definition R_a bs_c on (ad : AbsData) (curtid : val) : mpred : = \\ tid : Z,!! (tid = (curtid ad)) & & \\ data_a t sh tuint (Vint (Int . reprtid)) curtid . \end{matrix}$

Using this refinement relation, we can prove that the abstract state “ad” coincides with the concrete state “curtid”. Thus, the parent module program (e.g., the taskResched module) can directly manipulate the abstract state “ad” using the abstract functions “getCurtid_abs” and “setCurtid_abs” without knowledge of their concrete implementations.

Notice that in our verification system (Fig. 3), the assembly code is lifted to a functional specification based on our ARM assembly model (Fig. 8) directly. Thus, to verify the ctxtswitch module, we only need to prove its assembly code faithfully implements its functional specification.

After the curtid and ctxtswitch modules are verified, we start to verify the scheduler module (Fig. 9) based on the abstract state curid, rs, and ctxt in $L_{2}$ . The previous $L_{2}$ now becomes the $L_{1}$ for verification of the task scheduler module. Similarly, we separately prove $M, L_{1} ⊢ C^{M} : L_{1}^{'}$ and $L_{2} \underset{R}{⊒} L_{1}^{'}$ . As shown in Fig. 10, the corresponding API and functional specifications are the same, and the refinement proof is simple because we do not introduce any new abstract states. The main task is to prove functional correctness, which is also done using the VST. Note the separation logic predicates are removed, and all the logic reasoning is based on the abstract states.

When this step is completed, all of the functions of the EOS task scheduler have been verified on the appropriate abstract models. This means that we have defined correct specifications for our functions and verified our code. The result is the following verified modules:

$\begin{matrix} M_{curtid,} Ø ⊢_{R_abs_con} ℂ^{curtid} : L_{curtid} \\ M_{ctxtswitch}, Ø ⊢_{Ø} ℂ^{ctxtswitch} : L_{ctxtswitch} \\ M_{scheduler}, L_{curtid \circ ctxtswitch} ⊢_{id} ℂ^{scheduler} : L_{scheduler} \end{matrix}$ where, Ø means an empty set, R_abs_con means refinement relations between the abstract state and the concrete state, and id means no new abstract states are introduced.

4.3 Linking of the task scheduler

With all the modules verified, we proceed to link them together based on the functional specifications. The curtid and ctxtswitch are base modules in our case study, so their refined modules are $Ø ⊢_{Ø} ℂ^{curtld} : L_{curtld}$ and $Ø ⊢_{Ø} ℂ^{ctxtswitch} : L_{ctxswitch}$ respectively. Because there is no dependence between the curtid and ctxtswtich modules, we then apply the horizontal composition rule to compose them into a larger verified module: $Ø ⊢_{Ø} ℂ^{M_{curtid} \otimes M_{ctxtswitch}} : L_{curtid} \otimes L_{ctxtswitch},$ where the abstract state of the specifications $L_{curtid} \otimes L_{ctxtswitch}$ is the state composition of these two modules (as shown below):

Record AbsData :=

mkAbsData {

Curtid: Z; rs: CtxtStruct; ctxt: CtxtPool

Finally, we apply the vertical composition rule to link the curtid and ctxtswitch modules with the scheduler module.

$Ø ⊢_{Ø \circ R 1 \circ R 2} ℂ^{curtid} \otimes ℂ^{ctxtswitch} \otimes ℂ^{scheduler} : L_{scheduler},$

where R1 and R2 are the refinement relations between the scheduler abstract model and the curtid, ctxtswitch modules, respectively:

Definition R1

(a1: schedulerAbsData) (a2: curtidAbsData) :=

curtid a1 = Curtid a2.

Definition R2

(a1: schedulerAbsData) (a2: ctxtswitchAbsData) :=

rs a1 = rs a2 ctxt a1 = a2.

This result means that the behaviors allowed by the task scheduler specifications are refined by the scheduler C code, the curtid C code, and the ctxtswitch assembly code.

5 Conclusions

We propose a verification system for verifying a low-level task scheduler. Concerning the task scheduler usually written in different program languages and implemented using complex data structures, our verification system has several features:

supports the specification and verification of C programs with complex pointer structures

supports the specification and verification of ARM assembly code

supports modular verification framework to verify program modules at different abstraction levels.

We define different abstract levels with smaller modules (e.g. the curid and ctxtswitch modules) and composes them both horizontally and vertically to produce larger modules (e.g. the scheduler module). Machine context operations are supported in our verification system, such as context loading and context restoring. By the abstraction of task ids, machine registers, and task context data, we can verify a task scheduler naturally, as the approach readily addresses the task jump problem.

One issue not addressed in our verification system is the interrupts of processors. It is interesting to extend our framework to support verifying interrupts. Also, it is interesting to extend our framework to support tasks running over multi-processors, which is commonly seen in the modern EOSkernels.

Our long-term goal is to verify realistic EOS kernels with dynamic memory allocator and real-time task scheduling. The work presented in this paper makes a solid step toward our goal.

References

Guo

, Jiang

X-Y.

and Chen

Y-Y.

, Certification of thread context switching, J Comput Sci Technol 25(4) (2010), 827–840. DOI: 10.1007/s11390-010-1064-9.

Ferreira

J.F.

, Gherghina

, He

, et al., Automated verification of the FreeRTOS scheduler in Hip/Sleek[J], International Journal on Software Tools for Technology Transfer 16(4) (2014), 381–397.

, A Traffic Motion Object Extraction Algorithm, International Journal of Bifurcation and Chaos 25(14) (2015), Article Number 1540039.

, Wang

and Zou

, Research on internet information mining based on agent algorithm, Future Generation Computer Systems 86 (2018), 598–602.

, Wang

and Yuntao

, Bidirectional cognitive computing method supported by cloud technology, Cognitive Systems Research 52 (2018), 615–621.

Klein

and Tuch

, Towards verified virtual memory in L4[J], TPHOLs Emerging Trends 4 (2004), 16.

Beringer

, Petcher

, Katherine

Q.Y.

, et al., Verified Correctness and Security of OpenSSL HMAC[C]//, 24th USENIX Security Symposium (USENIX Security 15) (2015), 207–221.

Cao

, Beringer

, Gruetter

, Dodds

, Appel

A.W.

, VST-Floyd: A separation logic tool to verify correctness of C programs, J Autom Reasoning 61(1-4) (2018), 367–422.

Leroy

, The CompCert verified compiler[J], Documentation and user’s manual. INRIA Paris-Rocquencourt (2012), 53.

10.

Blazy

and Leroy

, Mechanized semantics for the Clight subset of the C language[J], Journal of Automated Reasoning 43(3) (2009), 263–288.

11.

Büchi

and Sekerinski

, Formal methods for component software: The refinement calculus perspective[C]//European Conference on Object-Oriented Programming. Springer, Berlin, Heidelberg (1997), 332–337.

12.

Bensalem

, Bozga

, Legay

, et al., Component-based verification using incremental design and invariants[J], Software & Systems Modeling 15(2) (2016), 427–451.

13.

, Koenig

, Ramananandro

, et al., Deep specifications and certified abstraction layers[C]//ACM SIGPLAN Notices, ACM 50(1) (2015), 595–608.