Formale Spezifikation und Verifikation wesentlicher Sicherheitseigenschaften eines Mikrokerns
Zusammenfassung der Projektergebnisse
Die heute verbreitetsten Computerprogramme und Betriebssysteme sind fehleranfällig und nicht ausreichend gegen Angriffe gesichert. Obwohl diese Software ausgiebig getestet und geprüft wurde, machen wöchentlich neue Nachrichten von erfolgreichen Viren- und Wurmangriffen und Sicherheitslücken die Runde. Die Softwarehersteller reagieren darauf mit Updates und Patches. Das DFG-Projekt „VFiasco" verfolgte das Ziel, in Zukunft nicht mehr nachträglich Fehler suchen und ausbessern zu müssen, sondern im Vorfeld mathematisch deren Abwesenheit zu beweisen. Eine solche Software-Verifikation ist äußerst aufwendig und war bis vor kurzem nur für sehr kleine Programme denkbar. Durch jüngste Fortschritte auf dem Gebiet der theoretischen Informatik wurde es jedoch möglich, solch eine Verifikation auch für mittelgroße Programme (mit mehreren zehntausend Quellcodezeilen) anzugehen. Gängige Standardbetriebssysteme wie Windows oder Linux liegen weit außerhalb dieser Größenordnung, können jedoch durch den Einsatz eines kleineren, daruntergeschobenen Kerns komplett aus der Vertrauenshierarchie von sicherheitskritischer Software genommen werden. VFiasco zielte daher auf einen solchen kleinen Kern: den an der TU Dresden entwickelten Mikrokern Fiasco. VFiasco entwickelte Methoden, Modelle und Werkzeuge für die Verifikation von Software in der genannten Größenordnung. Mit diesen Instrumenten wurden beispielhaft kleinere Verifikationsaufgaben gelöst. Eine vollständige Verifikation gelang im Rahmen dieses Projekts noch nicht, ist aber in dem EU-finanzierten Folgeprojekt ROBIN geplant. Im Rahmen des Projekts entstand eine nahezu vollständige Modellierung der Semantik der System-Programmiersprache C++. Diese Semantik modelliert erstmals selbst schwierig zu formalisierende Aspekte von C++ wie das Speichermodell, Typumwandlungen, goto, longjmp und die Ausnahmebehandlung. So wird es möglich, mit hohem Abstraktionsgrad Systemprogramme zu verifizieren, ohne diese zuerst in einer typsicheren Programmiersprache neu implementieren zu müssen. Unsere Fortschritte auf diesem Gebiet waren selbst für uns unerwartet groß, sodass wir uns anders als im ursprünglichen Projektplan vorgesehen dazu entschlossen, die Original-Implementation von Fiasco als Basis der Verifikation zu verwenden. Die Verifikation eines Betriebssystems kann nicht von einem abstrakten Programmiermodell (wie flat memory] ausgehen, da es Aufgabe des Betriebssystems ist, dieses Modell überhaupt erst für Anwendungsprogramme bereitzustellen. Eine überzeugende Verifikation muss daher von wenigen Grundannahmen ausgehen, die wiedererkennbar die tatsächliche Rechnerarchitektur abbilden. Wir entwickelten daher ein formales Modell oder IA32- (x86-) Hardwarearchitektur, das physischen und virtuellen Speicher, TLBs und Seitentabellen beschreibt. Der Mikrokern Fiasco wurde im Rahmen des Projekts weiter verbessert und sicherer gemacht. Wir stopften einige Sicherheitslücken und spezifizierten und programmierten neue Funktionen, die es erlauben, Sicherheitspolitiken für Nutzerprogramme durchzusetzen. Um die vergleichsweise teure Verifikation vorzubereiten, erhöhten wir die Softwarequalität auch mit traditionellen Methoden wie Tests und Model Checking. Um Tests weitgehend automatisiert ablaufen lassen zu können, entwickelten wir ein Werkzeug, das aus Annotationen im Quelltext automatisch Unit-Tests generiert und ausführt.
Projektbezogene Publikationen (Auswahl)
- Applying source-code verification to a microkernel: The VFiasco approach. Technical Report TUD-FI02-03-Marz 2002, TU Dresden, 2002
M. Hohmuth, H. Tews, and S. G. Stephens
- Coalgebraic Methods for Object-Oriented Specification. PhD thesis, TU Dresden, 2002
H. Tews
- The coalgebraic class specification language ccsl: Syntax and semantics. Technical Report TUD-FI02-08-August 2002, TU Dresden, 2002
H. Tews
- The semantics of C++ data types: Towards verifying low-level system components. In: Proceedings of Theorem Proving in Higher-Order Logics (TPHOLs), Emerging Trends, Rom, Italy, September 2003
M. Hohmuth and H. Tews
- Predicate and relation lifting for parametric algebraic specifications. In: J. Adámek and S. Milus, editors, Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS), volume 106 of ENTCS, pages 335-353. Elsevier, Amsterdam, 2004
H. Tews
- Coalgebraische Spezifikation und Verfeinerung. Vorlesungsmanuskript, 2005
H. Tews and H. Reichel
- Semantik und Verifikation imperativer objekt-orientierter Programme. Vorlesungsmanuskript, 2005
H. Tews and H. Reichel
