Case studies

Short public write-ups of demos you can run today. Full sources live under demos/. Showcase (must-pass) vs EXPECT FAIL taxonomy: demos/README.md.

Heartbleed-class bounds (CVE-2014-0160)

Story: OpenSSL Heartbleed read attacker-controlled payload_length without ensuring the record actually contained that many bytes.

Demo: demos/heartbleed.assura

Run:

assura check demos/heartbleed.assura

What the contract encodes: preconditions on record layout and padding so response size cannot exceed the buffer (bounds safety as SMT-checkable ensures on inputs).

What is proved: when the contract is in the supported fragment and check reports Verified for those clauses, the modeled over-read is impossible under the stated requires. See What we prove.

libwebp Huffman / heap overflow class (CVE-2023-4863)

Story: a CVSS 9.8 heap buffer overflow in libwebp (WebP) affected browsers and Electron apps.

Demo: demos/libwebp-huffman.assura

Run:

assura check demos/libwebp-huffman.assura
# optional:
assura check demos/libwebp-huffman.assura --verbose --stats

What the contract encodes: memory regions (MEM.1), taint tracking (SEC.1), precomputed table verification (NUM.2), axiomatic definitions (CORE.4), and the related feature surface aimed at the class of bug (see file header comments). The bounds are what assura check tries to prove no input violates. Unknown markers are incomplete encoding, not a green proof. What that proof does and does not cover: WHAT-WE-PROVE.md.

What is proved: structural + SMT obligations that fire for the features actually modeled on that file. Treat Unknown limitation markers as incomplete encoding, not green proof.