Heap hardening gap: gale_heap.c missing upstream 4.4 canary code

[avrabe]

Summary

Zephyr 4.4 added CONFIG_SYS_HEAP_HARDENING to lib/heap/heap.c — per-chunk canaries, poisoning on free, and three hardening tiers (BASIC/MODERATE/FULL). Our zephyr/gale_heap.c was forked from a pre-4.4 upstream and has none of it. When users enable CONFIG_GALE_KERNEL_HEAP=y, they silently lose the runtime hardening in exchange for Verus proofs.

Concrete diff

Upstream (lib/heap/heap.c):

• HEAP_CANARY_MAGIC 0x5A6B7C8D9EAFB0C1ULL / HEAP_CANARY_POISON 0xDEADBEEFDEADBEEFULL
• compute_canary() / set_chunk_canary() / verify_chunk_canary()
• SYS_HEAP_HARDENING_BASIC / _MODERATE / _FULL gates throughout

Ours (gale/zephyr/gale_heap.c): none of the above.

Why this matters

Gale's pitch is "strictly safer than upstream heap." Today that's false for users who want both formal verification AND runtime hardening — they cannot have both. That's a silent regression, not a documented tradeoff, which is worse.

Options

1. Port the hardening code into gale_heap.c. Preserves the replacement model; keeps gale's verification path. Cost: carrying more diff from upstream forever, re-porting on each Zephyr release.

2. Stop replacing heap.c. Let upstream's (hardened) heap handle allocation; expose Gale's verified model as a separate check layer callable at boundaries. Cost: architectural change to how gale composes with Zephyr; possibly removes some of gale's performance claims.

3. Document the tradeoff honestly and let users choose. Ship both, users pick runtime canaries vs formal proof (or combine them if feasible). Cost: doesn't fix the underlying gap, just makes it visible.

Recommendation

Option 2 in the long run — gale's value is the formal model, not carrying a heap fork. In the short term, Option 3 is minimum viable (a clear note in the README and in gale_overlay.conf comments).

Related

• This was discovered during the Zephyr fork rebase onto v4.4.0-rc3 (PR [DRAFT] Rebase Zephyr fork onto v4.4.0-rc3 (CI validation) #14).
• The same class of question applies to every kernel/*.c file we replace — tracked separately in a broader upstream-sync audit.

[avrabe]

Incremental progress — PR-3 of 4 from docs/research/heap-hardening-port-plan.md landed as 88238af.

State now:

• BASIC tier — done (PR-1, commit e6c0557 via PR heap: SYS_HEAP_HARDENING BASIC+MODERATE tiers #19).
• MODERATE tier free/realloc checks — done (PR-2, same commit).
• MODERATE tier free-list linkage + free_chunk_check call sites — done (PR-3, 88238af). Adds guards to free_list_remove_bidx, free_list_add_bidx, free_chunk, alloc_chunk (first-fit + best-fit), inplace_realloc GROW. Structural C-only, folds to no-ops at level=0, zero Rust/proof impact.
• FULL tier — still deferred. Requires per-chunk canary trailers (8-byte overhead), which drifts Heap::allocated_bytes in src/heap.rs:203 and needs the HP1 proof refresh.

Keeping this issue open for PR-4. The remote branch heap-hardening-draft is obsolete (already squash-merged via #19) and can be deleted.

[avrabe]

FULL tier landed in `109f815`. Completes PR-4 from `docs/research/heap-hardening-port-plan.md`.

`zephyr/gale_heap.c` +122 / −7:

• 8-byte canary trailer per chunk (`HEAP_CANARY_MAGIC = 0x5A6B7C8D9EAFB0C1`, `POISON = 0xDEADBEEFDEADBEEFULL`).
• Set on every alloc path, verify on every free/realloc/usable_size/free_chunk left-neighbor, poison on free-after-verify so double-free surfaces with a distinguished log line.
• Trailer slot reserved inside the chunk's physical footprint via `heap.h`'s `CHUNK_TRAILER_SIZE`.
• Folds to no-ops at `SYS_HEAP_HARDENING_LEVEL < 3`.

`src/heap.rs` +105 — HP9 proof layer:

• `reserved_bytes_spec = allocated_bytes + 8 * used_chunks`
• `lemma_reserved_bytes_bounded: reserved_bytes_spec() <= capacity` (discharged from the `min_chunk_size` precondition that `sys_heap_init` already enforces — no ensures clause of existing functions changed).
• `allocated_bytes` still = user-requested bytes (matches upstream's `chunk_usable_bytes`-based stats); trailer is physical overhead managed by heap.h sizing macros.

`plain/src/heap.rs` regenerated via verus-strip — also fixed the pre-existing doc-wrap divergence the strip gate was flagging.

Validation: cargo check + clippy clean; verus-strip gate PASS on heap.rs. `bazel test //:verus_test` deferred (sandbox). FV-HP-CANARY-001 added to verification.yaml.

Closing the PR-4 portion; leaving the issue open for any follow-on (e.g., the Kconfig comment block note in port plan §4, or runtime checks under the engine-bench hardened overlay).