Warum Software Bugs hat: Der mathematische Beweis, dass perfekte Verifikation unmöglich ist

Softwarefehler sind allgegenwärtig. Sie bringen Apps zum Absturz, korrumpieren Daten und töten gelegentlich Menschen. Ein Bericht des Consortium for Information and Software Quality von 2022 schätzte die Kosten mangelhafter Softwarequalität in den USA auf 2,41 Billionen Dollar. Kein Tippfehler. Billionen, mit einem B.

Die naheliegende Frage lautet: Warum baut man nicht einfach bessere Werkzeuge, die Fehler erkennen, bevor Software ausgeliefert wird? Die Antwort hat nichts mit Faulheit oder Budgetmangel zu tun. Sie liegt in der Mathematik. Drei Ergebnisse der Logik des 20. Jahrhunderts beweisen, dass Softwareverifikation unmöglich zu perfektionieren ist: kein Ingenieursversagen, sondern ein Grundgesetz des Universums, so unausweichlich wie die Lichtgeschwindigkeit. Kein Werkzeug, keine Technik, kein noch so großes Budget kann je garantieren, dass ein Programm fehlerfrei ist. Hier ist der Grund.

Der Traum, der starb: Hilberts Programm

1928 stellte der deutsche Mathematiker David Hilbert der Welt eine kühne Herausforderung: ein einziges mechanisches Verfahren zu finden, das für jede beliebige mathematische Aussage bestimmen kann, ob sie wahr oder falsch ist. Würde ein solches Verfahren existieren, ließe es sich auf alle Fragen der Mathematik anwenden, und damit auch auf alle Fragen darüber, ob ein Computerprogramm korrekt arbeitet, denn Programme sind mathematische Objekte.

Drei Jahre später zerstörte ein 25-jähriger österreichischer Logiker namens Kurt Gödel diesen Traum. Seine Unvollständigkeitssätze von 1931 bewiesen, dass jedes formale System, das mächtig genug ist, um grundlegende Arithmetik zu beschreiben, stets wahre Aussagen enthalten wird, die es nicht beweisen kann. Egal wie viele Regeln man hinzufügt: Es wird immer Wahrheiten geben, die durch die Maschen schlüpfen. Das System kann nicht einmal seine eigene Widerspruchsfreiheit beweisen.

Das war der erste Dominostein. Hat die Mathematik selbst blinde Flecken, erbt jedes auf ihr aufbauende Werkzeug diese blinden Flecken.

Die Unmöglichkeit der Softwareverifikation: Turing und das HalteproblemBewiesenes Ergebnis der Informatik: Kein Algorithmus kann für alle Programme bestimmen, ob sie irgendwann enden oder endlos laufen.

1936 griff Alan Turing Gödels Einsicht auf und wendete sie direkt auf die Berechnung an. Er stellte eine scheinbar einfache Frage: Kann man ein Programm schreiben, das jedes beliebige andere Programm untersucht und korrekt feststellt, ob es irgendwann anhält oder ewig weiterläuft?

Turing bewies, dass die Antwort Nein lautet. Sein Argument ist elegant. Angenommen, ein solches Programm existiert. Nennen wir es H. Man füttert H mit einem speziell konstruierten Programm, das genau das Gegenteil von dem tut, was H vorhersagt. Sagt H „dieses Programm hält an”, läuft das Programm in einer Endlosschleife. Sagt H „dieses Programm läuft ewig”, hält das Programm an. In beiden Fällen liegt H falsch. Dieser Widerspruch beweist, dass H nicht existieren kann.

Dieses Ergebnis, bekannt als Halteproblem, hat direkte Konsequenzen für die Fehlererkennung. Wenn man nicht einmal feststellen kann, ob ein Programm jemals aufhört zu laufen, kann man erst recht nicht feststellen, ob es die richtige Antwort liefert. Die grundlegendste Frage über das Verhalten von Software ist nachweislich unbeantwortbar.

Rices Theorem: der letzte Nagel im Sarg

