Teilprojekt 2: Akademisches System

Als Teil des Verisoft-Projekts soll ein durchgehend verifiziertes System (das Akademische System) zum Schreiben, Signieren und Senden von E-Mails konstruiert werden. Das akademische System repräsentiert einen vertikalen Querschnitt eines realen Standard-Computersystems, das alle Ebene umfasst, von der Hardware auf Gatterebene bis hin zu nebenläufigen Programmen. Die Eigenschaften des akademischen Systems entsprechen dabei den gewünschten Anforderungen an reale Systeme. Wir beschreiben die Komponenten des Akademischen Systems von unten nach oben.

Verisoft E-Mail System

Prozessor Hardware

Die Hardware-Plattform in Teilprojekt 2 ist durch den VAMP (Verified Architecture Microprocessor) [2] gegeben. Der VAMP ist eine 32-bit RISC CPU mit vollem DLX-Instruktionssatz mit einem Satz von IEEE-konformen Fließkomma-Instruktionen, delayed PC, Adressübersetzung und Unterstützung von maskierbaren geschachtelten präzisen Interrupts.

Die VAMP Hardware besteht aus einer 5-stufigen Pipeline mit einem Out-of-Order-Tomasulo-Scheduler mit Reorder-Buffer [3]. Es gibt fünf Funktionseinheiten, die XPU, die MU (Memory Unit), und drei FPUs (Floating Point Units). Anweisungen haben bis zu sechs 32-Bit-Quelloperanden und liefern bis zu vier 32-Bit-Ergebnisse. Die Fließkommaeinheiten [4] sind komplett IEEE-komform und unterstützen Operationen sowohl einzelner und doppelter Präzision als auch denormale Zahlen und die alle IEEE-Exceptions in Hardware. Die FPUs sind gepipelinet und die multiplikative FPU hat einen Zyklus in der Pipelinestruktur, damit Quotienten mit Newton-Raphson-Iterationen berechnet werden können. Die Speicherschnittstelle [5] des VAMP besteht aus zwei MMUs (Memory Management Units), die jeweils auf Instruktions- und Daten-Cache zugreifen; die Caches wiederum greifen auf einen physikalischen Speicher über ein Busprotokoll zu. Die Caches unterstützen Write-Back und werden mit Snooping konsistent gehalten.

Die formale Verifikation des VAMP mit MMUs ist abgeschlossen. Der gesamte PVS-Quellcode des Beweises ohne MMUs ist hier vorhanden. Die Korrektheitsargumente für virtuellen Speicher eines Hardware-Software-Systems werden in [6,7,8] gegeben.

Compiler

Wir implementieren und verifizieren formal einen Compiler, der auf einer Small-Step-Semantik für CO basiert, unserer eingeschränkten Version von C. Die Implementierung des Compilers erfolgt in C0 selbst. Wir benutzen eine Small-Step-Semantik, damit nebenläufige Programme und Kommunikation zwischen Programmen abgedeckt werden können. Ein Korrektheitsbeweis eines CO-Compilers mit einer Big-Step-Semantik wird in den Vorlesungsnotizen von Professor Paul präsentiert [10, p. 72-94]. Die folgenden Folien geben einen Überblick über einen Korrektheitsbeweis eines Betriebssystem-Mikrokerns inklusive Compilerkorrektheit [9].

Die Spezifikation des C0-Compilers in Isabelle/HOL und seine Implementierung in C0 ist abgeschlossen. Es wurde formal gezeigt, dass die Implementierung den gleichen Assembler-Code erzeugt, wie die Spezifikation. Der Beweis, dass das generierte Assembler-Programm das ursprüngliche C0 Programm simuliert wurde schon mathematisch geführt und wird zur Zeit in Isabelle/HOL formalisiert.

Mikrokernel und CVM-Ebene

Das Berechnungsmodell der Communicating Virtual Machines (CVM) und ein Korrektheitsbeweis ihrer Implementierung, die Basis fuer Betriebssystemkernkorrektheit, wird in [10] vorgestellt. Die CVM-Ebene stellt eine hardware-unabhängige Schnittstelle für Mikrokernel und nebenläufige Nutzerprozesse bereit. Einige Teile von CVM müssen in Assembler implementiert werden, da C0, eine vereinfachte Variante von Standard-C, aus gutem Grund keine Low-Level Programmierkonstrukte enthält. Der Mikrokern basiert auf dem CVM-interface und enthält keine Assemblerteile.

