Die formale Verifikation von Software gilt als eine der fortschrittlichsten Methoden, um Programme auf Korrektheit zu überprüfen und sicherzustellen, dass sie den spezifizierten Anforderungen entsprechen. Besonders im sicherheitskritischen Bereich von Betriebssystemen wie Mikro-Kernels gewinnt die formale Verifikation zunehmend an Bedeutung. Doch trotz des hohen technischen Anspruchs und der wissenschaftlichen Strenge, die diese Methode erfordert, sehen wir immer wieder Diskussionen über die vermeintliche Effizienz und den Vergleich von Verifikationsarbeiten, die auf irreführenden Kennzahlen beruhen – sogenannten "Benchmarking Crimes". Diese führen zu Verwirrung und falschen Erwartungen in der Fachwelt und behindern den Fortschritt. Ein verbreitetes Fehlurteil bezieht sich auf das Verhältnis von Beweisgröße zu Codegröße, auch bekannt als "Proof-to-Code Ratio".
Einige wissenschaftliche Veröffentlichungen stellen beeindruckende Zahlen vor, die suggerieren, dass neuere Projekte mit automatisierter Theorembeweisführung (ATP) den Aufwand der manuellen Theorembeweisführung (ITP) deutlich senken konnten, teilweise mit Faktoren von 3 bis 4 im Verhältnis der Linien Beweis zu Linien Code. Auf den ersten Blick wirkt das wie ein enormer Erfolg in Richtung Effizienzsteigerung und Automatisierung. Doch bei genauerer Betrachtung erweist sich diese einfache Kennzahl als irreführend und letztlich fast bedeutungslos. Das Hauptproblem mit dem Proof-to-Code-Ratio liegt darin, dass es die Komplexität der Spezifikation ignoriert. Ein Beweis ist nicht einfach eine mechanische Anlage an extra Code, sondern hängt maßgeblich davon ab, was genau spezifiziert wird.
Der Umfang und die Genauigkeit der Spezifikation bilden die Grundlage dafür, was überhaupt bewiesen werden muss. Um das deutlich zu machen, kann man das Beispiel einer Sortierfunktion betrachten, die eine Liste von Ganzzahlen in aufsteigender Reihenfolge ausgibt. Die Korrektheit einer solchen Funktion lässt sich nicht allein durch Aussagen über die Länge der Liste oder die Eigenschaft, dass sie sortiert ist, definieren. Erst eine vollständige Spezifikation, die etwa die Multiplikität der Elemente oder die Gleichheit der Elemente zwischen Eingabe und Ausgabe berücksichtigt, stellt eine korrekte Anforderung dar. Dabei zeigt sich schnell, dass eine sehr einfache Spezifikation weniger Aufwand beim Beweis benötigt als eine vollständige mit all ihren Nebenbedingungen.
Daraus folgt, dass Vergleiche von Proof-to-Code-Ratios zwischen unterschiedlichen Projekten, ohne Berücksichtigung der Spezifikationsqualität und Komplexität, wenig aussagekräftig sind – es wird bloß Äpfel mit Birnen verglichen. Tatsächlich zeigen Daten aus einer Analyse verschiedener systemnaher Projekte, dass die Spezifikationsgröße stark variiert und deutlich größere Auswirkungen auf die Gesamtkosten der Verifikation hat als die bloße Codegröße. Das belegt ein Vergleich von Systemen wie seL4, CertiKOS, SeKVM und einigen neueren ATP-basierten Ansätzen. Während der Codeumfang unterschiedlich sein kann, divergieren die Spezifikationsgrößen noch viel stärker, was sich in unterschiedlichen Proof-Größen widerspiegelt. Eine weitere wichtige Erkenntnis stammt aus Forschungsergebnissen, die aufzeigen, dass die Beweisgröße nicht linear mit der Spezifikationsgröße wächst, sondern quadratisch.
Das bedeutet: Verdoppelt man die Spezifikationsgröße, vervierfacht sich ungefähr der Aufwand für den Beweis. Diese Tatsache relativiert stark die Aussagekraft einfacher Verhältnisse und Kennzahlen wie Proof-to-Code oder sogar Proof-to-Spec. Das Verständnis dieser skalierenden Komplexität ist essenziell, wenn man die Realitäten der formalen Verifikation erfassen möchte. Das Argument für Modularität als Weg zur Beherrschung dieser Komplexität ist bekannt: Wenn man ein großes System in kleinere, weitgehend unabhängige Module zerlegt, sollte sich die Verifikationskomplexität reduzieren lassen. Formal ausgedrückt sinkt durch Aufteilung in k Module mit jeweils geringerer Spezifikationsgröße die Gesamtverifikation ungefähr proportional zu 1/k, anstatt gleichbleibend oder sogar steigend zu sein.
Allerdings trifft dieses Ideal gerade im Kontext hochintegrierter, komplexer Systeme wie dem seL4 Mikro-Kernel kaum zu. SeL4 zeichnet sich gerade durch ein stark verzahntes Design aus, bei dem viele Systemkomponenten global miteinander verbunden sind. Gerade das macht es besonders schwierig, hier wirklich sauber und ohne großen Mehraufwand zu modularisieren oder einzelne Invarianten isoliert zu beweisen. Die Komplexität der globalen Invarianten ist entscheidend für die hohe Beweislast des seL4-Projekts, und eine einfache Zerlegung in kleinere Teile ist kaum möglich, ohne Kompromisse bei der Korrektheit oder Performance einzugehen. Darüber hinaus zeigen Vergleiche zwischen interaktiver und automatischer Theorembeweisführung, dass automatisierte Ansätze grundsätzlich weniger Beweisaufwand benötigen – zumindest soweit sie eingesetzt werden können.
Sie sind jedoch aktuell noch limitiert in der Art und Komplexität der Spezifikationen, die sie feingranular und vollständig bearbeiten können. Manche neuere ATP-gestützte Projekte präsentieren daher wesentlich geringere Proof-to-Code-Ratios, doch muss man sich stets vor Augen halten, dass sich die Komplexität der zugrundeliegenden Spezifikation oftmals stark von bewährten komplexen Systemen wie seL4 unterscheidet. Diese Limitation spiegelt sich auch darin wider, dass Projekte, die zwar technisch einfacher sind und dennoch einen ähnlichen Grad der formalen Verifikation anstreben wollen, häufig kräftige Vereinfachungen im Systemmodell oder der Funktionalität machen müssen. Das führt zwar zu geringeren Proof-Aufwänden, aber auf Kosten der Realitätsnähe und des praktischen Nutzens des verifizierten Systems. In Summe führt der Rückgriff auf einfache „Benchmarking“-Kennzahlen wie Proof-to-Code-Ratios oft zu falschen Schlüssen und verzerrten Vorstellungen davon, wie aufwendig und komplex der Prozess der formalen Verifikation in der Praxis wirklich ist.
Diese sogenannten „Benchmarking Crimes“ sollten von der Community vermieden werden – stattdessen sollte die Diskussion über Aufwand und Effizienz differenzierter und auf valide Maße wie Spezifikationsgröße, Komplexität der Invarianten und Art des Beweises fokussiert werden. Verifikation ist ein tiefgreifendes, multidimensionales Unterfangen, dessen Aufwand sich nicht einfach in bruchstückhafte Kennzahlen pressen lässt. Die steigende Komplexität von Systemen verlangt gleichzeitig auch wachsendes Verständnis für die zugrundeliegenden Faktoren, die Einfluss auf Aufwand und Skalierbarkeit nehmen. Ein bislang eher vernachlässigter Aspekt ist dabei der Grad der Modularisierung und Vernetzung der Systemkomponenten – hier bieten sich Ansatzpunkte für zukünftige Forschung und verbesserte Methoden. Das Fazit lautet: Die formale Verifikation von Betriebssystemen bleibt eine anspruchsvolle Herausforderung, die sich weder mit einfachen Kenngrößen noch schnellen Vergleichen zufriedenstellen lässt.
Ein fundiertes Verständnis der zu verifizierenden Spezifikation und deren Komplexität, die Art der eingesetzten Werkzeuge sowie die systemarchitektonischen Gegebenheiten sind unerlässlich, um realistische Einschätzungen und Fortschritte zu erzielen. Das Ende der beeindruckenden „Proof-to-Code“-Mythenism lies in der Erkenntnis, dass nur umfassende Transparenz und differenzierte Kenngrößen eine belastbare Basis für neue Standards, bessere Vergleichbarkeit und letztlich effizientere Verifikation bilden können.