Klingt das Halteproblem wie ein enger, konstruierter Sonderfall, so hat Henry Gordon Rice diese Ausflucht geschlossen. In einem Aufsatz von 1953, der auf seiner Doktorarbeit an der Syracuse University basiert, bewies Rice etwas weit Umfassenderes: jede nicht-triviale Frage darüber, was ein Programm tut, ist unentscheidbar.

„Nicht-trivial” hat hier eine genaue Bedeutung. Eine triviale Eigenschaft ist eine, die entweder für alle Programme gilt oder für kein einziges. Alles andere ist nicht-trivial. Wie Rices Theorem besagt, kann kein Algorithmus eine nicht-triviale Frage über das Programmverhalten für alle möglichen Programme korrekt beantworten. Gibt das Programm jemals die Zahl 42 aus? Unentscheidbar. Greift es jemals auf Speicher zu, auf den es nicht zugreifen darf? Unentscheidbar. Ist es frei von Sicherheitslücken? Unentscheidbar.

Ein Softwarezuverlässigkeitsforscher fasste die praktische Konsequenz so zusammen: „Wir können nie mit Sicherheit wissen, ob Software incident-frei sein wird. Es ist möglich, aber wir können es nie beweisen.”

Wenn Bugs töten: die realen Kosten

Das sind keine abstrakten Bedenken. Die Strahlentherapiemaschine Therac-25 tötete zwischen 1985 und 1987 mindestens drei Patienten aufgrund von Race Conditions in ihrer Software. Frühere Modelle hatten Hardware-Verriegelungen, die Überdosierungen physisch verhinderten, doch der Therac-25 ersetzte sie durch reine Softwareprüfungen. Die Software versagte. Patienten erhielten Strahlendosen, die hundertfach über dem Vorgesehenen lagen.

1996 wich der Jungfernflug der Rakete Ariane 5 37 Sekunden nach dem Start vom Kurs ab und zerstörte sich selbst. Die Ursache: Eine 64-Bit-Gleitkommazahl wurde in einen 16-Bit-Integer umgewandelt, und der Wert lief über. Der Code war von der Ariane 4 übernommen worden, bei der die Werte kleiner waren. Niemand hatte ihn gegen Ariane 5s tatsächliche Flugbahn getestet. Der Schaden belief sich auf über 370 Millionen Dollar.

Eine vom NIST in Auftrag gegebene Studie aus dem Jahr 2002 ergab, dass Softwarefehler die US-Wirtschaft jährlich 59,5 Milliarden Dollar kosten. Bis 2022 war diese Zahl auf 2,41 Billionen Dollar angewachsen. Das NIST stellte fest: „Softwareentwickler wenden bereits rund 80 Prozent der Entwicklungskosten für die Identifizierung und Behebung von Fehlern auf, und dennoch werden kaum Produkte irgendeines anderen Typs mit einem so hohen Fehlerniveau ausgeliefert wie Software.”

Was tun, wenn man es nicht beweisen kann?

Die Unmöglichkeitsergebnisse bedeuten nicht, dass alle Hoffnung verloren ist. Sie bedeuten, dass wir ehrlich sein müssen, was „getestet” und „verifiziert” wirklich heißen. Mehrere Strategien funktionieren innerhalb der mathematischen Grenzen:

• Typsysteme fangen bestimmte Fehlerkategorien ab, indem sie einschränken, was Programme ausdrücken können. Sprachen wie Rust verhindern ganze Klassen von Speicherfehlern zur Kompilierzeit. Das funktioniert, weil die Typprüfung die Syntax des Programms untersucht, nicht sein Verhalten, und damit Rices Theorem umgeht.
• Testen findet Fehler, kann aber niemals ihre Abwesenheit beweisen. Wie der Informatiker Edsger Dijkstra feststellte, können Tests die Anwesenheit von Fehlern zeigen, niemals ihre Abwesenheit.
• Model Checking, das Clarke, Emerson und Sifakis den Turing Award 2007 einbrachte, verifiziert Eigenschaften endlicher Zustandssysteme erschöpfend. Model Checker haben Systeme mit Zustandsräumen von 10¹²⁰ analysiert, weit mehr Konfigurationen als Atome im beobachtbaren Universum. Sie funktionieren jedoch nur bei Systemen mit begrenztem Zustandsraum, nicht bei beliebigen Programmen.
• Formale Beweisassistenten wie Coq und Lean ermöglichen es Programmierern, mathematische Beweise für die Korrektheit ihres Codes zu schreiben. Das verlagert die Last: Statt ein beliebiges Programm automatisch zu verifizieren, muss der Programmierer den Beweis selbst liefern. Es funktioniert, ist aber aufwendig und auf kritische Systeme beschränkt.

