B METHOD for the construction of a MICROKERNEL

The B METHOD for the construction of MICROKERNEL – Based Systems :

• Sarah Hoffmann, Germain Haugou – STMicroeletronics
• Sophie Gabriele – STMicroelectronics
• Lilian Burdy – CLEARSY

Introduction

Microkernels have been developed to minimize the size of software that needs to run in privileged CPU-Mode. They provide only a set of general hardware abstractions, which then can be used to implement an operating system with a high level of reliability and security on top.

L4 is a second generation microkernel based on the principles of minimalism, flexibility and efficiency. Its small size (about 15,000 lines of C++) and its relevance for security make it a good candidate for formal analysis. This paper describes our approach to develop a formal model of the API of the L4 microkernel.  The goal was to evaluate the possibility to model such software with formal techniques, moreover, the objectives were:

• to describe precisely the mechanisms of L4,
• to obtain a more extensive documentation of the microkernel,
• to highlight the points where the specification was incomplete,
• to prove some static properties on the kernel.

Téléchargements & liens

• Conférence : same 2005
• Projet financé par la Région Provence Alpes Côte d’Azur : dans le cadre du programme R&D « Rousset 2003-2008 » 4ème année – Convention

Basic Concepts of L4

As a microkernel L4 aims to avoid the implementation of any system policies. It focuses on the basic mechanisms that allow constructing a complete operating system in non-privileged mode. The three fundamental abstractions are: tasks, threads and inter-process communication (IPC).

Tasks provide virtual address spaces. The address space translation towards physical memory is established decentralized by the tasks themselves. Initially, sigma0, the task created first, finds the available physical memory in its address space. It can share this memory with other tasks by sending one or more pages of virtual memory.

The receiving task specifies the place where to put the pages and the kernel establishes the new mapping. The task can then access the memory or map it recursively on to other tasks. Page faults are forwarded to a specific thread, the pager, which has to resolve the fault by providing a mapping.

Mappings may be revoked (unmapped) at any time, which results in a recursive unmapping of all further mappings that have been established from that page. For this, the kernel needs to track all mappings in what is conventionally called the mapping database.

Threads are execution contexts. As such they are attached to a task and are scheduled by the kernel according to the parameters that can be changed through system calls.

IPC allows to send messages synchronously and unbuffered between two threads. The content of these messages may consists of simple registers contents and of memory regions that are copied directly into the receiving address space. Memory pages are sent to other tasks via IPC as well.

Model of the L4 API

We have constructed a representation of the L4 microkernel API using this event B formalism. We have developed an abstract model of the data inside the microkernel and described the different ways to interact with it. Those interactions are, in fact, the different system calls. In L4, a system call is an entry point that allows carrying out many different actions. We have split those different actions into different events. This allows defining more clearly what is necessary to perform a single action and what this action will modify in the kernel.

We have obtained a model describing all the system calls and a manual outlining:

• the structure and the properties of the system abstractions
• and for eachpossible action its prerequisites as well as the modifications carried out by this action.

The data structures mainly represent the memory and the threads. These structures are not described in the API, but they appear through the specification of the system calls. In the model, they correspond to the definition of constants and variables.

On the other hand, each action is guarded by a predicate on those variables defining the conditions on which the corresponding system call can be called. This guard depends also on the system call parameters.

Animation and test

To validate the model against the running code (and vice versa), we have used the Brama animator framework in order to test the code using the model as an oracle. A test case consists of a kernel pre-state and a system call with specific parameters. The corresponding test application first makes some system calls to position the kernel in the pre-state, then it executes the system call, and finally the kernel post-state is dumped into a file. Using the animator, one can also set the model in a given state, execute some events and dump the model state into a file.

We have developed an interface that allows to convert a kernel state into a model state, associating the model variables with the implementation data. We have also converted a system call into a sequence of event executions. This allows to put the kernel and the model in an equivalent state starting from a unique description, to execute the system call and to compare the two resulting states in order to validate the conformance of the code to the model.

Basic concepts of L4

To conclude, we consider that the development of this model allows us to obtain more confidence in the correctness of the API, to describe its behavior from a different point of view and to establish a deeper understanding on how it works.

The test framework allows to validate the model against an implementation; the relation between the model and the implementation is not proven (as it could be in a complete formal development with code generation) but the test allows to ensure more confidence.

For software where efficiency is such a crucial requirement that it rules out code generation, this kind of test framework can be a realistic solution to construct a validation at two levels: at specification level, when constructing the model, and at implementation level when testing it.

Références

• J. Liedtke. L4 reference manual (486, Pentium, PPro). Arbeitspapiere der GMD No.1021, GMD — German National Research Center for Information Technology, Sankt Augustin, September 1996. Also Research Report RC 20549, IBM T. J. Watson Research Center, Yorktown Heights, NY, September 1996.
• U. Dannowski, J. LeVasseur, E. Skoglund, and V. Uhlig. L4 experimental kernel reference manual, version x.2. Technical report, 2004.
• M. Hohmuth, H. Tews, and S. G. Stephens. Applying source-code verification to a microkernel — the VFiasco project. Technical Report TUD–FI02–03–März 2002, Dresden University of Technology, 2002.
• H. Tuch and G. Klein. Verifying the L4 Virtual Memory Subsystem. Proc. NICTA Formal Methods Workshop on Operating Systems Verification, Technical Report 04011005T-1, National ICT Australia, 2004.