Bend-SSZ: Formally proving SSZ

What it is

bend-ssz is written in Bend, a language whose type checker doubles as a proof checker and which compiles to C, so the verified code is the code that actually runs. The proof architecture has four layers: a frozen, hand-audited spec transcription; the pinned type schemas; a generated implementation (packed 32-bit words, not byte lists, specifically so it differs from the spec enough that equality proofs mean something); and generated proofs, produced by untrusted generators and checked from scratch before merge.

How it works

Decode is two passes: a generated validator (offsets, lengths, padding, selectors) followed by a reader that copies out of the input buffer — nothing aliases the input. The budgeted decode entry point X_decode_checked_budget(buf, size, budget) computes X_dcost(size) = ((size>>3)+1)*K + 2^19 heap words before touching the input and refuses if it exceeds budget; K is 40 for blocks/ExecutionPayload, 7 for BeaconState, ≤7 otherwise. K itself is measured, not proved — validated empirically over 438 worst-case shapes, each decoding within at least 1.4x margin of its bound.

Preconditions / Affected

Applies to consensus clients handling SSZ decode paths (tested integration: Prysm via a C FFI, decode-only, behind a build tag). Unbounded decode (no budget applied) is the exposure condition for the memory-amplification issue below; on real network inputs the attack is already bounded (≤2^20 transactions, 10MiB message cap → ~150MiB heap, ~0.24s).

What to do

Two concrete findings worth acting on if maintaining an SSZ decoder:

• 32-bit size wraparound: lengths near 2^32 overflow in 32-bit arithmetic. Fix pattern used here: cap accepted encodings at NMAX = 2^32 - 32 bytes, make size arithmetic saturating (poison value 0xFFFFFFFF propagates through +/*), and have every encoder refuse a poisoned size rather than silently wrap.
• Decode memory amplification (DoS): a crafted message can blow up up to 28x on decode (measured: ExecutionPayload full of 1-byte transactions, 28.5-28.7x heap-per-input-byte; empty transactions, 27.4-28.0x; progressive containers with empty inner lists, 22.0x). Root cause: each variable-size element costs a box + array slot (24 bytes minimum, 86 for an empty transaction) against only a 4-byte offset on the wire. Mitigation: compute decode cost from input size before allocating, reject if over budget — i.e., adopt the budgeted-decode pattern above rather than decoding first and checking size after.

Performance tradeoffs if considering adoption: deserialize/serialize are roughly on par with Go's fastssz (median 0.8x/0.7x across 978 workloads), but hash_tree_root is ~3.9x slower (median, worst 7.6x) because it uses a pure-Bend SHA-256 instead of CPU SHA instructions — a deliberate choice for code-identity across platforms, not an oversight. Through the C FFI boundary, decode is 2-10x slower than native Go.

Caveats

The author states these are not independently reviewed and explicitly asks for scrutiny of the spec transcription. Trust still rests on: the spec transcription itself (human-read, not proof-checked), a Bend checker fork with an unmerged patch and no consistency proof (Type : Type), an unverified C compiler/runtime, and SHA-256 as an unverified premise. Four generic test types have decode proved only up to 2^29–2^31 bytes rather than full range. Performance numbers were measured on an earlier toolchain (Bend 2.0.25) on a loaded machine with spec-test-sized fixtures, not mainnet-sized state, and the author flags intent to re-run them.