Formal verifizierter Compiler
Der CompCert-Compiler
Fortsetzung des Artikels von Teil 1
Präprozessor, Assembler und Linker getrennt validiert
Vom formalen CompCert-Beweis nicht abgedeckt sind derzeit der Präprozessor, einige lokale Front-End-Transformationen, Assembler und Linker. Diese Übersetzungsschritte weisen keine hohe innere Komplexität auf und lassen sich gut durch Compiler Testsuites abdecken. Zusätzlich werden die Assembler- und Linkerphasen durch ein Tool zur Translation Validation, genannt Valex, geprüft, das Teil der kommerziellen CompCert-Distribution ist. Dabei wird a posteriori das Disassemblat des generierten ausführbaren Codes mit dem vom formalen Beweis abgedeckten Assemblercode verglichen und geprüft, dass Instruktionen und Daten einander entsprechen. Zudem wird die Struktur der ausführbaren Binärdatei überprüft.
Quellcode und Dokumentation des Compilers ebenso wie sämtliche Beweise können von der CompCert-Webpräsenz bei INRIA (compcert.inria.fr/download.html) heruntergeladen werden. Der aktuelle Entwicklungsstand kann auf Github (https://github.com/AbsInt/CompCert) eingesehen werden; eine versionierte Distribution ist als Quellcode-Download oder als vorcompiliertes Binary von AbsInt erhältlich. Die Verwendung von CompCert ist für Forschungszwecke kostenfrei. Kommerzielle Lizenzen mit Wartung und Gewährleistung werden von AbsInt vertrieben.
CompCert unterstützt derzeit die folgenden drei Architekturen: 32-bit-PowerPC, ARMv6 und Nachfolger sowie IA32. Experimentelle Untersuchungen anhand eines Benchmark aus unterschiedlichen Anwendungsbereichen, darunter Signalverarbeitung, Physiksimulation, 3D-Graphik, Textverarbeitung und Kryptografie zeigen, dass auf PowerPC und ARM der generierte Code doppelt so schnell ist wie GCC-Code ohne Optimierungen und 20 % langsamer als GCC4 bei Optimierungsstufe 3. Auf IA32 ist CompCert etwa 20 % langsamer als GCC4 bei Optimierungsstufe 1 [5]. CompCert lässt sich also durchaus mit einem modernen High-Performance Compiler messen; er erreicht zwar nicht ganz dieselbe Ausführungsgeschwindigkeit, ist dafür aber als korrekt bewiesen.
Zusammenfassend bietet CompCert einen bislang unerreichten Vertrauensgrad in die Korrektheit des Compilers: Zusätzlich zu der bislang üblichen testbasierten Validierung steht ein formaler Korrektheitsbeweis für alle Optimierungs- und Codeerzeugungsphasen zur Verfügung, der mathematisch exakt belegt, dass der generierte Maschinencode sich genauso verhält, wie es die Semantik des C-Quellprogramms vorgibt. Die Kosten des Aufspürens von Compiler-Fehlern und der Auslieferung des korrigierten Codes an Kunden können vermieden werden. Der Testaufwand zum Nachweis von Software-Eigenschaften auf Ebene des ausführbaren Binärcodes kann reduziert werden. Das Potenzial von Compiler-Optimierungen kann nun auch in hochsicherheitskritischen Anwendungsbereichen genutzt werden.
Literatur:
[1] Nullstone Corporation (Hrsg.): Nullstone for C. www.nullstone.com/htmls/ns-c.htm, 2007.
[2] E. Eide, E.; Regehr, J.: Volatiles are miscompiled, and what to do about it. In EMSOFT ’08, S. 255–264. ACM, 2008.
[3] Yang, X; Chen, Y; Eide, E.; Regehr, J.: Finding and understanding bugs in C compilers. In PLDI 2011, S. 283–294. ACM, 2011.
[4] McCarthy, J.; Painter, J.: Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, Band 19, S. 33–41, 1967.
[5] Leroy, X.; Blazy, S.; Kästner, D.; Schommer, B.; Pister, M.; Ferdinand, C.: CompCert – A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8. European Congress, Jan 2016, Toulouse, Frankreich. hal-01238879.
Der Autor:
Jobangebote+ passend zum Thema
| Dr. Daniel Kästner |
|---|
| studierte Informatik und Wirtschaftswissenschaften an der Universität des Saarlandes und promovierte im Jahr 2000. Er ist Mitgründer und CTO der Firma AbsInt Angewandte Informatik GmbH. Dr. Kästner war Gastdozent an der Universität des Saarlandes und Mitglied in Programmkomittees zahlreicher internationaler Konferenzen. Er ist Autor oder Koautor von über 50 Veröffentlichungen in den Bereichen funktionale Sicherheit, Validierung und Verifikation von sicherheitskritischer Software sowie Compilerbau und Programmanalysen für eingebettete Prozessoren. |
kaestner@absint.com
- Der CompCert-Compiler
- Präprozessor, Assembler und Linker getrennt validiert
Lesen Sie mehr zum Thema
Das könnte Sie auch interessieren
Security
Gehärtete Software macht IoT-Geräte sicherer
Entwicklungstools
Software-Infrastruktur für ARM-Cortex-M23 und -M33
Entwicklungstool
Schnelles Tracing für Cortex-M
Entwicklungstools
Neues Entwicklungssystem für STM32L4-Familie
Systemanalyse
Blick unter die Haube
