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 zeigten Regehr, Yang et al. bereits 2011 auf einer Vorläufer­version von CompCert:

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

Wer setzt CompCert ein?

Das Institut für Flugsystemdynamik an der TU München, in der Entwicklung von Algorithmen zur Flugsteuerung und Navigation

MTU Friedrichshafen, zur Zertifizierung der Kontroll­software für Notstrom­aggregate nach IEC 60880 und IEC 61508-3:2010, bei gleichzeitiger Senkung der Entwicklungszeiten und -kosten

Airbus France, für diverse Projekte im Toulouse-Werk

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.

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


Die berechneten Ausführungszeiten bedeuten eine 28% geringere Prozessorauslastung beim CompCert-Code im Vergleich zum Code, der mit unserem üblichen Compiler erzeugt wurde. Der Hauptgrund dafür ist die bessere Speicherverwaltung. Die Zahlen decken sich mit unseren Erwartungen sowie mit bislang veröffentlichten Forschungsarbeiten zu CompCert.“

MTU Friedrichshafen

Target-Prozessoren

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

Unterstützte Tool-Chains

Zum Präpro­zes­sie­ren und Erzeugen von Objekt­dateien und Executables müssen ein externer C-Präprozessor, Assembler und Linker benutzt werden. CompCert ist getestet auf Kompatibilität mit:

GNU logo DiabData logo

Wir bieten ein optionales Tool namens Valex, mit dem Sie das Assemblieren und Linken nachträglich validieren können. Es vergleicht den von CompCert erzeugten abstrakten Assembler mit dem disassemblierten Executable-Code.

Jetzt kostenlos testen

Testen Sie CompCert kostenlos an Ihren eigenen Anwendungen.