Ihre Test-Suite hat 94 % Abdeckung und null Fehler. Eine Symbolische-Ausführungs-Engine findet einen Crash in Ihrem Code in unter drei Sekunden.

Der Test ist nicht kaputt. Die Abdeckungsmetrik lügt nicht. Das Problem ist, dass Tests das Verhalten an spezifischen Punkten verifizieren. Symbolische Ausführung verifiziert das Verhalten über gesamte Regionen des Eingaberaums hinweg. Es ist egal, wie viele Beispiele Sie schreiben, wenn der Bug in der Lücke zwischen zwei von ihnen lebt.

Was symbolische Ausführung tatsächlich tut

Symbolische Ausführung ist eine Programmanalysetechnik, die Ihren Code mit symbolischen Variablen statt konkreter Werte ausführt. Ein normaler Test übergibt x = 5 an eine Funktion. Eine Symbolische-Ausführungs-Engine übergibt x = α, wobei α jede mögliche Ganzzahl repräsentiert.

Während der Code läuft, verfolgt die Engine Constraints. Wenn sie einen Branch wie if (x > 0) trifft, wählt sie keine Richtung. Sie spaltet die Ausführung auf. Ein Pfad trägt das Constraint α > 0. Der andere trägt α ≤ 0. Beide Pfade laufen unabhängig weiter.

Wenn ein Pfad eine Assertion, einen Speicherzugriff oder eine potenzielle Crash-Stelle erreicht, stellt die Engine einem SMT-Solver eine einfache Frage: „Gibt es einen Wert von α, der alle Constraints auf diesem Pfad erfüllt und gleichzeitig diese Sicherheitseigenschaft verletzt?“ Wenn der Solver ja sagt, liefert er ein konkretes Gegenbeispiel. Sie haben jetzt eine spezifische Eingabe, die einen Bug auslöst, für den Sie nie einen Test geschrieben haben.

Der Bug, den Ihre Unit-Tests nicht erkennen

Betrachten Sie eine Funktion, die Array-Grenzen validiert, bevor sie kopiert:

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

Ihre Test-Suite sieht vernünftig aus:

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

Alles grün. Aber offset und count sind size_t, vorzeichenlose Ganzzahlen. Auf einem 64-Bit-System kann offset + count auf eine kleine Zahl umlaufen, wenn beide groß sind. Wenn offset = 0xFFFFFFFFFFFFFFFF und count = 1, dann ist end = 0, was nicht größer als src_len ist. Die Grenzprüfung besteht. memcpy liest von einer ungültigen Adresse.

Kein vernünftiger Entwickler schreibt einen Testfall mit offset = 2^64 - 1. Der Eingaberaum ist unvorstellbar groß. Symbolische Ausführung muss den schlechten Input nicht erraten. Sie erkundet den Pfad, auf dem der Überlauf auftritt, und bittet den Solver, Werte zu finden, die das Constraint end ≤ src_len erfüllen, während offset + count überläuft. Der Solver liefert das Gegenbeispiel in Millisekunden.

Wie die Engine Pfade erkundet

Der Kernmechanismus ist Constraint-Sammlung und Pfad-Aufspaltung. Jede bedingte Anweisung in Ihrem Code wird zu einem Branch-Punkt. Die Engine hält ein Pfad-Constraint, eine boolesche Formel, die alle Bedingungen repräsentiert, die wahr sein müssen, damit die Ausführung den aktuellen Punkt erreicht.

An jedem Branch fragt die Engine den Solver:

  1. Ist das aktuelle Pfad-Constraint plus der True-Branch-Bedingung erfüllbar?
  2. Ist das aktuelle Pfad-Constraint plus der False-Branch-Bedingung erfüllbar?

Wenn beide erfüllbar sind, spaltet die Engine auf. Sie reiht beide Pfade zur Erkundung in die queue ein. So erreicht symbolische Ausführung exhaustive Pfadabdeckung für begrenzte Programme.

Wenn ein Pfad einen Crash, einen Out-of-Bounds-Zugriff oder eine fehlgeschlagene Assertion erreicht, bittet die Engine den Solver um eine erfüllende Belegung der symbolischen Eingaben unter dem aktuellen Pfad-Constraint. Diese Belegung ist Ihre Bug-auslösende Eingabe.

Sie können den Constraint-Solving-Schritt direkt mit Z3 sehen, dem SMT-Solver, der viele Symbolische-Ausführungs-Engines antreibt:

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Der Solver liefert konkrete Werte, die das Überlauf-Constraint erfüllen. Das ist der mathematische Kern der symbolischen Ausführung. Die Engine macht das automatisch über jeden Branch in Ihrem Programm hinweg.

Die Trade-offs, die sie davon abhalten, Ihre Test-Suite zu ersetzen

Symbolische Ausführung ist nicht umsonst. Es gibt drei Kosten, die einschränken, wo sie praktikabel ist.

Pfad-Explosion. Jede if-Anweisung verdoppelt die Anzahl der Pfade. Eine Funktion mit 20 unabhängigen Branches hat über eine Million Pfade. Die meisten Engines geben nach einem Timeout oder einem Pfad-Budget auf. Schleifen verschlimmern das. Eine Schleife, die symbolisch über einen unbegrenzten Bereich iteriert, erzeugt unendlich viele Pfade. Engines entrollen Schleifen typischerweise eine feste Anzahl von Malen und machen dann weiter.