Jeder dieser Ansätze tauscht Allgemeinheit gegen Stärke. Keiner widerspricht Rices Theorem. Alle akzeptieren die Unmöglichkeit und erschließen innerhalb ihrer Grenzen nutzbares Terrain.

Die unbequeme Wahrheit

Jedes Mal, wenn ein Unternehmen „Sicherheit auf militärischem Niveau” oder „fehlerfreie Software” verspricht, macht es eine Behauptung, die die Mathematik als ungarantierbar bewiesen hat. Die drei Ergebnisse von Gödel, Turing und Rice bilden eine Kette der Unmöglichkeit: Formale Systeme haben blinde Flecken, Berechnung hat unentscheidbare Fragen, und jede interessante Eigenschaft von Programmen fällt in die unentscheidbare Kategorie.

Das entschuldigt keine schlampige Ingenieursarbeit. Die Tode durch den Therac-25 wären mit grundlegenden Sicherheitspraktiken vermeidbar gewesen. Die Ariane-5-Explosion wäre mit angemessenen Tests vermeidbar gewesen. Was uns die Mathematik sagt, ist: Kein Maß an guter Ingenieursarbeit wird die Fehlerzahl jemals auf null bringen. Das Ziel ist nicht Perfektion. Es ist Resilienz: Systeme zu bauen, die sicher versagen, Fehler früh erkennen und beim Unvermeidlichen geordnet degradieren.

Softwarefehler sind kein Versagen der Softwareindustrie. Sie sind eine Konsequenz der Gesetze der Mathematik. Je früher wir das akzeptieren, desto besser können wir uns darauf vorbereiten.

Softwaredefekte kosteten die US-Wirtschaft laut dem zweijährlichen Bericht von CISQ im Jahr 2022 geschätzte 2,41 Billionen Dollar. Die Beharrlichkeit von Bugs trotz jahrzehntelanger Werkzeugverbesserungen wird oft als Ingenieursproblem gerahmt. Das ist es nicht. Es ist ein mathematisches Problem. Drei grundlegende Ergebnisse der Berechenbarkeitstheorie belegen, dass Softwareverifikation unmöglich zu perfektionieren ist: eine beweisbare, dauerhafte Beschränkung dessen, was jedes Werkzeug leisten kann.

Gödels Unvollständigkeit: Das Fundament bricht

1931 veröffentlichte Kurt Gödel zwei Theoreme, die David Hilberts Programm zerstörten, die gesamte Mathematik auf ein vollständiges, widerspruchsfreies und entscheidbares Fundament zu stellen.

Der erste Unvollständigkeitssatz besagt: Jedes widerspruchsfreie formale System F, das grundlegende Arithmetik ausdrücken kann, enthält Aussagen, die in F wahr, aber unbeweisbar sind. Der Beweis konstruiert einen Gödelsatz G_F, der effektiv sagt: „Diese Aussage ist in F nicht beweisbar.” Wäre G_F beweisbar, wäre das System widersprüchlich. Ist G_F unbeweisbar, ist das System unvollständig. Vollständigkeit und Widerspruchsfreiheit können nicht gleichzeitig bestehen.

Der zweite Satz erweitert dies: F kann seine eigene Widerspruchsfreiheit nicht beweisen. Man kann die Widerspruchsfreiheit von F in einem stärkeren System F’ beweisen, aber F’ kann wiederum seine eigene Widerspruchsfreiheit nicht beweisen, und so weiter ad infinitum.

