Formal specification of a simple operating system

Abstract

Within the Verisoft project, we aim at the pervasive modeling, implementation, and verification of a complete computer system, from gate-level hardware to applications running on top of an operating system. As an adequate representative for such a system we choose a system for writing, signing, and sending emails. The starting point of our work was a processor together with its assembly language, a compiler for a type safe C variant and a micro kernel. The goal of our work was to develop a (user-mode) operating system that bridges the gap between micro kernel and user applications. That is, formally specify and implement a system that, on the one hand, is built right on top of our micro kernel and, on the other hand, provides everything necessary for user applications such as an SMTP server, a signing server, and an email client. Furthermore, the design of this system should support its verification in a pervasive context. Within this thesis, we present the formal specification of such an operating system. Along with this specification, we (i) discuss the current state-of-the-art in formal methods applied to operating-systems design, (ii) justify our approach and distinguish it from other people's work, (iii) detail our implementation and verification stack, (iv) describe the realization of our operating system, and (v) outline the verification of this system.

Innerhalb des Verisoft-Projekts streben wir die durchgängige Modellierung, Implementierung und Verifikation eines kompletten Computersystems, von der Hardware auf Gatterebene bis hin zu Benutzeranwendungen, an. Ausgangspunkt unserer Arbeit war ein Prozessor inklusive Assembler Sprache, ein Compiler für eine typensichere C Variante und ein Mikrokern. Ziel unserer Arbeit war es, ein Betriebssystem (auf Benutzerebene) zu entwickeln, welches die Verbindung zwischen Mikrokern und Benutzeranwendungen herstellt. Das bedeutet, ein System formal zu spezifizieren und zu implementieren, welches auf der einen Seite direkt auf dem Mikrokern aufsetzt und auf der anderen Seite alle Voraussetzungen für Benutzeranwendungen wie einen SMTP Server, einen Signatur Server und ein E-Mail Programm erfüllt. Außerdem soll das Design dieses Systems seine durchgängige Verifikation unterstützen. In dieser Arbeit präsentieren wir die formale Spezifikation eines solchen Systems. Ferner (i) diskutieren wir den aktuellen Stand im Bereich der formalen Methoden im Betriebssystemdesign, (ii) rechtfertigen unseren Ansatz und differenzieren ihn von dem anderer, (iii) stellen die unterschiedlichen Implementierungs- und Verifikations-Schichten unseres Projektes vor, (iv) beschreiben unsere Umsetzung des Systems und (v) skizzieren seine Verifikation.