Sammler Group

Programmiersprachen und Verifikation

Low-Level-Systemsoftware wie Betriebssysteme oder Hypervisoren ist das Herzstück moderner Computersysteme. Solche Systemsoftware stellt oft wichtige Komponenten bereit, die die Zuverlässigkeit und Sicherheit des Gesamtsystems gewährleisten. Das bedeutet im Umkehrschluss, dass Fehler und Schwachstellen in solcher Low-Level-Systemsoftware zu katastrophalen Ausfällen und Sicherheitsproblemen führen können. Das Aufspüren und Verhindern solcher Fehler in Low-Level-Systemen ist daher von entscheidender Bedeutung, um eine zuverlässige Grundlage für die moderne computerbasierte Welt zu schaffen.

Ein wichtiger Ansatz zur Beseitigung solcher Fehler und Schwachstellen ist die formale Verifikation. Im Gegensatz zum Testen, welches das Vorhandensein von Fehlern für bestimmte Eingaben nachweisen kann, beweist die formale Verifikation die Abwesenheit ganzer Klassen von Fehlern und Schwachstellen für alle Eingaben, indem sie einen Beweis dafür erbringt, dass das Programm eine mathematische Spezifikation erfüllt.

Die Sammler Gruppe entwickelt neuartige Ansätze und Werkzeuge, welche die formale Verifikation von realen Programmen ermöglichen, wobei der Schwerpunkt auf Low-Level-Software liegt. Um dies zu erreichen, erstellt die Gruppe realistische Modelle von Programmiersprachen wie C oder Assembler, welche die Feinheiten, auf die Programmierer in Low-Level-Sprachen angewiesen sind (z. B. das Verhalten der zugrunde liegenden Architektur), genau erfassen, und entwickelt dann Verifikationsmethoden, die realen Code anhand dieser Modelle verifizieren können. Die Arbeit der Gruppe reicht von der Weiterentwicklung der theoretischen Grundlagen der Verifikation – z. B. für Beweismethoden für die Interaktion verschiedener Programmiersprachen im selben Programm – bis zur Entwicklung praktischer Verifikationswerkzeuge, die eine automatische Verifikation ermöglichen und gleichzeitig maschinell überprüfbare Korrektheitsnachweise in einem Beweisassistenten erzeugen.