Für die Softwareverifikation ist die Implikation strukturell. Jedes formale System, das mächtig genug ist, über Programme nachzudenken (was mindestens grundlegende Arithmetik erfordert), wird wahre Aussagen über diese Programme enthalten, die es nicht beweisen kann. Die Theoremkette setzt sich fort: Gödels Ergebnisse führten direkt zu Churchs Beweis, dass das Entscheidungsproblem unlösbar ist, und zu Turings Beweis, dass kein Algorithmus das HalteproblemBewiesenes Ergebnis der Informatik: Kein Algorithmus kann für alle Programme bestimmen, ob sie irgendwann enden oder endlos laufen. lösen kann.

Das Halteproblem: Unentscheidbarkeit der einfachsten Frage

In seinem Aufsatz von 1936 „On Computable Numbers” formalisierte Alan Turing Berechnung mittels Turingmaschinen und bewies, dass das Halteproblem unentscheidbar ist.

Der Beweis ist ein Diagonalargument. Man nehme an, es existiert eine total berechenbare Funktion h(i, x), die 1 zurückgibt, wenn Programm i bei Eingabe x hält, und 0 sonst. Man konstruiert Programm g, das bei Eingabe i die Funktion h(i, i) aufruft: Gibt h den Wert 1 zurück, läuft g ewig; gibt h 0 zurück, hält g. Nun wertet man h(g, g) aus. Sagt h, g halte, dann läuft g (Widerspruch). Sagt h, g laufe, dann hält g (Widerspruch). Folglich kann h nicht existieren.

Das ist keine Einschränkung aktueller Hardware oder Algorithmen. Es ist ein Widerspruchsbeweis, der für jedes Berechnungsmodell gilt, das einer Turingmaschine äquivalent ist, einschließlich aller allgemeinen Programmiersprachen, die es gibt.

Die praktische Konsequenz: Statische Analysewerkzeuge, die Code auf Fehler scannen, stoßen ständig an das Halteproblem. Werkzeuge wie ESLint, SonarQube oder Sicherheitsscanner erzeugen zwangsläufig falsch-positive Treffer oder übersehen echte Probleme, weil eine perfekte Analyse mathematisch unmöglich ist.

Die Unmöglichkeit der Softwareverifikation: Rices Theorem

Das Halteproblem mag eng wirken: Es betrifft nur die Terminierung. Henry Gordon Rices Verallgemeinerung von 1953 schließt jeden verbleibenden Schlupfwinkel.

Rices Theorem besagt: Sei P eine Teilmenge der natürlichen Zahlen, die (1) nicht-trivial ist (weder leer noch gleich N) und (2) extensional (wenn Programme m und n dieselbe Funktion berechnen, dann gilt: m ist genau dann in P, wenn n in P ist). Dann ist P unentscheidbar.

Vereinfacht gesagt: Jede nicht-triviale semantische Eigenschaft von Programmen ist unentscheidbar. „Semantisch” bedeutet verhaltensbezogen, nicht syntaktisch. „Nicht-trivial” bedeutet für manche Programme wahr und für andere falsch. Die folgenden Fragen sind alle unentscheidbar:

• Terminiert Programm P bei Eingabe n?
• Gibt P bei jeder Eingabe 0 zurück?
• Greift P jemals auf nicht-allokierten Speicher zu?
• Ist P äquivalent zu einer gegebenen Spezifikation Q?
• Enthält P eine Sicherheitslücke?

Ein Softwarezuverlässigkeitsingenieur stellte bei der Anwendung von Rices Theorem auf die Vorfallsanalyse fest: „Wir können nie mit Sicherheit wissen, ob Software incident-frei sein wird. Es ist möglich, aber wir können es nie beweisen.” Die Konsequenz: Jedes mentale Modell, das Software als „stabil, solange keine äußere Kraft einwirkt” betrachtet, ist mathematisch unhaltbar.

Was Rices Theorem nicht sagt

Rices Theorem verbietet nicht jede Programmanalyse. Es zielt spezifisch auf semantische Eigenschaften und allgemeine (Turing-vollständige) Sprachen. Syntaktische Eigenschaften, etwa „enthält der Quellcode eine While-Schleife”, sind entscheidbar. Typprüfung ist entscheidbar, weil sie die Struktur des Programmtexts untersucht, nicht das Laufzeitverhalten. Statische Typsysteme in Sprachen wie Haskell, Rust oder OCaml nutzen genau diese Unterscheidung: Sie erzwingen syntaktische Einschränkungen, die bestimmte Verhaltenseigenschaften (wie Speichersicherheit) garantieren, ohne den unentscheidbaren Allgemeinfall lösen zu müssen.

