Operating-system verification gains increasing research interest. The complexity of such systems is, however, challenging and many endeavors are limited in some respect: Some projects focus on a particular aspect like memory safety, not pursuing functional correctness. Others restrict their verification efforts to a single layer of software, assuming correctness of those below. Only few projects aim at pervasive formal verification of a computer system over several software layers. In our paper, we present an approach to the formal specification of a microkernel-based operating system at several layers and glance on our verification experience with this model stack. From our experience, we conclude that pervasiveness entails more than just cumulative verification efforts on several layers. In fact, it is a challenging task to integrate models and proofs into a uniform, coherent theory.
Consequently, we need an assembly semantics, a C semantics and a
simulation theorem between both semantics. Leinenbach and Petrova [
Outline. In Sect. 2, we explain the fundamentals of our operating system. This section comprises a sketch of the correct compiler, a survey of the features of our microkernel, and an outline of the system’s implementation design. With these prerequisites in place, we give an overview of our model stack in Sect. 3. Certainly, we cannot descend into all details of the stack in this paper.1 Hence, we confine ourselves to aspects of encapsulation and state partitioning. In Sect. 4, we describe our formal specification of the generic interface between the user processes and the kernel. Moreover, we sketch our formal model for assembly and C0 processes. This process abstraction is an elementary prerequisite for the model of communicating user processes as well as for the top-level specification of the operating system. We illustrate in Sect. 5, why we use the process abstraction already in the Vamos specification and how we have constructed the latter model in order to support the abstraction towards Coup and the top-level specification. We conclude in Sect. 6. 2 2.1
In this section, we summarize work of Leinenbach and Petrova [
The inline-assembly statement is an important feature for language extensions. Though the effect of this statement cannot be expressed in the formal C0 semantics, the compiler literally embeds the given assembly code into the compilation. Using this hook, we can implement C0 functions that use inline assembly in order to extend C0 by a functionality that cannot be expressed by other C0 statements. 1 The complete Isabelle/HOL theories of the models as well as detailed documentation are made available at the Verisoft repository, see <http://www.verisoft.de/VerisoftRepository.html>
For C0 and for the assembly language, two small-step transition semantics have been formalized in Isabelle/HOL. Leinenbach has formally proven compiler correctness by a stepwise simulation between both semantics. Below, we describe the semantics in detail. We often deal with structured values, which we define by enumerating the components in prose, e. g., “a value x consisting of two components this and that ”. We refer to a single component with a dot, e. g., x.this refers to component this of value x. An update of this component is denoted by x [this := q].
C0 Semantics. For lack of space, we can only glance at the C0 semantics. C0 programs are statically represented by the program environment Γ , which comprises a symbol table of global variables, a type-name environment, and a function table. The dynamically changing state sC0 of a C0 program in execution is composed of – the remaining program sC0.prog, and – the current state of the program variables sC0.mem.
In the following sections, we assume an evaluation function get-val for the lookup, and an update function set-val for the manipulation of a certain variable in the memory. We refer to the value of expression e in state sC0 by get-val (sC0, e). If we update the left-value l in state sC0 with some expression u, we denote the resulting configuration by set-val (sC0, l, u).
The transition relation δCse0q of this semantics is a partial function.
The Target Assembly Language. The assembly semantics was developed for
the risc processor Vamp [
We denote the state space of the assembly semantics by Sasm. Assembly computations are modeled by the partial function δasesqm ∈ Sasm * Sasm. Note that the effects of exceptions like illegal page faults cannot be fully determined from the assembly-machine state. In that case, δasesqm gets stuck. But with sufficient resources, a compiled C0 program does not generate exceptions during normal execution. Moreover, the memory size sasm.V can neither be read nor changed by the assembly machine itself but depends on the operating-system kernel. We extend the semantics accordingly in Sect. 4. 2.2
In this section, we sketch the features of Vamos and explain the fundamental access-control mechanism that establishes the process roles “privileged process” and “device driver”.
Our microkernel Vamos performs the following tasks: (a) enforcement of a minimal access control, (b) process management, (c) memory management, (d) priority-based round-robin scheduling, (e) support for user-mode device drivers, and (f) inter-process communication (IPC). Processes can control these tasks via the kernel’s application binary interface (ABI). Table 1 lists the kernel calls that constitute the ABI.
Most kernel calls are reserved for so-called privileged processes. Thus, only a privileged process can bring up new processes or kill existing ones, alter the memory consumption of processes, change their scheduling parameters, or control the registration of device drivers. Any process, however, might use the IPC mechanism. Thus, the privileging serves as a minimal access control. We presume that the privileged processes constitute the user-mode parts of the operating system and implement a more sophisticated access-control mechanism. Non-privileged processes may then communicate with the privileged processes in order to request kernel services on their behalf.
When Vamos boots, it launches one single process, the init process. This process is privileged and has to set up the required servers of the operating system, start and register the device drivers, and possibly run initial applications.
A device driver is a user process, which is designated for the communication with certain devices. Only if a process is registered as a driver for a particular device, it may place read or write requests from or to that device, respectively. Moreover, the device driver is notified of interrupts from that device. 2.3
Fig. 1 depicts the implementation structure of Vamos. The lowest software layer
is called communicating virtual machines (CVM). This layer encapsulates all
hardware-specific low-level functionality, which is possibly using inline assembly.
CVM has two major tasks: memory virtualization and switching between
different threads of execution. Hence, CVM includes a page-fault handler with a
simple memory swapping facility [
Using this framework, we have implemented our microkernel Vamos in C0 without extra portions of inline assembly. On every kernel entry, CVM preserves the old context, establishes a suitable C0 environment and calls the function kdispatch of Vamos. For the manipulation of the user memory or registers, Vamos may call the primitives of CVM. The return value of kdispatch determines, which user machine resumes when the kernel execution finishes. rseU eodm
App
SOS
App kcalls kcalls
Vamos
primitives e o kdispatch d m m e t s y S
CVM Hardware
SOS Coup (C0+asm)? (C0+asm)? Vamos
asm? CVM
C0 asm?
Fig. 2. Schematics of our model stack
While CVM and Vamos run in the privileged system mode of the processor, user machines run in the unprivileged user mode. In the figure, we labelled one user machine “SOS” for simple operating system and the others “App” as abbreviation for application. The SOS constitutes the highest layer of our operating system. It features an advanced rights management with different users, implements a sophisticated access control to kernel services like process creation and provides further services like file-system and network access. All user machines interact with the kernel via kernel calls. The special instruction trap causes an exception, which is handled in Vamos. Vamos can examine and alter the state of the user machine using CVM primitives, thus identifying the user machine’s specific request and storing the kernel’s corresponding response. 3
In analogy to the software stack, we have developed a model stack. For each software layer, this stack contains a specification that fully describes the observable behavior of this layer. The specification describes the full functionality of the software layer, on the one hand, and forms the foundation for the simulation proofs for the more abstract layers, on the other hand. We build the model stack as a means of verifying statements about the real system on a convenient, abstract layer. Such statements include safety and liveness properties.
Fig. 2 shows our model stack. The lowest model describes CVM. This model
comprises a kernel machine, given in the C0 semantics, and a number of user
machines with virtual memory, given in the assembly semantics. The kernel runs
in system mode with disabled interrupts. The user machines, in contrast, may
be interrupted after each assembly instruction, thus we model them on assembly
level. We will not descend into the details of this model in the present publication
because it has been described earlier [
We can instantiate the kernel of CVM with the Vamos implementation, i. e., the C0 program that implements (the hardware-independent part of) our microkernel is executed as CVM’s kernel machine. The Vamos model specifies the behaviour of the resulting system. In short, this model establishes assembly processes that communicate with the kernel via a well-defined interface, the kernel ABI. A code-correctness proof for the Vamos implementation establishes the simulation theorem between the instantiated CVM model and the Vamos specification.
While the Vamos processes use the assembly semantics, the SOS and the applications are written in C0. The kernel ABI is encapsulated in a few library functions. Except for the library functions, the verification of these programs should certainly employ the more abstract C0 semantics. For this purpose, we designed the model communicating user processes (Coup). This model simulates Vamos but it abstracts from the scheduler and establishes C0 processes. We need to abstract from the particular Vamos scheduler because of the different granularity of the program semantics: The execution of a process might be suspended and resumed on every assembly instruction but a C0 statement usually contains several assembly instructions. The simulation proof has three parts: (1) The execution traces of Coup should contain all traces of Vamos. (2) There is a confluent reordering of any execution trace such that there is no scheduling event during a single C0 statement. (3) The kernel library is correctly implemented.
We can instantiate one of the C0 processes with the implementation of SOS. The SOS model specifies the behaviour of the resulting system. The simulation between both models can be shown by the functional correctness of the SOS implementation. 4
In this section, we formalize the interface between the processes and the kernel. Both kernel models, the Vamos specification and the Coup model, use this process abstraction in order to access and manipulate processes. Our abstraction is based on the observation that Vamos interacts with processes only via a well-defined interface, the kernel ABI. Hence, we can encapsulate processes in a self-contained input-output automaton, thereby hiding the internal state and just exposing the generic interface.
We define a process as input-output automaton described by a tuple (Sproc, Σproc, Ωproc, ωproc, vm-sizeproc, init proc, δproc) with state space Sproc, input alphabet Σproc, output alphabet Ωproc, output functions ωproc and vm-sizeproc, initialization function init proc, and transition function δproc.
While the state space Sproc depends on the individual process abstraction, the interface between the kernel and the processes is naturally shared by all process abstractions. This interface is entirely defined by Σproc and Ωproc.
The output alphabet Ωproc enumerates all possible kernel calls. Additionally, we have to treat a few error cases. As the kernel calls are internally identified by a number, a process might specify an invalid number. This condition is represented by the special output value undefined trap. Moreover, a process might generate exceptions like an arithmetic overflow or an illegal page fault. These exceptions are collectively represented as value runtime error. Finally, the output ε denotes the intention to perform a local computation.
The input alphabet Σproc reflects all kernel-initiated changes of a process. These comprise all possible responses to kernel calls, on the one hand, and the demand to change the amount of virtual memory, on the other hand. While the former are the synchronous reaction to a kernel call, the latter may be issued asynchronously at any stage of a process. In order to perform a local transition, we pass the input ε to the transition function δproc.
In addition to the usual functions δproc ∈ Σproc × Sproc → Sproc for transitions and ωproc ∈ Sproc → Ωproc for the output, we use two more functions in our process abstraction. In order to compute the overall memory consumption of the process system, Vamos needs to know the amount of virtual memory that is currently occupied by every process. The function vm-sizeproc ∈ Sproc → N provides the necessary information. When a new process is created, Vamos has to translate a representation of a given binary executable file into the corresponding, initial process state. We specify this translation in the function init proc ∈ N? → Sproc.
For the kernel specification, the generic abstraction of processes as selfcontained input-output automata is rather a matter of taste than necessity. However, this generic process abstraction is a cornerstone of the Coup model. Moreover, it is crucial for the simulation theorem between Vamos and Coup because both models mainly differ in the process abstraction. Hence, it proved to be beneficial that many definitions of the specification are parametrized over the process abstraction and can thus be reused in Coup as well. Finally, the introduction of this parameter on the whole Coup model is just a logical consequence because it paves the way for the integration of other language semantics.
In the following, we refine the generic abstraction with specific process models for assembly and C0.
Assembly Processes. We reuse the state space Sasm of the assembly semantics for our assembly processes. Based on this state space, we now define the output functions ωasm and vm-sizeasm, the transition function δasm, and the initialization function init asm. The function vm-sizeasm simply returns the value of the component V of the current state: vm-sizeasm(sasm) = sasm.V . However, the definitions for other functions are too complex to fully present them here. We constrain ourselves to an exemplary excerpt.
Fig. 3 depicts the formal definition of the output function ωasm and the transition function δasm for the call process clone. We assume that sasm is the state of an assembly process. The predicate trap holds iff the current instruction is a trap, and the function simm extracts the sign-extended immediate constant from the current instruction. If there is a trap with immediate constant 2, the output function will return the pair of value process clone and the content of register 11. Let us now assume that the kernel recognizes this output from the current process but the process is not privileged. In this case, the kernel signals this error condition by passing value err unprivileged via the transition function to the current process. Then, the transition function updates the register 22 with the corresponding error code and increases the program counters. trap(sasm) ∧ simm(sasm) = 2 =⇒ ωasm(sasm) = (process clone, sasm.gpr(11))
2 gpr(22) := −4 3 δasm(err unprivileged, sasm) = sasm4 pc := sasm.pc + 4 5
dpc := sasm.dpc + 4 C0 Processes. In order to represent C0 processes, we define an automaton with the following signature: (SC0, Σproc, Ωproc, ωC0, vm-sizeC0, init C0, δC0)
Any state sC0 ∈ SC0 comprises the static program environment as well as the dynamic program state of the C0 machine as described in Sect. 2.1. We store the program environment because processes might dynamically be created and killed, hence the program might change. The output functions ωC0 and vm-sizeC0, the transition function δC0, and the initialization function init C0 are defined in analogy to their assembly-process counterparts.
For example, the formal definition of the output function and the transition function for the call process clone is given in Fig. 4. We assume that sC0 is the current state of a C0 process. The component sC0.prog denotes the remaining program of the process. We consider the first statement of the program. If this statement is a call to the function vc process clone, we define the output of ωC0 as the pair of process clone and the value of the first argument to the function call. Let us now assume that the kernel recognizes this output from the current process, clones the given process, and computes the value hnnew as new identifier for the clone. It would then pass this value via the transition function to the current process, thus signalling the success of the clone operation. In this case, the transition function updates the memory sC0.mem at the address designated by the left-value e with value hnnew and removes the function call from the remaining program. 5
In the previous section, we described our process model. Now, we embed the processes into the two concurrent kernel models, the Vamos specification, and the Coup model. The former specifies the exact behaviour of our microkernel with a particular scheduler. This model is used for code verification. The latter abstracts the scheduler and focusses on the interaction of the processes with the sC0.prog = ”e = vc process clone(e0); r”
» mem := set-val(sC0.mem, e, hnnew) – =⇒ δC0((succ new process, hnnew), sC0) = sC0 prog := r microkernel.We need this more abstract model in order to describe the reordering of interleaved sequences and to introduce C0 processes.
Both models are Moore machines. We describe the kernel specification with the tuple (Sv, s0v, Σˆ, Ωˆ, ωv, δv) and the Coup model with (Svc, s0vc, Σˆ, Ωˆ, ωvc, δvc). The state spaces Sv, Svc contain the initial states s0v and s0vc, respectively. For device communication, we use the input alphabet Σˆ and the output alphabet Ωˆ. The functions ωv and ωvc determine the output in a current state. Finally, δv and δvc describe the transitions of the models. The notable difference between these machines regards the determinism: While the Vamos specification is fully deterministic, Coup features a non-determinism in its scheduling decisions. Consequently, the transition relation δv is functional while δvc is not.
Below, we introduce the different components of the models side by side.
Device Communication. Our kernel uses memory-mapped I/O for device
communication. Hence, the output alphabet Ωˆ comprises read and write accesses to
device addresses. The input alphabet Σˆ consists of interrupt lines and optionally
incoming data. Hillebrand et al. [
A central part of the Vamos specification are the scheduling data structures. The component sv.schedds is divided into sub components. The current time time ∈ N is a counter for clock ticks. Process-specific scheduling information for active processes is collected in the partial function procdb that maps PIDs to a record of (a) the time slice tsl , (b) the amount of consumed time ctsl , and (c) the absolute timeout to. If a process is found to be computing when a timer interrupt raises, the component ctsl is increased until the process has finally run for tsl ticks. In this case, another process is scheduled. If a process calls the kernel for IPC and no partner is ready for communication, the absolute timeout to is computed from the current time and the relative timeout that has been specified with the call.
Moreover, the scheduler maintains different queues for scheduling. They are represented as finite sequences in the Vamos specification. Namely, there is a ready queue ready(prio) of schedulable processes for each priority prio ∈ {0, 1, 2}. The processes that cannot currently be scheduled (because they are waiting for an IPC partner) are held in a queue named wait .
In Vamos, the current process is the first process in the highest, non-empty ready queue. If all ready queues are empty, the current process is undefined. Formally, we define the function cup as: cup(sv.schedds) = p ⇐⇒ ∃i : sv.schedds.ready(i) = (p, . . . ) ∧
∀ j > i : sv.schedds.ready(j) = ()
The corresponding Coup state svc inherits most components of sv. Only two components change: The process abstraction becomes a model parameter, i. e., component svc.procs of a Coup state svc is a partial function from PIDs to a generic state space Sproc for processes. Moreover, the scheduling data structures are replaced by a current-process indicator. We retain the current process in the state in order to compute the output from the current state. The output function ωvc signals the demand for device communication. In order to determine this demand, we need to employ the output function ωproc of the current process. Consequently, we fix this process beforehand instead of including transitions for all ready processes in the transition relation.
Transitions. A transition δv(σˆ, sv) of the Vamos specification under the device input σˆ ∈ Σˆ has up to three phases: 1. If the current process cp = cup(sv.schedds) is defined, we consult its output ωproc(sv.procs(cp)) and compute the response according to the current Vamos state. For instance, if a process calls process clone, we check for sufficient privileges and resources and choose the corresponding response σ ∈ Σproc for success or failure. With this response, we advance the current process: sv [procs(cp) := δproc(σ, sv.procs(cp))]. 2. If the timer-interrupt line is raised, the scheduler increases the clock-tick counter sv.schedds.time and the consumed time sv.schedds.procdb(cp).ctsl of the current process. Moreover, the scheduler wakes up all processes p with elapsed timeouts. 3. Finally, Vamos delivers interrupts to waiting drivers and saves the remaining interrupts for later delivery in sv.devds. σ
The Coup transitions behave very similarly. However, a transition svc ←→ s0vc ∈ δvc, obtains cp directly from svc.cup. Moreover, the only visible effect of the second phase is the wake-up of certain waiting processes. This effect is simulated non-deterministically and independently from the timer interrupt. Reusability. As mentioned earlier, we worked hard to reuse as much definitions as possible in the different layers of abstraction. For example, in contrast to the Coup model, the kernel specification does not actually rely on the encapsulation of processes as self-contained input-output automata. Since Vamos only considers assembly processes, it would be easier to directly manipulate the state of these processes. However, in order to literally reuse update functions and definitions, we invested the extra work and already introduced the input-output automata at this level of our model stack.
Consider the formal definition of the function v clone updt procs in Fig. 5. This function describes the necessary updates in case of a successful call to process clone. Without going into detail, depending on the relation between the calling process (psubj) and the process that was cloned (pobj), this function updates the state of the calling process, the state of the cloned process, and the state of the new process. The important thing about this definition is that the updates are presented in a process-abstraction independent manner. Rather than updating particular registers, as it would suffice for assembly processes, we feed the generic transition function δproc with generic input, e.g. (succ new process, hnnew). Now, this generic interface between kernel and processes allows us to use v clone updt procs in both models, i.e. Vamos and Coup. Proceeding in a similar way with all kernel calls keeps the models clear and maintainable. Furthermore, tedious equivalence proofs between Vamos and Coup are avoided. 6
Related Work. With the CLI stack [
if x = psubj then δproc((succ new process, hnnew), procs(psubj)) else if x = pnew ∧ psubj = pobj then δproc((succ new process, 0), procs(psubj)) else if x = pnew then procs(pobj) else procs(x) Fig. 5. Formal definition of the function v clone updt procs that computes the component procs after a call to process clone and its machine code implementation was proven to be correct. However, this kernel is fairly simple compared to modern microkernels.
Many recent projects undertake verification efforts on modern microkernels.
Among them are L4.verified [
Traditionally, concurrent systems are described by the Calculus of
Communicating Systems [
Discussion. We presented an approach to a pervasive, formal specification of a microkernel-based operating system. The formal models of our microkernel Vamos and the SOS occupy almost 400 kB and comprise about 8,000 lines of specification. The formalization took us about 48 person months. The different specification layers resemble essentially the implementation layers.
A recurring problem was the semantic gap between the high-level implementation language C0 and certain hardware details that were manipulated by the considered programs. Such details concerned hidden hardware components like devices, on the one hand, and the granularity of atomic operations on the hardware level, on the other hand. Both problems arose simultaneously when we argued about C0 processes: In pure C0, we cannot express kernel calls. Hence, we extended the original C0 semantics by a library of functions that implement the kernel calls using inlined assembly. Moreover, user machines may be interrupted after the execution of any assembly instruction. Consequently, we had to justify that we may confluently shift all rescheduling events to statement boundaries before we could argue about C0 processes. In non-pervasive approaches, these challenges are likely to be skipped.
When we began to specify the different layers of our operating system, we started with independent models. As expected, many parts of the formal models overlapped because we specified the same operating system at several layers of abstraction. After a short period of evaluation for each abstraction layer, we coupled the models as tight as possible in order to minimize the proof efforts for the simulation theorems between adjacent models.
This ambivalent approach was very successful. In the very beginning, the specifications change very often, such that maintaining dependencies between them would be very tedious and distracting from the individual problems. As soon as the models stabilized, however, there was a common ground for a tight meshing. The synergies between the layers could easily be identified and utilized.
The key to shared definitions between the Vamos specification and the Coup model was twofold: On the one hand, we unitized the state space in a way that permits easy abstraction between the different abstraction layers. On the other hand, we established the process abstraction already at the Vamos specification. Both arrangements together enabled a very tight mesh, which could even be reused in the SOS specification.
Of course, this tight mesh of the models has drawbacks: The specification of an abstract layer depends massively on the underlying layers, which impedes the understanding of this model. Moreover, even the lower layers became more complicated, so for instance, when the process abstraction was already introduced in the Vamos specification. Finally, several layers were affected whenever the abstraction at one level turned out to be wrong.
From our experience, however, we conclude that the advantages outweigh the drawbacks. We saved valuable time by reusing the definitions, which we otherwise had spent in distracting equivalence proofs. For instance, we succeeded with the step-wise simulation proof between the Vamos specification and the Coup model within two months. We have proven this simulation for most kernel calls within days. Most of the time, however, we spend with the verification of IPC. This effort was caused by a considerably simpler modelling of IPC in Coup, which became possible after the scheduler was abstracted. In this particular case, the simpler modelling was desirable and hence, we invested the additional time for the proof. Independent models, however, would possibly have caused such an overhead for every kernel call.
In the code-correctness proof for Vamos, there is only a minimal overhead (hours) induced by the use of the process abstraction in the specification. All in all, we invested about 18 person months to show the correctness of the IPC send call. Including all auxiliary functions, the implementation of this call accounts for nearly half the code size and comprises the most complex parts. Again 18 person month had been spent on the functional verification of the file system and the hard disk driver code in the SOS. This code covers 20% of the SOS implementation.
Summary. The fundamental difference of our “pervasive” approach compared to “incremental” approaches that focus on a single layer at a time regards the design of specifications: At first, models are usually adapted to the actual verification goal. If it is the only goal, to show that the formal specification precisely describes the implementation, the specification tends to move closely towards the implementation. If a model is used as fundament of an underlying component without a proof, there is a likelihood that the model over-abstracts the actual implementation. At second, regarding one single layer at a time necessarily leads to self-contained, independent models. When combining those different layers later on, there is a tremendous proof effort necessary to establish simulation theorems between the adjacent layers. Our approach prevents this effort by the specification design.