Formal verifizierter Compiler Der CompCert-Compiler

Der Aufwand, der betrieben wird, um sicherheitskritische Software zu schreiben, ist hinfällig, wenn der Compiler Fehler macht. Mit dem ­CompCert-C-Compiler existiert ein Tool, für das formal nachgewiesen wurde, dass der erzeugte Code mit der Semantik des Quellprogramms übereinstimmt.

Moderne Compiler sind komplexe Software-Systeme, in denen zahlreiche hochoptimierte Algorithmen zur Ausführung kommen – und die Fehler enthalten können. Studien wie [1, 2, 3] haben Fehler in allen untersuchten kommerziellen Compilern und Open-Source-Compilern aufgedeckt, darunter Abstürze und Fehlcompilierungen. Bei einer Fehlcompilierung erzeugt der Compiler aus einem korrekten Quellprogramm stillschweigend fehlerhaften Maschinencode. Zwar können solche Übersetzungsfehler beim normalen Software-Test entdeckt werden, es werden in der Regel jedoch keine systematischen Tests auf Compiler-Fehler hin durchgeführt. Treten sie im Feld auf, sind sie oft mit hohem Aufwand verbunden, da sie häufig schwer einzugrenzen und als Compiler-Fehler zu erkennen sind und darüber hinaus die betroffene Software aktualisiert werden muss.

Programmierfehler der Entwickler treten in der Regel zwar häufiger auf als Compiler-Fehler, dennoch hat die Gefahr von Fehlcompilierung bei sicherheitskritischer Software erhebliche Auswirkungen. Alle aktuellen Sicherheitsnormen, darunter DO-178B/C, ISO 26262 und IEC-61508, fordern, potenzielle Gefahrenstellen zu identifizieren und nachzuweisen, dass die Software keine relevanten Sicherheitsziele verletzt. Viele Verifikationsmaßnahmen werden auf Architektur-, Modell- oder Quellcodeebene ausgeführt. Die dort nachgewiesenen Eigenschaften gelten allerdings nicht notwendigerweise auch für den ausführbaren Maschinencode, nämlich genau dann nicht, wenn der Compiler fehlerhaften Code erzeugt. Auch vom Betriebssystem zugesicherte Eigenschaften sind unter Umständen verletzt, wenn beim Compilieren des Betriebssystems fehlerhafter Code erzeugt wurde. Fehlcompilierung ist somit ein nicht zu vernachlässigendes Risiko, das zusätzliche aufwändige Verifikationsaktivitäten erfordert, wie zum Beispiel zusätzliche Testläufe und Code Reviews auf Ebene des generierten Maschinencodes.

Ergebnis jahrelanger Forschung

Die ersten Versuche, die Korrektheit eines Compilers formal zu beweisen, stammen aus den 1960er Jahren [4]. Der CompCert-Compiler wurde über viele Jahre als Forschungsprojekt unter Federführung von Xavier Leroy (INRIA) und durch Mitwirkung zahlreicher renommierter Forscher aus der ganzen Welt entwickelt. Mit Erreichen der Marktreife ist CompCert nun seit 2015 von AbsInt als erster formal verifizierter optimierender Compiler auf dem Markt erhältlich. Ihn unterscheidet von anderen Compilern, dass durch maschinenunterstützte mathematische Beweise formal nachgewiesen wurde, dass keine Fehlcompilierung auftreten kann. Der Beweis zeigt, dass der von CompCert erzeugte ausführbare Code sich genauso verhält, wie es die Semantik des C-Quellprogramms vorgibt. Dies ermöglicht einen nie zuvor dagewesenen Vertrauensgrad in die Korrektheit des Compiler, der auch den höchsten Software-Zuverlässigkeitsanforderungen gerecht wird.

Wie andere Compiler auch, besteht CompCert aus einer Folge von Übersetzungsphasen, bei denen der C-Code schrittweise in immer elementarere Zwischendarstellungen bis hin zum Maschinencode übersetzt wird (Bild). Kernstück des Front End ist ein formal verifizierter Parser; im Back End wird eine Reihe von Codeoptimierungen durchgeführt, darunter Registerallokation, Instruktionsselektion, Eliminierung gemeinsamer Teilausdrücke, Konstantenpropagation und Redundanzentfernung. Für jede der 20 Hauptphasen im Front End und Back End wurde formal bewiesen, dass Fehlcompilierung ausgeschlossen ist; ein weiterer Beweis deckt das Zusammenspiel der Phasen ab. Die Beweise zeigen, dass die Transformation zwischen Eingabe und Ausgabe jeder Phase semantikerhaltend durchgeführt wird. Um dies zu ermöglichen, wurde für jede Quell-, Zwischen- und Zielsprache, von C bis zum Assembler-Code, eine formale Semantik definiert. Hierdurch werden alle möglichen Verhaltensweisen des Programms exakt definiert. Freiheitsgrade des Compilers, z.B. bezüglich der Auswertungsreihenfolge von Ausdrücken oder bei Laufzeitfehlern durch undefiniertes Verhalten des Quellcodes, werden hierbei gesondert berücksichtigt. Die notwendigen Beweise sind zu komplex, um sie von Hand durchzuführen. Sie wurden daher maschinenunterstützt durch Einsatz des Beweisassistenten Coq durchgeführt. Aus der Coq-Spezifikation wird nicht nur der Korrektheitsbeweis erzeugt, sondern auch die Implementierung des Compilers selbst in der funktionalen Programmiersprache CAML.