Softwaretest oder formale Verifikation – warum der mathematische Beweis entscheidend ist

In diesem Auszug aus Elektor Engineering Insights Nr. 54 habe ich Quentin Ochem von AdaCore die offensichtliche – aber lästige – Frage gestellt: Warum können wir nicht einfach für alles Softwaretests machen und damit fertig sein?

Wie Quentin betont, würde selbst eine winzige Funktion mit zwei Ganzzahlen eine astronomische Anzahl von Testfällen erfordern, um jede Möglichkeit abzudecken. Sie würden bis zum Hitzetod des Universums testen und trotzdem etwas übersehen. Abdeckungsmetriken, Fuzzing, Grenzwertanalysen – sie helfen alle, aber keiner kann die Korrektheit beweisen.
 

Formale Verifikation hingegen kann das tatsächlich. Mit SPARK können Sie mathematisch beweisen, dass Ihr Code in 100 % der Fälle das tut, was die Spezifikation verlangt. Dieses Maß an Sicherheit ist im Bereich Sicherheit vielleicht übertrieben, wo „neun Neunen“ Zuverlässigkeit – also 99,9999999 % – je nach Kosten ausreichend sein kann. Aber bei der Sicherheit brauchen Angreifer nur eine einzige Schwachstelle in zehn Millionen Zeilen Code, daher schlägt der Beweis immer die Wahrscheinlichkeit.

Quentin hat auch überlegt, dass KI bei der Party mitmacht – nicht um statische Analysatoren zu ersetzen, sondern um sie mit neuen Möglichkeiten zur Fehlersuche und vielleicht sogar mit Vorschlägen für Korrekturen zu unterstützen. Ich habe ihm gesagt, dass ich es glaube, wenn meine IDE aufhört, mich wegen fehlender Semikolons zu nerven.

Sagen Sie Ihre Meinung: Softwaretests vs. Formale Verifikation

Formale Verifikation mag wie akademischer Overkill klingen, aber Quentins Punkt ist klar: Wenn Angreifer nur einen Fehler finden müssen, stehen die Chancen gegen Sie, wenn Sie sich allein auf Tests verlassen. Werkzeuge wie SPARK verschieben das Argument von Wahrscheinlichkeit zu Sicherheit – und das wirft Fragen für alle auf, die Code schreiben – von Embedded-Entwicklern bis zu Software-Teams, die ständig unter Druck stehen, zu liefern. Mich interessiert Ihre Meinung: Ist der Beweis die Zukunft oder begnügen sich die meisten von uns weiterhin mit „genug getestet“? Teilen Sie Ihre Gedanken in den Kommentaren.