Fallstudien: Theorie trifft Praxis

Therac-25 (1985-1987)

Die Strahlentherapiemaschine Therac-25 verursachte zwischen 1985 und 1987 mindestens sechs Überdosierungsvorfälle, bei denen Patienten Strahlendosen erhielten, die hundertfach über der vorgesehenen Menge lagen. Die Grundursache waren Programmierfehler bei gleichzeitigen Prozessen (Race Conditions). Das Vorgängermodell, der Therac-20, hatte Hardware-Verriegelungen, die Überdosierungen physisch verhinderten. Der Therac-25 entfernte diese Verriegelungen und verließ sich vollständig auf softwarebasierte Sicherheitsprüfungen. Die wegweisende Untersuchung von Leveson und Turner aus dem Jahr 1993 führte die Ausfälle auf „generell schlechte Softwaredesign- und Entwicklungspraktiken” und übertriebenes Vertrauen in die Fähigkeit von Software zurück, Sicherheit zu gewährleisten.

Die Race Condition, die Patienten tötete, ist genau die Art von Verhaltenseigenschaft, die Rices Theorem als unentscheidbar erklärt: „Gerät dieses nebenläufige Programm jemals in einen Zustand, in dem der Strahl abgefeuert wird, ohne dass das Ziel in Position ist?” Kein allgemeiner Algorithmus kann diese Frage für beliebige Programme beantworten.

Ariane-5-Flug 501 (1996)

Am 4. Juni 1996 wich der Jungfernflug der Ariane-5-Rakete 37 Sekunden nach dem Start vom Kurs ab und zerstörte sich selbst. Das Trägheitsreferenzsystem versagte, weil ein 64-Bit-Gleitkommawert (horizontale Abweichung, BH) in einen vorzeichenbehafteten 16-Bit-Integer umgewandelt wurde und der Wert den 16-Bit-Bereich überschritt. Der Code war von der Ariane 4 übernommen worden, bei der das Flugprofil geringere Geschwindigkeitswerte erzeugte. Die Programmierer hatten nur vier von sieben kritischen Variablen gegen Überlauf geschützt, gestützt auf Annahmen, die für Ariane 4s Flugbahn galten, nicht aber für Ariane 5.

Die Lions-UntersuchungskommissionFormelles Untersuchungsverfahren der US-Marine zur Aufklärung von Vorfällen; kein Strafgericht, aber befugt, Verantwortlichkeiten festzustellen. stellte fest, dass „die Spezifikation des Trägheitsreferenzsystems und die auf Geräteebene durchgeführten Tests die Ariane-5-Flugbahndaten nicht ausdrücklich einschlossen. Folglich wurde die Neuausrichtungsfunktion nicht unter simulierten Ariane-5-Flugbedingungen getestet, und der Konstruktionsfehler wurde nicht entdeckt.” Der Schaden betrug über 370 Millionen Dollar.

Die Zustandsraumexplosion

Selbst bei endlichen Zustandssystemen, auf die Rices Theorem nicht direkt zutrifft, stößt die Verifikation auf eine praktische Mauer: die Zustandsraumexplosion. Ein System mit n binären Variablen hat 2ⁿ mögliche Zustände. Edmund Clarke, dessen Arbeiten zum Model Checking den ACM Turing Award 2007 einbrachten (geteilt mit E. Allen Emerson und Joseph Sifakis), beschrieb die zentrale Herausforderung: „Ein Computersystem führt einfache Operationen aus, aber diese Operationen können in einer schwindelerregenden Anzahl unterschiedlicher Reihenfolgen auftreten. Das macht es dem Designer unmöglich, jede mögliche Sequenz zu überblicken und ihre Konsequenzen vorherzusagen.”

Clarkes und McMillans Durchbruch war das symbolische Model Checking mittels binärer Entscheidungsdiagramme (BDDs), die mehrere Zustände kompakt kodieren. Das ermöglichte Model Checkern, Systeme mit Zustandsräumen von 10¹²⁰ zu verifizieren. Symbolisches Model Checking funktioniert jedoch nur bei endlichen Zustandssystemen. Reale Software mit unbeschränkter Rekursion, dynamischer Speicherallokation und Eingaben beliebiger Länge bleibt für vollständige Verhaltensverifikation außer Reichweite.

Arbeiten innerhalb der Grenzen

Die Unmöglichkeitsergebnisse definieren eine Obergrenze, keinen Boden. Innerhalb dieser Grenzen ist erheblicher Fortschritt möglich:

• Abstrakte Interpretation (Cousot & Cousot, 1977) berechnet korrekte Überapproximationen des Programmverhaltens. Sie kann die Abwesenheit bestimmter Fehlerklassen beweisen, auf Kosten falsch-positiver Treffer. Das ist genau der Kompromiss, den Rices Theorem erlaubt: „Es ist möglich, ein Werkzeug zu implementieren, das immer über- oder unterschätzt; in der Praxis muss man entscheiden, was das geringere Problem ist.”
• Abhängige Typsysteme (Coq, Agda, Lean, Idris) ermöglichen die Kodierung von Spezifikationen als Typen und Beweisen als Programme. Die Programme sind auf totale Funktionen beschränkt (garantiert terminierend), verzichten bewusst auf Turingvollständigkeit, um Entscheidbarkeit zurückzugewinnen.
• Model Checking verifiziert Eigenschaften der Temporallogik auf endlichen Zustandsmodellen erschöpfend. Es wird vielfach in der Hardware-Verifikation und Protokollanalyse eingesetzt.
• Bounded Model Checking und SAT/SMT-Löser verifizieren Eigenschaften bis zu einer begrenzten Tiefe und transformieren das Problem in Boolesche Erfüllbarkeit. Sie können unbeschränkte Korrektheit nicht beweisen, sind aber effektiv beim Aufspüren von Fehlern.
• Laufzeitverifikation und -überwachung prüft Eigenschaften während der Ausführung statt statisch, erkennt Verletzungen, sobald sie auftreten. Dieser Ansatz akzeptiert, dass Vordeployment-Verifikation unvollständig ist, und fügt ein Sicherheitsnetz hinzu.

Der gemeinsame Nenner: Jede wirksame Technik schränkt entweder die Sprache ein (macht sie sub-Turing), schränkt die Eigenschaft ein (prüft Syntax oder begrenztes Verhalten statt voller Semantik) oder akzeptiert Unvollständigkeit (korrekt aber nicht vollständig, oder vollständig aber nicht korrekt).

Die unbequeme Wahrheit

Eine NIST-Studie von 2002 ergab, dass Softwareentwickler bereits rund 80 % der Entwicklungskosten für das Identifizieren und Beheben von Defekten aufwendeten. Bis 2022 hatte die Gesamtkosten mangelhafter Softwarequalität in den USA 2,41 Billionen Dollar erreicht, allein die angehäufte technische Schuld betrug 1,52 Billionen.

Diese Zahlen werden nicht gegen null konvergieren. Die Kette der Unmöglichkeit von Gödel (1931) über Turing (1936) bis Rice (1953) definiert eine permanente Obergrenze für das, was Verifikation leisten kann. Jede hinreichend ausdrucksstarke Programmiersprache wird Programme erzeugen, deren Verhalten kein Werkzeug vollständig vorhersagen kann. Das Halteproblem ist nur das einfachste Beispiel; Rices Theorem stellt sicher, dass jede interessante Verhaltensfrage dasselbe Schicksal teilt.

Die ingenieurtechnische Antwort muss Resilienz sein, nicht Perfektion. Tiefenverteidigung. Redundanz. Hardware-Verriegelungen, die Software nicht vertrauen. Tests, die akzeptieren, dass sie nur Fehler finden, niemals ihre Abwesenheit beweisen können. Typsysteme, die ganze Fehlerkategorien konstruktiv verhindern. Und die ehrliche Anerkennung, dass der Traum von nachweislich korrekter Allzwecksoftware kein ungelöstes Problem ist. Es ist ein gelöstes. Die Antwort lautet: Es ist unmöglich.