Formal verifiziertes Kompilieren

CompCert ist ein formal verifizierter optimierender C-Compiler. Er ist insbesondere zum Kompilieren sicher­heits­kritischer Software gedacht, die den aller­höchsten Standards entsprechen muß. Als Eingabe akzeptiert er den größten Teil der C99-Spezifikation, mit wenigen Einschränkungen und einigen Erweiterungen. Als Ausgabe erzeugt er Assembler-Code für ARM, PowerPC und x86.

Was macht CompCert einzigartig?

Im Gegensatz zu allen anderen Compilern ist CompCert mithilfe computerunterstützter mathematischer Beweise formal verifiziert. Damit entspricht der ausgegebene Maschinencode bewiesenermaßen exakt der Semantik des eingegebenen C-Codes.

Dieses Maß an Vertrauen in die Korrektheit des Kompilierungsprozesses ist beispiellos und einmalig. Nur mit CompCert können Sie den allerhöchsten Anforderungen der striktesten Standards sicher genügen.

CompCert-Diagramm

Die formale Beweisführung deckt die gesamte Überführung des abstrakten Syntax­baumes in Maschinen­code ab. Zum Präpro­zes­sie­ren und Erzeugen von Objekt­dateien und Executables müssen ein externer C-Präprozessor, Assembler, Linker und C-Bibliotheken benutzt werden. Diese nicht­verifizierten Schritte sind allerdings wohl­verstanden und aus der Implementierungs­sicht robust. Das konnten Regehr, Yang et al. im Jahre 2011 auf einer Vorläufer­version von CompCert zeigen:

Das Verblüffende an unseren CompCert-Ergebnissen ist die Abwesenheit von Middle-End-Bugs, die wir in allen anderen Compilern gefunden haben. Mit Stand Anfang 2011 ist die Entwicklungs­version von CompCert der einzige Compiler, für den Csmith keine Falschcode-Fehler findet. Dabei haben wir alles versucht und etwa sechs CPU-Jahre Rechen­zeit der Aufgabe gewidmet. CompCerts offen­kundige Unverwüst­lichkeit ist ein starkes Argument dafür, daß innerhalb eines Beweis­systems mit maschinellen Sicherheits­überprüfungen entwickelte Compiler­optimierungen dem Benutzer eindeutige Vorteile bringen.“

Ihre Vorteile

Verfügbarkeit

CompCert erzeugt Maschinencode für ARM, PowerPC (32-Bit) und IA32 (32-Bit-x86).

Die Entwicklung wird geleitet durch Xavier Leroy am französischen Nationalen Forschungsinstitut für Informatik und Automatisierung, INRIA. Für nichtkommerzielle Zwecke ist der Einsatz von CompCert kostenlos. Wir bieten Lizenzen und Kundenbetreuung für kommerzielle Benutzer an und tragen aktiv zur Weiter­entwicklung des Tools bei.

Quellcode und Dokumentation (inklusive der Compiler­beweise) stehen für Sie auf INRIAs Seite zum Download bereit.

Der Quellcode ist auch über GitHub erhältlich.