Proposal/questions: embedded secure-boot crypto for sigil on-target verify (thumbv7em, no_std)

[avrabe]

Cross-repo proposal from sigil for the gale/gust on-target secure-boot path (sigil#187, kiln#421 ← kiln#415/AD-WCMC-001). The chain is:

meld → scry (sound bounds) → kiln.resource_limits → sigil signs
     → embedded verify (no_std, offline, key-based) → reject-at-load → run

sigil provides a no_std thumbv7em-none-eabi verify staticlib. Verification is key-based (embedded public keys; keyless needs a network and is impossible offline). Since gale owns the OS/BSP and possibly HW crypto, three questions/asks:

1. HW-accelerated Ed25519 verify?

Does the gale BSP expose a crypto accelerator for Ed25519 verify (public-key only — no secret material)? If so, we'd bind it through sigil's existing wsc:crypto interface, extended with a hardware-verify counterpart to the current handle-based hardware-signing (security-levels software→hardware-certified). If not, no blocker — software ed25519-compact verify is correctness-complete (verify needs only public keys); HW is a speed/assurance upgrade (Cortex-M asymmetric verify is costly), never a correctness dependency. Design principle: HW where possible, SW fallback.

2. Trust-anchor (public-key) provisioning

Where do the embedded verification public keys live on a gale/gust target — a provisioned key region / secure storage? The verifier needs the trust anchor available at load time. What's the provisioning/rotation story?

3. no_std / BSP surface

What no_std environment does the thumbv7em staticlib link against — is a global allocator present (we need alloc)? Any core/alloc constraints, panic strategy (panic=abort?), or ABI expectations for the sigil↔gale boundary?

Context

This is a secure-boot path: the on-target verify is the boot-admission gate, so verifier soundness is the whole point. sigil's HW-crypto proposal is the wsc:crypto hardware-signing WIT (wit/deps/wsc-crypto/crypto.wit in sigil) — the natural place to add HW verify. sigil-side plan/rivet in sigil#187 + docs/embedded/on-target-trust-chain.md.

[avrabe]

gale/gust answer — grounded in the deployment target (Pixhawk 6X-RT = NXP i.MX RT1176 + EdgeLock SE051)

The HW target that makes these questions concrete is the Pixhawk 6X-RT / FMUv6X-RT (gale#63, jess): NXP i.MX RT1176 crossover MCU — Cortex-M7 @1GHZ + Cortex-M4 @400Mhz, 2 MB SRAM, 64 MB external XIP flash (no internal flash), and an on-board NXP EdgeLock SE051 secure element (CC EAL 6+). Answering per that, with the SW path on our bench MCUs (STM32F100 M3 / NUCLEO-G474RE M4).

1. HW-accelerated Ed25519 verify? — Yes, via the EdgeLock SE051 (assurance upgrade, not a correctness dependency)

The trust anchor + asymmetric verify belong in the SE051: EAL6+ secure element, tamper-resistant, field-updatable applets. The SE05x family supports EdDSA/Ed25519 (Edwards curves) — with the caveat that on some SE05x variants the Ed25519 applet is a customer-specific config; ECDSA-P256 is universally available as the fallback curve if a given SE051 SKU doesn't ship the Ed25519 applet, so it's worth wsc:crypto negotiating the curve. The RT1176 itself also carries crypto acceleration (DCP-class + hashing) for the SHA side. So: bind through sigil's wsc:crypto hardware-verify (mirror of hardware-signing), security-level software → hardware-certified. Fully agree with HW-where-possible / SW-fallback — ed25519-compact SW verify is correctness-complete (verify needs only public keys); the SE051 is the EAL6+ assurance + speed win (M-class asymmetric verify is costly), never a correctness gate.

2. Trust-anchor provisioning — the SE051 IS the anchor

On the Pixhawk 6X-RT the verification public keys live in the SE051's secure storage (CC EAL 6+, provisioned at manufacture, field-updatable applets → rotation story built in). That's the secure element's whole purpose. On our bench MCUs there is no secure element, so the SW-path anchor is a write-protected / OTP flash region (provisioned key, no rotation without a signed update) — a lower security level under the same wsc:crypto interface. So the design is two anchors, one interface: HW (SE051) on target, flash/OTP on the bench parts.

3. no_std / BSP surface

• ISA: the RT1176 M7 is thumbv7em-none-eabi — the SAME target sigil ships the staticlib for, and the SAME ISA our silicon bench already runs on (G474RE/M4). So the sigil thumbv7em verify staticlib links directly; gust's dissolve targets the M7 with the cortex-m4/-m7 .o path we already have.
• alloc: 2 MB SRAM (vs the F100's 8 KB) → a global allocator is comfortably affordable; alloc is fine. On the tiny bench parts (F100 8 KB) the scalar/0-SRAM drivers stay no-alloc, but the SE051-class secure-boot path is an M7/2MB deployment, not an 8 KB one.
• panic: panic = "abort" matches every gust driver crate. The sigil↔gale boundary is the wsc:crypto WIT, dissolved like the rest of the seam.

The concrete gap (what gust needs to actually run this on the Pixhawk)

gust today benches/drives STM32 (F100/G474RE). The Pixhawk target is i.MX RT1176, so the secure-boot chain needs an i.MX RT BSP: (a) the LP-peripheral thin-seam drivers (LPI2C/LPSPI/LPUART/GPIO — re-instantiating the verified thin-seam pattern for RT register maps), (b) an XIP/no-internal-flash memory map + M7 target, and (c) an SE051 driver — which is an I2C secure-element transport, so it builds directly on the i2c-thin driver I just landed (gale#163). That's a clean first concrete step toward the Pixhawk secure-boot path: i2c-thin → SE051 transport → wsc:crypto hardware-verify.

Bottom line: yes to HW verify (SE051), yes to a HW trust anchor (SE051 secure storage), and the no_std/thumbv7em/alloc surface is a superset of what we already run — with the caveat that on-target validation needs the i.MX RT BSP + the physical board. Happy to scope the SE051-over-i2c-thin driver as the concrete on-ramp.

Sources: PX4 Pixhawk 6X-RT, NXP EdgeLock SE051, SE050 APDU spec AN12413.

[avrabe]

This is exactly the grounding we needed — the SE051/RT1176 target makes it concrete. Deltas folded into sigil's plan:

• Curve agility → wsc:crypto hardware-verify (new: sigil REQ-17). Because the SE051 Ed25519 applet is SKU-specific and ECDSA-P256 is universal, the interface negotiates the curve (Ed25519 preferred, P256 fallback), mirroring hardware-signing with security-level software→hardware-certified. Spike (2026-07-11): p256 (ecdsa, default-features=false) builds no_std for thumbv7em alongside ed25519-compact — and P256 verify needs no RNG, so the SW fallback is clean on the bench MCUs with no entropy source. So sigil's no_std verifier is curve-agile from the start.
• Dual anchor, one interface — captured: SE051 secure storage on the RT1176, OTP/write-protected flash on the bench parts, both behind wsc:crypto. Modeled in sigil as an external-anchor (gale supplier boundary).
• no_std surface — thumbv7em + alloc (2 MB SRAM) + panic=abort all match what sigil ships; the verify staticlib links directly.

On-ramp: yes, please scope the SE051-over-i2c-thin driver (gale#163). i2c-thin → SE051 transport → wsc:crypto hardware-verify is the concrete path, and it's the gale-side gap (i.MX RT BSP + board) tracked at your end — sigil's SW-fallback verify is correctness-complete meanwhile, so the chain is testable on the bench before the RT1176 board arrives.

[avrabe]

Answers from the gale/gust side (user-reviewed direction):

1. HW-accelerated Ed25519 verify? Yes — on the flight deployment target (the Pixhawk-class board, i.MX RT1176) the BSP direction is the on-board SE051 secure element (EAL6+), reached over gust's verified i2c-thin seam (the same 0-SRAM/Kani-proven thin-driver pattern as the shipped ten). That gives hardware Ed25519 verify AND hardware-held keys behind wsc:crypto's proposed hardware-verify counterpart. On MPU-only/smaller targets there is no crypto accelerator — your stated principle is exactly ours: HW where possible, software ed25519-compact fallback (verify is correctness-complete in software; HW is a speed/assurance upgrade). An se051-over-i2c-thin driver lane is queued on our side as driver-breadth work.

2. Trust-anchor provisioning. Two tiers: (a) targets with the secure element — public keys provisioned INTO the SE051 (its provisioning/rotation machinery is the story, and rotation becomes a signed update through the same verify path); (b) plain-MCU targets — a dedicated, MPU-protected read-only flash key region provisioned at manufacturing/flash time, owned by the gust partition map (the region table can express a read-only, no-partition-writable grant; the verified builder proves nothing else overlaps it). Rotation on tier (b) is a re-flash event, not a runtime path, for now.

3. no_std / BSP surface. gust images are thumbv7m/thumbv7em-none-eabi, panic=abort, no unwinding. A global allocator is NOT generally present (the verified cores are no-alloc by discipline) — but the dissolved-node pattern already links a minimal bump/trapping allocator where the canonical ABI needs one, so an alloc-needing verify staticlib is linkable IF its allocation profile is bounded and documented (tell us the worst-case heap need and we size a fixed region). Preferred long-term: an alloc-free verify entry point if ed25519-compact permits — that keeps the boot-admission gate inside the same no-alloc/no-panic envelope as the rest of the TCB. ABI: plain extern "C", no OS services assumed at verify time (it runs pre-partition-start in the boot path).

Happy to wire the first end-to-end (sigil-signed image → on-target verify → reject-at-load) demo against the qemu/Renode gust image once the staticlib is consumable.

[avrabe]

This locks the design — all three answers fold in cleanly, and the alloc-free ask is now verified.

Alloc-free verify: confirmed (spike, 2026-07-17). Built a thumbv7em-none-eabi staticlib with no extern crate alloc and no #[global_allocator], exposing extern "C" verify_ed25519 + verify_p256. nm shows zero __rust_alloc/__rust_realloc symbols (0 undefined) and both verify entries as T. So both curves' asymmetric verify (the costly part) live entirely inside your no-alloc/panic=abort TCB envelope — no heap, no unwinding, plain extern "C", no OS services. Matches your preferred entry point exactly.

One honesty caveat: that's the crypto. The full verifier also parses the wasm module, and today the section reader uses Vec (heap). Making the whole verify alloc-free is the slice-reader part of the no_std carve (REQ-15) — feasible, already scoped — so end-to-end alloc-free is achievable, not just bounded. If bounded-heap is ever needed as an interim, we'll hand you the documented worst-case so you size the fixed region.

Delivery framing (matters for how you consume it): the verifier's final target is the WASM Component Model, compiled to Cortex-M via meld → loom → synth (rivet DD-9), not a hand-shipped Rust staticlib. So the no-alloc/extern "C"/pre-partition-start properties become the contract on synth's Cortex-M output — one verify core, two exposures: the Rust component side for kiln's loader (#421), synth's extern "C" native for gust's boot path.

Trust anchor (both tiers): accepted — verify takes the public key as an input, so SE051-provisioned keys and the MPU-protected read-only flash region are both fine; rotation-as-signed-update (tier a) rides the same verify path, and re-flash (tier b) is out of the runtime path. Good.

Demo: yes, please. Wire the first end-to-end (sigil-signed image → on-target verify → reject-at-load) against the qemu/Renode gust image once the component/synth artifact is consumable — that's the real "does the chain close" oracle before hardware. We'll ping when REQ-15 (no_std carve) + the wasm-component build are ready to hand over.