CompCert ist ein formal verifizierter optimierender C-Compiler. Er ist insbesondere zum Kompilieren sicherheitskritischer Software gedacht, die den allerhöchsten Standards entsprechen muß.
Als Eingabe akzeptiert CompCert den größten Teil der C99-Spezifikation, mit einigen Einschränkungen und vielen Erweiterungen. Als Ausgabe erzeugt er Assembler-Code für ARM, PowerPC, AArch64, RISC-V 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.
Die formale Beweisführung deckt die gesamte Überführung des abstrakten Syntaxbaumes in Maschinencode ab.
Zum Präprozessieren und Erzeugen von Objektdateien und Executables müssen ein externer C-Präprozessor, Assembler, Linker und C-Bibliotheken benutzt werden. Diese nichtverifizierten Schritte sind allerdings wohlverstanden und aus der Implementierungssicht robust. Das zeigten Regehr, Yang et al. bereits 2011 auf einer Vorläuferversion 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 Entwicklungsversion von CompCert der einzige Compiler, für den Csmith keine Falschcode-Fehler findet. Dabei haben wir alles versucht und etwa sechs CPU-Jahre Rechenzeit der Aufgabe gewidmet. CompCerts offenkundige Unverwüstlichkeit ist ein starkes Argument dafür, daß innerhalb eines Beweissystems mit maschinellen Sicherheitsüberprüfungen entwickelte Compileroptimierungen dem Benutzer eindeutige Vorteile bringen.“
2022 wurde das CompCert-Entwicklerteam mit dem Software-System-Preis der ACM und dem ACM SIGPLAN Programming Languages Software Award ausgezeichnet.
Ihre Vorteile
- Der Einsatz von CompCert ist die logische Fortführung des Einsatzes formaler Verifikation auf der Quellcode-Ebene (statische Analyse, Model-Checking). Nur mit CompCert gelten alle Sicherheitseigenschaften, die Sie auf der Quellcode-Ebene nachgewiesen haben (z. B. die Abwesenheit jeglicher Laufzeitfehler), garantiert auch für den erzeugten Binärcode.
- Beim Einsatz von herkömmlichen Compilern für sicherheitskritische Anwendungen werden in der Regel alle Optimierungen komplett ausgeschaltet. Bei CompCert müssen Sie das nicht tun, da seine Optimierungen ebenfalls formal verifiziert sind. Somit können Sie die Leistung Ihrer Anwendung dramatisch steigern, den Stackverbrauch senken und die Ausführung beschleunigen.
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 Kontrollsoftware für Notstromaggregate nach IEC 60880 und IEC 61508-3:2010, bei gleichzeitiger Senkung der Entwicklungszeiten und -kosten
Airbus France, für diverse Projekte im Toulouse-Werk
Die 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 Optimierungsstufe 3.
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 herkömmlichen 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.“
Target-Prozessoren
CompCert erzeugt Maschinencode für ARM, PowerPC (32-Bit), IA32 (32-Bit-x86), AMD64 (64-Bit-x86), AArch64 und RISC-V (32- und 64-Bit).
Unterstützte Tool-Chains
Zum Präprozessieren und Erzeugen von Objektdateien und Executables müssen ein externer C-Präprozessor, Assembler und Linker benutzt werden. CompCert ist getestet auf Kompatibilität mit:
- GCC (Version 4 oder neuer)
- WindRiver Diab für PowerPC (Version 5)
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 ausprobieren
Testen Sie CompCert kostenlos an Ihren eigenen Anwendungen.
Kommerzielle Version
Akademische Version
PDF-Downloads
- Produktflyer
- Factsheet
- Valex-Factsheets: PPC, ARM