Embedded: no_std on-target verifier + signed WCMC/size manifest for the kiln on-board interpreter trust chain

[avrabe]

Context

kiln is bounding how much memory an arbitrary wasm can consume for fixed-RAM embedded (gale/gust) — decision: pulseengine/kiln#415, AD-WCMC-001. scry (sound abstract interpretation, DO-333) computes the hard half (shadow-stack / longest-path bounds); those bounds go into kiln's kiln.resource_limits custom section.

The catch: scry runs host-side and cannot run on the embedded target, so the target can't recompute the bounds — it must trust signed ones and verify them on-target. sigil is the natural fit (embedded signatures, offline verification, already has "verify image size before signing" precedent). But two adjustments are needed:

Ask

1. A no_std sigil verifier library for on-target verification. sigil is std-only today (no #![no_std] anywhere), so sigil verify is a host CLI. The embedded interpreter (on thumbv7em-none-eabi, gale/gust) needs a no_std verify lib it can call to check a module's embedded signature offline, on the target, before admitting it. This mirrors kiln's own no_std push (kiln-async already ships a thumbv7em staticlib).

2. The WCMC / resource-limits manifest must be a SIGNED field of the attestation — not an unsigned custom section. So the size bounds (max_memory_usage, max_call_depth, shadow-stack bound, table/global sizes) are covered by the signature, and the target can trust them for reject-at-load (refuse a module whose signed bounds exceed the provisioned RAM/stack budget).

3. Key-based offline verification for the embedded profile — sigil's own recorded residual is "offline keyless verification impossible" (Sigstore/keyless needs network), so air-gapped gale/gust must verify with embedded public keys, not keyless.

Why it matters

Without on-target verification, reject-at-load would key off an unsigned size claim in the module — trivially forgeable. The whole point (moving a fixed-RAM overrun from "mid-mission trap in the field" to "integration failure on the bench") only holds if the target trusts the bound. sigil is what makes the bound trustworthy.

Coordination

Planning/coordination; kiln-side tracked in kiln#415 / AD-WCMC-001. The pipeline: meld → scry (bounds) → kiln.resource_limits → sigil signs → embedded verifies (no_std, offline, key-based) → reject-at-load → run.

[avrabe]

Clarification on the shape (important): the no_std verifier should be a library designed to be compiled INTO kiln's embedded loader, not a standalone verifier component/tool that the loader invokes.

On the target, verify-signature + check-signed-size-fits-budget + reject-at-load must be one inseparable admission step inside kiln's module-load path (the on-board interpreter's load_module). Reasons:

1. Non-bypassable — no code path can admit unverified bytes; verification isn't an optional call the loader might skip, it's fused into the load.
2. Minimal TCB — a single fused loader, not loader + separate verifier + IPC between them. This matters for the gust minimal-TCB argument (~4-fn shim); a separate verifier component grows the TCB and the attack surface.

So the concrete deliverable is a #![no_std] verify crate (thumbv7em-capable, key-based, offline) with a small embed-friendly API that kiln calls inline before instantiation — not a sigil verify binary. The host CLI stays as-is for build-time signing/verification.

[avrabe]

Planned + de-risked. sigil-side rivet plan: FEAT-12 → REQ-15 (no_std verify-core staticlib for thumbv7em, v0.10.0), REQ-16 (signed reject-at-load of kiln.resource_limits, v0.11.0), DD-8 (secure-boot verify profile: key-based Ed25519, HW-preferred/SW-fallback). Full write-up: docs/embedded/on-target-trust-chain.md.

Feasibility — better than the ask assumes (thanks to the #129 carve)

• Ask 🟢 [LOW] Add metrics for failed signature validations and signing attempts #3 (key-based verify) already exists in wsc-verify-core (signature/{multi,simple,keys}.rs) — std today, no new design.
• Ask 🟢 [LOW] Create comprehensive security model documentation for users #2 (signed bounds) — reuse kiln's ResourceLimitsSection verbatim; sigil's whole-module signature already covers it (only the sig section is stripped). Work is "require + verify + reject-at-load", not a new format.
• Ask Implement Rekor Checkpoint-Based Verification with Security Hardening #1 (no_std lib) — spike (2026-07-11): ed25519-compact + ct-codecs (default-features=false) build no_std for thumbv7em-none-eabi with public-key verify working. The dep wall is clear; remaining work is sigil's mechanical std→no_std carve (feature-gate file-IO, slice reader for io::Read, alloc collections).

Secure-boot framing + crypto

reject-at-load is the boot-admission gate; verifier soundness is the point. Crypto is HW-where-possible / SW-fallback — verify uses only public keys, so the software ed25519-compact path is correctness-complete; HW (via gale's wsc:crypto) buys speed/assurance, not correctness.

Cross-repo proposals posted

• kiln#421 — loader-integration contract (verify-before-trust; reject if sig-invalid∨section-absent∨over-budget; embed_limits-before-sign).
• gale#164 — HW Ed25519 verify? / trust-anchor provisioning / no_std BSP surface.

[avrabe]

kiln-side synced: contract confirmed on kiln#421, and landed as AD-LOADER-VERIFY-001 in kiln's rivet (fail-closed loader admission: sig-invalid ∨ section-absent ∨ over-budget; verify fused into load_module; Rust staticlib boundary; SR-45 extended to verify-before-trust). I'll add the rivet cross-links to sigil:REQ-15/REQ-16/DD-8 once they're on sigil's main. Confirmed: cargo-kiln embed-limits exists as the pre-sign step, and the loader hook (extract_resource_limits_from_binary) is ready to wire.