Externer Zustand und Systemaufrufe. Symbolische Ausführung funktioniert am besten mit reinen Funktionen. Wenn Ihr Code aus einer Datei liest, einen Netzwerk-Request macht oder eine Datenbank abfragt, hat die Engine keine Ahnung, welcher Wert zurückkommt. Manche Tools modellieren gängige Bibliotheksaufrufe heuristisch. Andere verlangen, dass Sie Mock-Modelle schreiben. Das ist mühsam und fehleranfällig.

Solver-Timeouts. Die Constraint-Formeln für echten Code sind komplex. Arrays, Bitvektoren, Gleitkomma-Arithmetik und nicht-lineare Mathematik können einen SMT-Solver in exponentielle Zeit treiben. Ein Pfad, der konkret in Mikrosekunden läuft, kann symbolisch Minuten dauern. Engines lassen diese Pfade fallen und melden sie als ungelöst.

Wegen dieser Grenzen ist symbolische Ausführung ein Komplement zu Tests, kein Ersatz. Sie findet die tiefen Eckfälle. Ihre Tests verifizieren die gängigen Fälle und das Integrationsverhalten.

Drei Wege, es auf echtem Code auszuprobieren

Sie brauchen keinen Doktor, um symbolische Ausführung zu betreiben. Moderne Tools verbergen die meiste Komplexität.

Für C/C++: KLEE. KLEE ist die klassische Open-Source-Symbolische-Ausführungs-Engine, die auf LLVM aufbaut. Sie kompilieren Ihren Code zu LLVM-Bitcode mit clang -emit-llvm, dann führen Sie klee auf dem Ergebnis aus. KLEE hat schwere Bugs in GNU Coreutils, SQLite und anderen weitverbreiteten C-Codebases gefunden.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE gibt .ktest-Dateien für jeden Bug aus, den sie findet. Sie können sie mit einer kleinen Runtime abspielen, um die exakten Eingaben zu sehen.

Für Python und Binärdateien: angr. angr ist ein Python-Framework für symbolische Ausführung, Binäranalyse und Reverse Engineering. Es arbeitet auf kompilierten Binärdateien, Sie brauchen also keinen Quellcode. Sie schreiben ein Python-Skript, um symbolische Register und Speicher aufzusetzen, dann lassen Sie angr erkunden.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr ist langsamer als KLEE, aber es handhabt echte Binärdateien mit all ihren chaotischen Calling Conventions und Bibliotheksabhängigkeiten.

Für Rust: Kani. Kani ist ein Rust-spezifischer Verifier, der auf CBMC aufbaut. Sie annotieren eine Funktion mit #[kani::proof] und führen cargo kani aus. Es prüft auf arithmetische Überläufe, Out-of-Bounds-Zugriffe und Assertion-Failures mit symbolischer Ausführung unter der Haube.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kani ist der einfachste Einstieg, wenn Sie bereits im Rust-Ökosystem sind. Es integriert sich mit cargo und liefert Fehlertraces in vertrautem Format.

Häufig gestellte Fragen

Ersetzt symbolische Ausführung Fuzzing?

Nein. Fuzzing generiert zufällige Eingaben und beobachtet Crashes. Symbolische Ausführung argumentiert über Pfade und findet Eingaben, die spezifische Constraints erfüllen. Fuzzing skaliert auf große Programme und lange Läufe. Symbolische Ausführung findet tiefere Bugs in kleineren Regionen. Die beiden Techniken arbeiten gut zusammen. Tools wie Driller und QSYM kombinieren sie, indem sie Fuzzing für Abdeckung und symbolische Ausführung für schwer erreichbare Branches nutzen.

Kann symbolische Ausführung beweisen, dass mein Code keine Bugs hat?

Nur für begrenzte Programme ohne unbegrenzte Schleifen und ohne external dependencies. Für die meisten Produktivcodes kann symbolische Ausführung die Abwesenheit bestimmter Bug-Klassen bis zu einer Pfad-Tiefe beweisen. Sie kann nicht totale Korrektheit beweisen.

Wie lange dauert der Lauf?

Minuten bis Stunden für kleine Funktionen. Symbolische Ausführung ist kein CI-Speed-Dämon. Führen Sie sie auf kritischen Sicherheitsfunktionen, Parsern und Grenzprüf-Code aus. Versuchen Sie nicht, Ihr ganzes Web-Framework symbolisch auszuführen.

Fangen Sie mit einer Funktion an

Sie müssen nicht Ihre ganze Codebase symbolisch ausführen. Wählen Sie eine Funktion, bei der ein Bug wehtun würde. Ein Parser. Ein Autorisierungs-Check. Ein Buffer-Copy.

Schreiben Sie einen KLEE-Harness, ein angr-Skript oder einen Kani-Proof. Führen Sie es aus. Sehen Sie zu, wie es eine Eingabe findet, für die Sie nie einen Test geschrieben hätten. Beheben Sie den Bug. Schlafen Sie besser.

Das Ziel ist nicht, Ihre Tests zu ersetzen. Das Ziel ist, aufzuhören, so zu tun, als würden 94 % Abdeckung 94 % Sicherheit bedeuten. Symbolische Ausführung findet die Lücken. Ihre Tests werden das nie.