Am 25. Juni 2026 ging ein technischer Blogbeitrag des Ubuntu-Teams still online. Im Titel versteckten sich zwei scheinbar widersprüchliche Fakten: SQLite – die am weitesten verbreitete Datenbank der Welt – hatte einen Bug. Und dieser Bug steckte seit 2010 im Code.
Anders gesagt: Er versteckte sich 16 Jahre lang.
Sechzehn Jahre. Was bedeutet das? 2010 wurde das iPhone 4 vorgestellt, WhatsApp existierte noch nicht, Menschen tippten SMS auf Tastentelefonen. Und in diesem Jahr wurde der Bug mit einer einzigen Codezeile in SQLite eingefügt und nistete sich fortan still in jedes Smartphone, jeden Browser, jedes Betriebssystem ein. Hunderte Millionen Geräte, 16 Jahre Zeit – niemand hat ihn je entdeckt.
Am Ende fand ihn kein Mensch. Ein mathematisches Modell fand ihn.
Abbildung: Das Ubuntu-Team modellierte das Checkpoint-Verhalten von SQLite WAL in TLA+. Das Modell benötigt nur 20 Schritte, um diesen 16 Jahre verborgenen Fehler zu reproduzieren. Quelle: ubuntu.com
Zunächst eine Klärung: Was ist SQLite, und warum steckt es in Ihrem Handy?
Vorab eine Begriffsklärung: SQLite ist keine „App” – Sie finden auf Ihrem Handy kein Icon mit der Aufschrift „SQLite”. Es ist eine „Datenbank-Engine”, die darauf spezialisiert ist, auf Handys, Computern und in Browsern Daten zu speichern und zu verwalten.
Ein Beispiel: Ihre Chatverläufe in Messaging-Apps, die Kontakte in Ihrem Telefonbuch, die gespeicherten Passwörter Ihres Browsers, die lokalen Daten, die beim Benutzen von Banking-, Shopping- oder Social-Media-Apps anfallen – hinter all dem arbeitet fast immer SQLite. Es ist die meistinstallierte Datenbank der Welt, ohne jede Konkurrenz. Schätzungen zufolge laufen weltweit über eine Billion SQLite-Datenbanken im Betrieb.
Und ausgerechnet in dieser „Fundament”-Software lag 16 Jahre lang ein Bug. Allein diese Tatsache lässt einen frösteln.
Aber das wirklich Spannende an dieser Geschichte ist: wie dieser Bug gefunden wurde.
Ein Problem, das zu finden dem Menschen unmöglich ist
Sehen wir uns den Bug selbst an. SQLite hat einen Betriebsmodus namens WAL (Write-Ahead Log, zu Deutsch etwa: „Vorausschreib-Logbuch”). Vereinfacht gesagt: Wenn mehrere Programme gleichzeitig Daten lesen und schreiben, dient das WAL als „Schmierblatt”. Wer schreibt, schreibt erst aufs Schmierblatt; wer liest, wird vorerst nicht beeinträchtigt. Erst später werden die bestätigten Einträge ins offizielle Hauptbuch übertragen. Dieser Vorgang heißt „Checkpoint”.
Der Bug tritt genau dann auf, wenn dieser „Übertragungs”-Vorgang und ein neuer „Schreib”-Vorgang gleichzeitig stattfinden. Mit einem Alltagsbild erklärt:
Angenommen, Sie und ein Kollege bearbeiten gleichzeitig eine Tabelle. Der Kollege fügt im „Entwurfsbereich” neue Datensätze hinzu. Sie sind dafür zuständig, bereits bestätigte Inhalte aus dem Entwurfsbereich in die offizielle Datei zu übertragen. Sie werfen einen Blick in den Entwurfsbereich und sehen: 100 Datensätze müssen übertragen werden. Sie fangen an und übertragen 50 – da fügt der Kollege 5 neue Datensätze hinzu und setzt den internen Zähler des Entwurfsbereichs zurück. Sie machen mit den restlichen 50 weiter, aber weil der Zähler zurückgesetzt wurde, übertragen Sie in Wirklichkeit nur alte Indexnummern und lassen einige der eigentlich zu übertragenden Daten aus.
Das Ergebnis: In der offiziellen Datei fehlen einige Datensätze. Daten sind verloren.
Genau das beschreibt die SQLite-Dokumentation: eine „Race Condition” während des WAL-Checkpoints – zwei Operationen sind nicht richtig synchronisiert und kollidieren in einem extrem präzisen Zeitfenster.
Das Schlüsselwort ist „extrem präzise”. Um diesen Fehler auszulösen, muss eine ganze Kette anspruchsvoller Bedingungen gleichzeitig erfüllt sein: Der Schreibvorgang und der Checkpoint müssen exakt gleichzeitig ablaufen. Genau in dem winzigen Moment, nachdem der Checkpoint die WAL-Größe gelesen hat und bevor er mit dem Übertragen beginnt, muss ein anderer Schreibvorgang abgeschlossen werden und den WAL-Zähler zurücksetzen. Dieses Zeitfenster misst möglicherweise nur wenige Mikrosekunden.
Wenn Menschen Testfälle schreiben, um Bugs zu finden, raten sie im Grunde – sie raten, wo etwas schiefgehen könnte, und versuchen es dort wiederholt. Aber das Trigger-Fenster dieses Bugs ist so schmal, dass es jenseits jeder menschlichen Vorhersage liegt. Egal wie viele Tester Sie einsetzen, wie viele automatisierte Testskripte Sie schreiben – Sie können niemals jede mögliche Kombination von Operationsreihenfolgen abdecken. Die Zahl möglicher Kombinationen ist astronomisch.
Das ist der Grund, warum dieser Bug 16 Jahre lang unentdeckt in Hunderten Millionen Geräten schlummern konnte.
Was ist TLA+: Kein Testwerkzeug, sondern ein mathematischer Beweis
Um zu verstehen, wie das Ubuntu-Team diesen Bug fand, muss man ein Konzept begreifen: Formale Verifikation.
Der einfachste Vergleich, den ich geben kann: Herkömmliches Testen ist wie eine „Stichprobe” – Sie greifen wahllos ein paar Mal in einen Sack Reis, um zu sehen, ob Sandkörner darin sind. Formale Verifikation ist wie ein „mathematischer Beweis” – Sie können logisch herleiten, ob sich in diesem Sack Reis Sand befindet oder nicht, ohne jedes einzelne Korn umdrehen zu müssen.
TLA+ ist ein Werkzeug für formale Verifikation. Der Name steht für „Temporal Logic of Actions”, erfunden von der Informatik-Legende Leslie Lamport – demselben Mann, der auch LaTeX (das Textsatzsystem für wissenschaftliche Arbeiten) entwickelt und den Paxos-Konsensalgorithmus entworfen hat (die Grundlage praktisch aller heutigen verteilten Systeme).
Was TLA+ tut, ist schnell erklärt: Sie abstrahieren das zu prüfende Softwareverhalten in ein mathematisches Modell – Sie schreiben keinen Code, sondern beschreiben in mathematischer Sprache, „wie sich dieses System unter verschiedenen Bedingungen verändern sollte”. Dann erschöpft der Model Checker von TLA+ sämtliche möglichen Zustandskombinationen und prüft, ob die von Ihnen definierten Regeln unter allen Umständen halten.
Mit den Worten des Ubuntu-Teams: Nachdem sie das Verhaltensmodell von SQLite WAL in TLA+ erstellt hatten, fand der Model Checker „in nur 20 Schritten ein Gegenbeispiel”. Zwanzig Schritte. Sechzehn Jahre vs. 20 Schritte.
Abbildung: Statische Version des TLA+-Modells. Es zeigt, wie die Race Condition zwischen Schreib- und Checkpoint-Operation zum Datenverlust führt. Quelle: ubuntu.com
Warum menschliches Testen diesen Kampf niemals gewinnen kann
Ein tiefergehender Punkt: Warum kann eine mathematische Methode einen Bug finden, den 16 Jahre lang kein Mensch entdeckt hat? Der Grund liegt im fundamentalen Methodenunterschied.
Menschliche Testmethoden – ob manuelles Herumklicken oder automatisierte Skripte – sind im Kern „enumerativ”: Man listet Szenarien auf, von denen man glaubt, dass dort Probleme auftreten könnten, und prüft jedes Szenario. Das Problem: Der Zustandsraum eines Softwaresystems explodiert kombinatorisch. Ein System mit 100 Operationsschritten hat eine Anzahl möglicher Zustandsreihenfolgen in der Größenordnung von 100 Fakultät – eine Zahl, die die Anzahl der Atome im Universum übersteigt. Vollständige Aufzählung ist unmöglich.
Werkzeuge wie TLA+ stehen zwar theoretisch ebenfalls vor dem Problem der „Zustandsexplosion”, aber sie können etwas, was Menschen nicht können: Sie prüfen: Tritt unter allen von mir definierten Bedingungen jemals ein Problem auf?
Diesen Satz sollte man zweimal lesen.
Menschliches Testen beantwortet die Frage: „Welches Problem habe ich gesehen?” Formale Verifikation beantwortet die Frage: „Könnte es jemals ein Problem geben?”
Ersteres ist passiv, von der Vorstellungskraft abhängig und übersieht leicht Dinge. Letzteres ist aktiv, erschöpfend und übersieht keinen einzigen berechneten Zustand.
Die Ubuntu-Ingenieure waren nicht klüger als die SQLite-Entwickler – das SQLite-Team ist für extrem hohe Codequalität bekannt, seine Testabdeckung gehört zur Branchenspitze. Aber das Werkzeug ist ein anderes. Ein Lineal und ein Mikroskop sehen nicht dieselbe Dimension der Welt.
Warum der Konkurrent nicht betroffen war: ein unerwarteter Fund
Diese Geschichte hat noch eine faszinierende Nebenerzählung. Das Ubuntu-Team führte diese Verifikation überhaupt nur durch, weil es selbst ein Projekt namens Dqlite pflegt – eine auf SQLite basierende verteilte Datenbank. Sie wollten wissen: Ist dieser SQLite-Bug auch in Dqlite vorhanden?
Also erstellten sie zusätzlich ein TLA+-Modell von Dqlite. Das Ergebnis: Dqlite ist nicht betroffen.
Der Grund ist einfach: Dqlite ist an dieser Stelle „konservativer” designt als SQLite. Beim Checkpoint sperrt es sämtliche Schreiboperationen und stellt sicher, dass „Übertragen” und „Schreiben” nie gleichzeitig stattfinden. Das kostet zwar etwas Performance, vermeidet aber genau diese Race Condition.
Dqlites Design ist nicht unbedingt besser. Aber manchmal stellt sich eine konservative Entscheidung, die man vor Jahren beiläufig getroffen hat, 16 Jahre später plötzlich als richtig heraus. Die Kausalitätsketten der Softwareentwicklung sind manchmal bemerkenswert.
Der SQLite-Fix: eine einzige Codezeile
Am 5. März 2026 veröffentlichte SQLite den Bugfix. Der Fix ist denkbar einfach: Während des Checkpoints wird eine zusätzliche Prüfung eingebaut, die kontrolliert, ob der WAL in der Zwischenzeit zurückgesetzt wurde. Falls ja, beginnt der Checkpoint von vorn.
Anders gesagt: Sechzehn Jahre Risiko, gelöst durch eine einzige Codezeile.
Aber dass der Code einfach ist, heißt nicht, dass das Problem einfach war. Wo genau diese Zeile eingefügt werden muss und welche Bedingung geprüft werden muss – diesen Prozess durchzuführen, ist extrem schwierig. So schwierig, dass die weltbesten Datenbankingenieure von SQLite es 16 Jahre lang nicht gesehen haben.
Was das bedeutet: ein sich wandelnder Trend
Zwei Punkte möchte ich hervorheben.
Erstens: Der SQLite-Fall ist kein Einzelfall. Amazon, Microsoft, Oracle und andere setzen TLA+ bereits seit Jahren zur formalen Verifikation kritischer Infrastruktur ein – AWS-Kerndienste wie S3 und DynamoDB durchliefen in frühen Entwurfsphasen TLA+-Modellprüfungen. Nur spielten sich diese Fälle meist in geschlossenen Unternehmenssystemen ab, für die Öffentlichkeit unsichtbar. Dass nun ein omnipräsentes Open-Source-Projekt wie SQLite einen Bug per formaler Verifikation entdeckt, ist ein weithin sichtbares Signalereignis.
Zweitens: Die „Einstiegshürde” der formalen Verifikation sinkt. TLA+ ist kein Werkzeug für jedermann – es verlangt mathematisches Denken und die Fähigkeit zur Systemmodellierung. Aber ähnlich wie vor 20 Jahren niemand dachte, dass „automatisiertes Testen” zum Standard werden würde – und es heute selbstverständlich ist –, bewegt sich auch die formale Verifikation vom „Spezialistenwerkzeug” zum „Teamstandard”. Dass das Ubuntu-Team mit TLA+ einen Bug in der ausgereiftesten und am weitesten verbreiteten Datenbank der Branche fand, spricht für sich: Die Basissoftware, der Sie vertrauen, kann Schwachstellen enthalten, die selbst ihre Autoren nicht kennen. Und Mathematik ist der einzige zuverlässige Weg, sie zu finden.
Vor 16 Jahren testete man Software mit Intuition und Fleiß. 16 Jahre später findet ein mathematischer Beweis in 20 Schritten einen Fehler, den kein menschliches Auge je sehen konnte.
Das ist Fortschritt. Durch bessere Werkzeuge.
Referenzen: