SciDok

Eingang zum Volltext in SciDok

Lizenz

Dissertation zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-24206
URL: http://scidok.sulb.uni-saarland.de/volltexte/2009/2420/


OS verification extended : on the formal verification of device drivers and the correctness of client/server software

Alkassar, Eyad

pdf-Format:
Dokument 1.pdf (1.316 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Betriebssystem , Verifikation , Treiber <Programm> , Festplatte , Client-Server-Konzept , Implementierung , RPC
Freie Schlagwörter (Deutsch): Gerätetreiber , Client/Server Software
Freie Schlagwörter (Englisch): OS veri cation , device driver , client/server software , hard disk , remote procedure call
Institut: Fachrichtung 6.2 - Informatik
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Paul, Wolfgang (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 17.07.2009
Erstellungsjahr: 2009
Publikationsdatum: 15.09.2009
Kurzfassung auf Englisch: This thesis tackles two important challenges in OS veri cation: The formal verification of device drivers and the correctness of client/server software. Device drivers are an integral part of system software. Not only high-level functionality such as le I/O depends on devices. Even basic OS features, such as demand paging, need correctly implemented drivers. In this thesis, we show how to pervasively integrate devices and their drivers into a language stack reaching from the level of assembly up to high-level languages. This stack is leveraged for the formal veri fication of a simple hard disk driver, which is subsequently embedded into Verisoft's micro kernel. To the best of our knowledge, this marks the rst formal functional veri cation of a device driver against a realistic device and system model. Remote procedure calls (RPCs) lie at the heart of any client/server software. In the second part of this thesis, we present a speci cation of an RPC mechanism and we outline how to verify an implementation of this mechanism at the code level. The formalization is based on a model of user processes running concurrently under a simple OS, which provides inter-process communication and portmapper system calls. A simple theory of non interference permits us to use conventional sequential program analysis between system calls. To the best of our knowledge this is the first
treatment of the correctness of an entire RPC mechanism at the code level.
Kurzfassung auf Deutsch: Diese Arbeit behandelt zwei wichtige Probleme in der Veri kation von Betriebssystemen (BS): Die formale Veri kation von Gerätetreibern und die Korrektheit von Client/Server Software. Grundlegende Funktionen eines BS, wie z.B. Demand Paging, setzen korrekt implementierte Treiber voraus. In dieser Arbeit zeigen wir auf, wie Geräte nahtlos in allen Semantikschichten integriert werden können|von Assembler bis hin zu einer C ähnlichen Hochsprache. Diese durchgängige Theorie wird anschließend verwendet, um einen einfachen Festplattentreiber (Teil des Verisoft Mikrokerns) formal zu verifi zieren. So weit uns bekannt, stellt dies die erste formale Veri kation eines Treibers im Kontext eines realistischen Geräte- und Systemmodells dar. Implementierungen von Client/Server Software basieren oftmals auf Remote Procedure Calls (RPCs). Im zweiten Teil dieser Arbeit, spezi zieren wir einen solchen RPC Mechanismus und skizzieren dessen Veri kation auf Codeebene. Die Formalisierung basiert auf einem Modell von Benutzerprozessen die nebenläufi g in einem einfachen BS ausgeführt werden. Dieses BS stellt Interprozess-Kommunikation und Portmapper Funktionalität über spezielle Systemaufrufe zur Verfügung. Um sequentiell über einzelne Prozesse argumentieren zu können, füuhren wir eine kleine Theorie
zur Bestimmung der Abhängigkeit von Systemaufrufen ein. So weit uns bekannt, behandelt diese Arbeit erstmals die Korrektheit eines vollständigen RPC Mechanismus auf Codeebene.
Lizenz: Standard-Veröffentlichungsvertrag

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English