The C bounded model checker: criminally underused

Original Article ↗ Hacker News Discussion ↗

Formal verification tools like CBMC, a bounded model checker for C (and backend for Amazon’s Kani for Rust), are praised for catching subtle bugs such as buffer overflows and logic errors by exhaustively exploring program paths within given bounds. Commenters debate how well these tools scale beyond small, unit-test-style code, how they compare to alternatives like Frama-C, KLEE, and sanitizers, and whether the effort they require is preferable to switching to safer languages. The conversation broadens into long‑standing problems in C—undefined behavior, missing array-length information, and weak safety guarantees—and whether language evolution or external tools are the more realistic path to safer low-level software.

Adoption and Use Cases of CBMC

  • Several commenters argue CBMC is underused and advocate bringing hardware-style formal verification into mainstream software.
  • Examples cited: verifying crypto code, AWS C libraries, FreeRTOS components, HTTP client functions, and large commercial C projects (~500K LOC).
  • Some users report finding real bugs such as buffer overflows, denial-of-service loops, and issues in parsers and networking code.

Scalability and Verification Style

  • Consensus: CBMC works best at unit or small-module level, not whole large systems.
  • Effective use requires:
    • Contract-based design: explicit pre/postconditions and assertions.
    • “Shadow” functions that replace complex callees with simplified, nondeterministic models that respect the same contract.
    • Keeping search depth shallow so each run finishes quickly.
  • Retrofitting onto legacy, poorly structured code is seen as harder than using it from the start.

Comparison with Other Tools

  • Frama-C, Coq VST, seL4’s approach: more powerful but require more expertise and don’t scale easily to everyday code.
  • KLEE: good on simple tools like GNU text/coreutils; struggles with complex structured inputs (e.g., protobufs, C++ containers).
  • Static analyzers (e.g., compiler analyzers plus annotations) can cover some buffer issues; CBMC still valued as another safety layer.
  • CBMC is also used as the backend for Kani, a Rust verification tool.

C Arrays, Bounds, and Language Design

  • Extended debate about C’s loss of array size on decay to pointers and resulting buffer bugs.
  • Proposals discussed: fat pointers/slices, non-owning sized arrays, and pointer-to-array parameters; some implemented in other languages.
  • Frustration that C standards have not adopted such features, while taking on more obscure ones (e.g., Unicode identifiers).

Undefined Behavior and Uninitialized Memory

  • CBMC models uninitialized locals as nondeterministic values, which can diverge from C’s UB semantics.
  • Some argue a verifier should treat any UB (like reading uninitialized variables) as an immediate error; others note CBMC’s current focus is “C-like” models, not exact C semantics.
  • Long subthread on UB, compiler optimizations, “friendly/boring C,” sanitizers, and OS behavior shows deep concern over UB-driven miscompilations and security bugs.
  • Agreement that CBMC should be used alongside compiler warnings and sanitizers as part of defense in depth.