Der Mikrokernel ist in CO implementiert. Die formale Verifikation ist in Arbeit.

Betriebssystem

Der Kernelaufrufe des oben erwähnten Mikrokerns sind für die Implementierung eines einfachen Betriebssystems gedacht. Es bietet E/A Operationen auf Dateien, Interprozesskommunikation, Remote Procedure Calls und Zugang zu der Peripherie als Systemaufrufe für Nutzerprozesse an.

Netzwerk und Kommunikationprotokolle

TCP/IP

Das standardisierte Internet Protocol (IP, RFC 791), das paketbezogene Kommunikation zur Verfügung stellt, und das Transport Control Protocol (TCP, RFC 793), das zuverlässige verbindungsbasierte Kommunikation bietet, sind implementiert.

Der Protokollstandard und seine relevanten Eigenschaften (Lebendigkeit, Sicherheit, Paketreihenfolge) ist formalisiert worden. Manche dieser Eigenschaften sind bereits verifiziert worden.

Mail Server (SMTP)

Der Mailserver implementiert das Simple Mail Transfer Protocol (SMTP, RFC 2821). Er sorgt für die Funktionalität von E-Mail Übertragung durch SMTP (sendmail), empfängt E-Mails durch SMTP und liefert sie an den korrekten Empfänger / Nutzer (Mailserver).

Der SMTP Protokoll ist formal spezifiziert und implementiert worden. Die formale Verifikation ist im Gang.

Anwendungsoftware

Signature Modul

Dieses Modul bietet als Funktionalität das Signieren von Texten (insbesondere E-Mails) und das Prüfen solcher Signaturen. Es benutzt einen asymmetrischen Signaturalgorithmus (RSA-PSS) mit einer SHA Hashfunktion.

Es gibt bisher eine formale Spezifikation von den Modulinterfaces und von RSA-PSS (inkl. Fehlerbehandlung). RSA und SHA1 sind in CO implementiert worden, und eine einfache Version von RSA ist verifiziert worden.

E-Mail-Client

Bis jetzt ist der E-Mail-Client die oberste Anwendung und stellt die Nutzerschnittstelle für das ganze Akademische System dar. Die Funktionalität des Clients umfaßt das Editieren, Signieren und Senden von E-Mails, sowie von Empfangen, Prüfen der Signatur, und lesen einer E-Mail.

Der E-Mail-Client ist formal spezifiziert und in CO implementiert worden. Seine Verifikation ist im Gang. Eine Arbeit über die formale Definition von Sicherheitsanforderungen von Nutzerinterfaces (wie der E-Mail-Client) ist in [1] veröffentlicht worden.

Referenzen

  1. Bernhard Beckert and Gerd Beuster. Formal Specification of Security-relevant Properties of User Interfaces. In Proceedings, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal. October 11-15, 2004.
  2. Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, and Wolfgang J. Paul. Instantiating uninterpreted functional units and memory system: functional verification of the VAMP. In CHARME 2003, volume 2860 of LNCS, pages 51-65. Springer, 2003.
  3. Daniel Kröning. Formal Verification of Pipelined Microprocessors. PhD thesis, Saarland University, Saarbrücken, Germany, 2001.
  4. Christian Jacobi. Formal Verification of a Fully IEEE-compliant Floating-Point Unit. PhD thesis, Saarland University, Saarbrücken, Germany, 2002.
  5. Sven Beyer. Putting it all together - Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.
  6. Mark Hillebrand and Wolfgang J. Paul. Virtual Memory Simulation Theorems. Slides, 2003.
  7. Iakov Dalinger, Mark Hillebrand, and Wolfgang J. Paul. On the Verification of Memory Management Mechanisms. Technical Report, 2005.
  8. Mark Hillebrand. Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.
  9. Wolfgang J. Paul, Mauro Gargano, Mark Hillebrand, and Dirk Leinenbach. Correctness of an Operating System Microkernel. Slides, 2004.
  10. Wolfgang J. Paul, Dilyana Dimova, and Mario Mancino. Systemarchitektur (German). Lecture notes, Sommersemester 2002.
  11. Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, and Wolfgang Paul. On the Correctness of Operating System Kernels. In Proceedings, 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Oxford, United Kingdom. August 22-25, 2005.

 
Revision 14 Dec 2006