[gburd]

What

__bam_defdecompress (the default compressed-btree key/data decoder,
src/btree/bt_compress.c) read each varint's leading byte — and the magic byte
*s at offset 0 — before checking the compressed buffer was long enough:

s = compressed->data;
if (*s == CMP_INT_SPARE_VAL) ...              /* *s, no size check at all */
size = __db_decompress_count_int(s);          /* reads s[0] */
if (size > compressed->size) return (EINVAL); /* the check is AFTER the read */

A compressed btree's pages come from disk, so a corrupt or truncated compressed
item is a trust boundary (db_verify, a hostile file, DB->get over a
damaged page). A short item over-reads up to one byte past compressed->size
at each of the three varint sites; a zero-length item reads *s with no check
at all — a heap over-read on hostile input.

Fix

Bound the current offset (size, which tracks s's displacement) strictly
inside compressed->size before every __db_decompress_count_int, and require
compressed->size >= 1 before *s. The __db_decompress_int32 reads were
already covered by the following size > compressed->size check, so only the
lookahead byte and the magic byte needed guarding. One hunk; no format,
log-record, ABI or region change (region sig 0x841f4ea8 unchanged).

How it was found and proved

Found by CBMC: test/cbmc/harness_bt_decompress.c (RFC 0025 B1, on
test/cbmc-expand / #263) proves the decoder's memory safety over every bounded
input. The unmodified engine code produces a counterexample (the over-read);
the -DB1_FIXED variant — this fix — verifies.

Test (fails before, passes after)

test/db/run_bt_decompress_bounds.sh + bt_decompress_bounds.c: the compressed
item is placed flush against a PROT_NONE guard page, so the over-read faults
on any build, not only under ASan.

• master: case A (size 0) and case B (size 1) both die on SIGSEGV (the
  over-read); VERDICT ... FAIL.
• this branch: both return EINVAL; VERDICT ... PASS.

Also confirmed under ASan: master aborts with a heap-buffer-overflow READ in
__db_decompress_count_int (db_compint.c:306) ← __bam_defdecompress
(bt_compress.c:548). SKIPs cleanly on a build without --enable-compression
(the decoder is not compiled in then). MANIFEST entry + executable mode added.

LTS

lts/2026.10.7 has the identical code. Backport:
backport/2026.10.7/bt-decompress-bounds (cherry-pick -x), L1/L3/L4 gates
pass (region sig byte-identical, base FAILs / backport PASSes).

[github-actions]

Coccinelle convention checks

No new violations. ✅

Resolved since baseline (3) -- update dist/cocci/baseline.txt to lock these in.

rule_mutex_unbalanced|MUTEX_UNBALANCED|src/btree/bt_curadj.c|return (ret);
rule_mutex_unbalanced|MUTEX_UNBALANCED|src/crypto/mersenne/mt19937db.c|return (ret);
rule_mutex_unbalanced|MUTEX_UNBALANCED|src/mp/mp_register.c|return (ret);

[github-actions]

ABI diff vs v2026.10.8 (libabigail — authoritative)

abidiff exit bitmask: 0

Removed exported symbols (nm -D, _NNNN version suffix normalized)

None.

---

Advisory: libabigail/nm is the authoritative binary-ABI check; Coccinelle is complementary source-level early warning. See dist/cocci/README.md.

[gburd]

Lead review: the first commit (2e99a1f) stops the varint lookahead over-read, but not the bigger hole. The decoded prefix, suffix and data length are from disk and can be any u32. With prefix 4 and suffix 0xFFFFFFFE, prefix + suffix wraps to 2, size += suffix wraps back under compressed->size, every check passes, and memcpy copies about 4 GB, on both paths. __bamc_start_decompress also copied the first record's decoded length out of the page unchecked, so one corrupted length byte crashes a plain DB->get.

e067d65 bounds those lengths before any sum, checks the first-record length the way __bam_compress_salvage already does, and adds cases C, D (the wrap on each path) and E (a real compressed database with one byte corrupted on disk, public API only) to bt_decompress_bounds.

Dev box, Debian 12, --enable-compression --enable-diagnostic:

code	A	B	C	D	E
master	SIGSEGV	SIGSEGV	SIGSEGV	SIGSEGV	SIGSEGV
2e99a1f only	pass	pass	SIGSEGV	SIGSEGV	SIGSEGV
+ e067d65	pass	pass	pass	pass	pass

The CBMC harness missed the wrap because its varint model returned a value of at most about 2^17. It now returns any u32, and the first commit alone fails the proof (new b1-wrap arm on #263).