Begriff
CBMC (C Bounded Model Checker)
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Frama-C analysiert Intervalle.
CBMC geht einen anderen Weg: Es simuliert den Code symbolisch.
Es rollt Schleifen auf ("Tu dies max 10 mal").
Es wandelt den C-Code in eine gigantische boolesche Formel um (SAT).
x = y + 2 wird zu Logik-Gattern.
Dann fragt es einen SAT-Solver: "Gibt es Inputs, die assert(x > 0) verletzen?"
Wenn ja, gibt es dir den exakten Trace (Gegenbeispiel).
"Wenn Input A=5 und B=-1, dann Crash in Zeile 42".
Extrem präzise für Low-Level Bugs (Buffer Overflows).
Merksatz: Ein Bounded Model Checker für C und C++, der Programme und Assertions in logische Formeln übersetzt und mittels SAT/SMT-Solvern nach Fehlern sucht (bis zu einer begrenzten Schleifentiefe).
Kommandozeile: cbmc verkehrsampel.c.
Es prüft Arrays, Pointer-Arithmetik und sogar Concurrency (Race Conditions).
Amazon FreeRTOS (IoT-Betriebssystem) nutzt CBMC, um zu beweisen, dass die Memory-Management-Funktionen sicher sind.
1. Bounded
Das "B" in CBMC.
Da Schleifen unendlich sein können (Halting Problem!), prüft CBMC nur bis Tiefe $k$ (z. B. 100).
--unwind 100.
Wenn der Bug erst nach 101 Iterationen kommt, findet CBMC ihn nicht.
Das ist der Kompromiss: Vollautomatisch und sau-schnell, aber nicht "vollständig" für unendliche Läufe (anders als Frama-C).
2. Bit-Precise
CBMC versteht Bits.
Es weiß, dass int 32-bit ist und überlaufen kann (INT_MAX + 1).
Viele formale Methoden ignorieren das (rechnen mit idealen Zahlen). CBMC findet den Overflow.
1. SAT-Encoding: Von C zu Bit-Logik
Wie verwandelt CBMC Code in Mathe?
Jede Zuweisung x = x + 1 wird umgewandelt in eine neue logische Variable $x_1 = x_0 + 1$. Dies nennt man Static Single Assignment (SSA) Form.
Der gesamte Programmfluss wird zu einer einzigen, gigantischen booleschen Gleichung verknüpft. Kontrollstrukturen (if-then-else) werden als Multiplexer-Logik abgebildet.
Am Ende erhält man eine Formel mit Millionen von Variablen. Da moderne SAT-Solver (wie Z3 oder CaDiCaL) heute extrem effizient sind, kann CBMC Probleme lösen, die vor 10 Jahren noch unberechenbar schienen.
2. Loop Unwinding & Completeness Threshold
Das größte Problem ist das Unwinding. Wenn du eine Schleife hast: while (read()) { ... }, weiß CBMC nicht, wie oft sie läuft.
Man gibt ein Limit an (--unwind 10).
CBMC fügt am Ende eine Unwinding Assertion ein. Das ist ein Check, der prüft: "Wäre die Schleife eigentlich häufiger gelaufen?".
Wenn ja, sagt CBMC: "Beweis unvollständig!". Damit verhindert CBMC, dass man ein falsches Sicherheitsgefühl bekommt. Man kann so lange "hoch-unwinden", bis die Assertion hält. Dann hat man — für Programme mit festen Grenzen — einen vollständigen Beweis der Korrektheit erbracht.
3. Java & Memory Model Checks
Obwohl für C berühmt, unterstützt CBMC auch Java (JBMC). Besonders interessant: CBMC kann das Weak Memory Model analysieren. Auf modernen CPUs (ARM/x86) werden Instruktionen oft umgeordnet. Ein Programm, das auf einem Kern funktioniert, kann auf zwei Kernen crashen, weil die Cache-Synchronisation fehlt. CBMC kann diese Umordnungen symbolisch simulieren und so subtile Concurrency-Bugs finden, die bei normalen Tests (Heisenbugs) niemals auftreten würden, aber in Produktion unter Volllast zum Systemabsturz führen.
Quick-Check
CBMC vs Frama-C?
CBMC: Findet Bugs schnell (Bug Hunting). Gut für CI/CD. Frama-C: Beweist Korrektheit (Safety). Gut für Zertifizierung.Kann es C++?
Ja, aber C++ ist ein Biest. Die Unterstützung ist komplexer.Daniel Kroening?
Prof in Oxford (und dann Amazon). Einer der Päpste des Model Checkings.