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 CompCert 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

Der Einsatz von CompCert ist die logische Fort­führung des Einsatzes formaler Verifi­kation (statische Analyse, Model-Checking) auf der Quellcode-Ebene. Nur mit CompCert gelten alle Sicherheits­eigenschaften, die Sie auf der Quellcode-Ebene nachgewiesen haben, garantiert auch für den erzeugten Binärcode.

Ausführungszeit immer im Blick

Auf gängigen eingebetteten Prozessoren läuft der von CompCert erzeugte Code in der Regel doppelt so schnell wie unoptimierter GCC-Code, und nur 20 % langsamer als GCC-Code auf Optimierungs­stufe 3. Details zu den benutzten Benchmarks sind auf Anfrage erhältlich.

Chart of CompCert vs. GCC execution times for 23 benchmarks
Ausführungszeiten von 23 Benchmark-Programmen, kompiliert mit ■ gcc -O0, ■ CompCert, ■ gcc -O1 und ■ gcc -O2

Mit CompCert können wir die Ausführungszeit unserer Flugsteuerungsalgorithmen erheblich reduzieren. Die gewonnene Zeit kann für zusätzliche Funktionalität genutzt werden.“

TU München, Institut für Flugsystemdynamik

Target-Prozessoren

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

Akademische Version

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. Quellcode und Dokumentation (inklusive der Compiler­beweise) stehen auf INRIAs Seite zum Download bereit. Der Quellcode ist auch über GitHub erhältlich.

Beachten Sie, daß akademische und kommerzielle Versionen unterschiedlich numeriert werden.

Kommerzielle Version

AbsInt bietet Lizenzen und Kundenbetreuung für kommerzielle Benutzer an und trägt aktiv zur Weiter­entwicklung des Tools bei. Um CompCert kostenlos zu testen, drucken Sie das PDF-Lizenz­formular aus und senden oder faxen Sie es ausgefüllt an uns zurück.