Skip to content

Commit 9ed1022

Browse files
docs: consolidate the security-tooling session — reconcile ship-blocker status + log
Coherence pass banking the session's work (no code change): * CLAUDE.md ship-blocker section: note the COMPILE-TIME half of S-1/S-2/S-3 is complete (all three mode-production compile_error! fences + the closure code verify_and_lock/lockdown_ta_pool exist; S-1 fence added this session, keyed to mode-production alone so the irreversible ratchet never bricks dev chips). Scoped precisely: the fences PREVENT shipping without the hardening; they do NOT close the blockers — the bench silicon ratchet + the S-2 PQ1-HSM cert do. Fixes the prose-lags-code gap found this session. * work-todo Completion Log: one 2026-06-17 index row covering CI-reds + codehash-misdiagnosis fix, kontrol-cheatcodes isolation, Kani/Miri adoption + follow-ups, the full ProVerif+Tamarin protocol-verification track, and the S-1 build fence. Detail stays in §34 / §18b / the ship-blocker section / the proverif+tamarin READMEs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent c89c455 commit 9ed1022

2 files changed

Lines changed: 2 additions & 0 deletions

File tree

‎CLAUDE.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ No devices shipped, no funds on-chain — domain tags / parameters are still ren
3232
- **S-6 — RESOLVED 2026-05-28.** `store_objects` and `store_duress_objects` now pass `None` for the *user* UserID's admin-delete policy entry; data objects keep the admin entry (DoS-wipe path preserved). The substitution attack is structurally closed: admin can no longer delete USERID_OBJ → recreate at the same OID with a chosen PIN. Trade-off: a chip that hits 10-wrong-PIN lockout is single-use — `admin_factory_reset` wipes data but USERID_OBJ stays orphaned (locked, gates nothing). The OID range must be bumped in firmware (v6 → v7) to re-provision; documented inline + in `docs/se050-userid-pin-auth.md`. AN12413's bare `DeleteAll` APDU (`80 04 00 2A`) requires session auth against the NXP-reserved `RESERVED_ID_FACTORY_RESET = 0x7FFF0205` credential we don't hold — full-chip factory reset is therefore out-of-scope for firmware.
3333
- **S-7 — RESOLVED 2026-05-28** for sub-items a (`max_attempts=0` → `Se050Error::InvalidParam`; explicit `write_userid_unlimited` for admin/duress/E2E), b (`SW=0x6986` no longer mapped to `Ok` in `delete_object`), c (extended-Lc commands now emit 2-byte Le per ISO 7816-4), d-doc-side (status-code mappings cross-checked against AN12413 Table 15 + NXP `se05x_enums.h:80-95`). **Still open:** d-silicon — run an `iterative_wipe` against a throwaway UserID, drive `auth_attempts == max_attempts`, send VERIFY, capture actual SW from chip. Update `AuthMethodBlocked`'s mapping if the empirical SW differs from 0x6986.
3434
- S-5/S-6/S-7 corresponds to `docs/security-review-2026-05.md` §§C-7/C-8/C-9 (now marked Fixed); `docs/threat-model.md` Claim 3 provisional flag and Claim 5 updated. The bring-up state for the OPTIGA blockers (S-1/S-2/S-3) is still acceptable ONLY because no devices have shipped.
35+
- **Code/build-fence status (2026-06-17):** the COMPILE-TIME half of S-1/S-2/S-3 is complete — all three `mode-production` `compile_error!` fences are in `nsc/mod.rs` (S-3 hw-counter-required + S-2 reset-oids-forbidden pre-existing; **S-1 lock-operational-required added 2026-06-17, keyed to `mode-production` ALONE so the irreversible LcsO ratchet never fires on dev/test release-hardware builds and bricks dev chips**), and the closure CODE exists (`optiga::OptigaTrustM::{verify_and_lock, lockdown_ta_pool, lock_oid}`; `apdu` metadata builders for `Auto(F1D0)` / TA-pool-neutralize / counter). What REMAINS is bench/factory only: the irreversible LcsO ratchet + sacrificial-part validation (per `docs/production-todo.md`), and S-2's production PQ1-factory-HSM trust-anchor cert (a key-custody deliverable — the public sample cert in `reset.rs` only ships behind the now-fenced `optiga-reset-oids`). These fences PREVENT shipping without the hardening; they do NOT close the blockers — the silicon work does.
3536

3637
- **TZSC config (originally regressed #4; designed-fix landed; enforcement SILICON-VALIDATED 2026-05-20).** `secure/src/sau.rs` now wires `GTZC1_TZSC_SECCFGR{1,3}` correctly: AHB2 peripherals (USB OTG FS, AES, HASH, RNG, PKA, SAES) are governed by `GTZC1_TZSC_SECCFGR3` of the SAME controller (not GTZC2 as previously assumed — verified via the CMSIS `GTZC_CFGR3_*_Pos` constants in STM32CubeU5). Allowlist marks AES/HASH/RNG/PKA/SAES + I2C1/I2C2 as SECURE; OTG (bit 10) stays NS for the USB HID stack. **`make gtzc-enforcement-hw` PASSED on real B-U585I-IOT02A 2026-05-20:** all 7 secure-marked peripherals (I2C1/2, AES, HASH, RNG, PKA, SAES) RAZ-fault on NS access (read=0, GTZC violation IRQ fires, `hw::tzic::VIOLATION_COUNT` bumps 1 per probe; final 7/7) — so invariant #4's enforcement half is proven on silicon, not just QEMU. **USB-enumerates half also VALIDATED 2026-05-20:** with the GTZC config live (OTG NS), the device enumerates over USB-C as `1209:7051 "Generic PQSigner OS"` on a real B-U585I in ~1 s — so GTZC does not break USB. (Getting there uncovered + fixed two unrelated `init_ucpd` register bugs — CC Type-C detectors were disabled, and the dead-battery was never disabled via `PWR_UCPDR.UCPD_DBDIS`; see commit `b325dd8`. Also surfaced a test-methodology gotcha: `probe-rs reset` leaves the core halted on this setup, so USB/runtime tests must use `probe-rs run` or a power-cycle.) **So invariant #4's TZSC regression is now fully validated on silicon (both enforcement + USB-coexistence).** Only TAMP (in GTZC2) remains as a separate follow-up.
3738
- **Debug instrumentation may ship in this branch.** `debug-log` allowed on hardware, `secure_log!` in the wizard, NS pre-USB register dumps, DHCSR-gated semihosting prints in `hw::hash::init_clock`. CI must still gate production on `debug-log` / `e2e-test` / `mock-se` OFF.

‎docs/work-todo.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2365,6 +2365,7 @@ When a task above is completed, update it here with the date and a one-line summ
23652365

23662366
| Date | Item | Summary |
23672367
| --- | --- | --- |
2368+
| 2026-06-17 | Security-tooling adoption sprint: CI gate hardening, Kani/Miri, full protocol-verification track (ProVerif + Tamarin), S-1 build fence | Multi-track session executing the §34 SOTA adoption shortlist + the bench-free OPTIGA ship-blocker code. **(1) CI reds + a misdiagnosis caught:** fixed the 2 pre-existing reds — usb_hw raw-MMIO→`hw::mmio::Reg32` (`4d1d6476`) and a codehash-pin drift. The codehash "fix" was initially WRONG (re-pinned to a local 8-lib build); root-caused via a clean-room clone to a local-only `kontrol-cheatcodes` lib perturbing solc metadata (the canonical 7-`foundry.lock`-lib build is `0xf1ef…`); reverted the bad re-pin, added the real fix (CI `contracts` job now restores the exact `foundry.lock` libs — they were gitignored + not submodules, so CI never compiled), and isolated the source by gating kontrol-cheatcodes install/cleanup in `run_kontrol.sh`. CI promoted to gate both formerly-red suites (`secure-tests` + `contracts forge test`), born-green-verified. **(2) Kani + Miri adopted** (`make kani`/`make miri`): 6 verified Kani panic/overflow/OOB harnesses on the adversarial parse surface (`decode_item` used≤len, `bytes_to_u256`, `deserialize_pin_state`, ERC-20 calldata + a no-misdecode display-integrity proof, ERC-7730 IR header) + Miri 0-UB on the host-reachable unsafe incl. the secure-crate NS-pointer deref. Cap-monotonicity follow-up DEFERRED with reasoning (the extractable part is a guard-restatement; the real property is in the F-10-hardened flash RMW). **(3) Protocol-verification track COMPLETE** (`make proverif` 15 RESULTs + `make tamarin` 6 lemmas, all green; ProVerif 2.05 CLI + Tamarin 1.12/Maude 3.5.1 prebuilt, no sudo/GHC): ProVerif — dual-SE seed-unlock secrecy (Claims 1/2 + PIN-gate auth + positive control), SCP03 handshake (session-key secrecy + mutual auth + static-leak residual), OPTIGA Shielded Connection handshake, SCP03 replay no-forgery; Tamarin — three-way PIN-attempt lockstep (a partial counter reset is always caught; all-3-reset is the S-3-closed residual), SCP03 replay no-replay. Honest scope throughout (handshakes abstracted as pre-shared keys in the seed model; replay split tool-by-strength; anti-vacuity controls on every secrecy claim). **(4) S-1 ship-blocker build fence** (`832a369d`): `nsc/mod.rs` now `compile_error!`s when `mode-production` + `optiga-trust-m` lacks `optiga-lock-operational` — keyed to `mode-production` ALONE (not the stm32u585-release belt-and-braces) because the LcsO ratchet is irreversible and would brick dev chips on `make e2e-hw`/`play-hw-display`. Discovered S-2/S-3 fences already existed (prose lagged code); the compile-time half of all three blockers is now complete (closure code — `lockdown_ta_pool`/`verify_and_lock` — also already present). Remaining ship-blocker work is bench/factory only (silicon ratchet + sacrificial-part validation; S-2 PQ1-HSM cert). Detail in §34, §18b, the ship-blocker section (top), and `contracts/verification/{proverif,tamarin}/README.md`. Memories updated (`project_security_tooling_sota`, new `reference_foundry_codehash_lib_sensitivity`). |
23682369
| 2026-06-16 | Security-tooling SOTA deep-research (3-pass) + adoption guide (`docs/security-tooling-sota-2026-06.md`) + §34 | Ran a 3-pass deep-research sweep (~250 systems: AIxCC CRSes, agentic offensive, security MCP servers, LLM contract auditors, Rust FV, PQC constant-time/FV, EVM symbolic, protocol verification, embedded symbolic, SPHINCS+ SCA/FI, ZKNOX/Ledger-Donjon/Trezor peers, supply-chain) + a local read of `SPHINCS-`, `LeanLoop`, and `secure/src/crypto.rs`. **Headline (non-action):** the SPHINCS+ fault-attack literature (Genêt TCHES 2023, eShard #3, SLasH-DSA arXiv 2509.13048) proves verify-before-release is NECESSARY-BUT-INSUFFICIENT against grafting faults — only redundant recomputation + byte-compare works — and `c10_sign_verified_with_progress` ALREADY does exactly that (SIGN_A→SIGN_B→ct_eq→verify, cites the paper); CLAUDE.md was underselling it → corrected. **Differentiators confirmed:** no prior verified SLH-DSA *implementation* exists anywhere; ZKNOX (lattice-only) does zero FV; `SPHINCS-/verity` already proves the C13 Yul verifier (C10 port = the A3.1 task); Ledger Donjon broke Trezor Safe 3/5 by voltage glitch (validates the dual-SE XOR-split + S-1/S-2/S-3 urgency). Adopt-now shortlist (cargo-checkct/Kani/Miri/hevm-equiv/halmos/dudect/cargo-deny-bans/Tamarin) filed as §34; Binsec/Rel ruled NO-GO (no ARMv8-M decoder); poqeth confirms ~5–13M gas for a full-budget on-chain SPHINCS+ verify vs C10's ~115K (validates the "minus" design). Saved memory `project_security_tooling_sota`; enriched `project_sphincs_upstream_repo` + `project_leanloop`. No code/proof changes (this entry + §34 + CLAUDE.md doc-fix + memories + docs only). |
23692370
| 2026-06-16 | Animated splash-screen preview on the NV3007 LCD (`splash-test` feature + `make splash-test-hw`) | Ported the three `assets/splash-1{6,7,8}-*.standalone.html` revisions (hyperspace / horizon / nebula) — which share one identical `<canvas>` animation registry — to a no_std Rust renderer in `secure/src/ui/splash_test.rs`. Renders into a 1-bit packed **landscape** framebuffer (428×142, 7.6 KB — a full RGB565 native frame would be 119 KB vs the 192 KB secure SRAM budget) then blits via the SAME landscape→native transpose the trusted-UI text path uses (`ui::lcd` `FLIP=(true,false)` → native `(nx,ny)=(141-ly, lx)`). f32 math via a new **optional** `micromath` dep (pure-Rust no_std approximations; `num-traits` off; only compiled under `splash-test`). `main()` short-circuits into `ui::splash_test::run()` after `ui::init()` brings the panel up + SysTick starts (so `timeout::now()` is the animation clock); cycles the 3 revisions ~12 s each forever. One intentional divergence: integer-LCG PRNG (the browser's f64 multiply loses precision before masking) → star coordinates differ but field density/character match. **Verified:** clean `cargo check` for thumbv8m (zero diagnostics in the new module), non-splash builds unaffected, `WORDMARK` byte-identical to source, and a 4-agent adversarial fidelity workflow (per-animation + scaffolding/orientation reviewers, each finding independently verified) returned **0 confirmed divergences**. **On-silicon confirmed (all 3 render correctly), then an optimization pass landed for smoothness:** (1) blit rewritten from 428 per-row `set_window` calls/frame to ONE full-frame `set_window` + a single continuous chunked RAMWR stream via a new `lcd_nv3007::write_pixels_with(n, closure)` primitive (mirrors the proven `write_pixels_solid` framing; scan-order verified pixel-identical against the HW-validated `blit_glyph` multi-row fill) — makes all 3 animations SPI-bound (~24 ms/121 KB-at-40 MHz floor ⇒ ~40 fps for hyperspace/horizon); (2) nebula per-pixel `powf(n,2.2)` → 256-entry LUT and per-pixel `sqrt` for `carve` eliminated via a squared-distance branch that skips the carved-out centre AND the saturated body (`sqrt` only in the 104..172 annulus) — the dominant nebula cost; (3) per-revision avg-FPS logged for bench readout. A 2-agent workflow verified both changes behavior-preserving (`safe:true`, no bugs; one optional `get` bounds-guard applied for `set`/`get` symmetry). **On-silicon FPS readout then exposed the REAL bottleneck:** hyperspace 16 fps / horizon 6 fps / nebula ~0.8 fps (1.2 s/frame) — far worse than any blit/compute estimate, because the firmware is otherwise all-integer so **the Cortex-M33 FPU was never enabled** and the default `thumbv8m.main-none-eabi` (soft-float ABI, no FPU feature) compiled every `sin`/`cos`/`sqrt`/`powf` to soft-float emulation (~24 µs/transcendental). **Fix: build `splash-test-hw` with `-C target-feature=+fp-armv8d16sp` (the M33 FPU, soft-float ABI KEPT so the CMSE veneer / NS interface is byte-unchanged — "softfp") + `enable_fpu()` flips `CPACR` CP10/CP11 at the top of `run()` before the first VFP op.** Binary-verified: 698 hardware VFP instructions (incl. `vmla.f32` in the noise/bilinear hot loops), zero f32 soft-float in the render bodies (the only residual is `fmodf` for the float `%` in hyperspace drift — inherent, no VFP modulo exists, negligible). This is the dominant smoothness win (nebula compute ~30× faster). **Post-FPU FPS (20/17/10) + a new compute-vs-blit DWT split** (logged per-revision) then localised the remaining bottleneck precisely: blit = **constant 48.6 ms for all three** (vs `fill_screen`'s 24 ms floor for the same byte count) while compute was tiny (hyperspace 1.4 ms) — i.e. the blit was **CPU-bound on the per-pixel transpose+bit-unpack**, not SPI-bound; also bumped `micromath` + splash hot fns to `opt-level=3` / `#[optimize(speed)]`. Restructured the framebuffer to **native scan order** (`set` does the `FLIP=(true,false)` transpose once per *lit* pixel: `k = lx*FRAME_WIDTH + (141-ly)`) so the blit became a branch-light **byte-wise expand** (verified pixel-identical to the prior workflow-blessed blit by an exhaustive host program over all 60 776 pixels — perfect bijection, 0 mismatches, no OOB; binary shows 0 multiplies in the blit body). **But the next on-silicon readout showed the blit UNCHANGED at exactly 48.6 ms** — disproving the CPU-bound hypothesis. Root cause: `spi_hw::init` runs the `ui-lcd` SPI at **÷8 = 20 MHz** (chosen for the *trusted UI* because the dev board's LD2 LED on PE13=SCK shimmers at 40 MHz), and 121 552 B × 8 / 20 MHz = exactly 48.6 ms — the blit was **SPI-clock-bound**, not CPU-bound, which is why the closure work was free (hidden in the FIFO-wait shadow). **Fix: the `splash-test` build alone runs SPI at ÷4 = 40 MHz** (mutually-exclusive cfg from the 20 MHz trusted-UI default; binary-confirmed `CFG1=0x10000007`) → blit ~halves to ~24 ms. The native-layout byte-wise blit, while not the bottleneck at 20 MHz, is what keeps the polled FIFO fed at 40 MHz (the heavier old closure would have starved). Net expected: hyperspace ~38 / horizon ~30 / nebula ~14 fps. On-silicon confirmed: hyperspace **38** / horizon **30** / nebula **14** fps, blit now a constant 24.3 ms (the 40 MHz floor) — hyperspace/horizon maxed for a full-frame repaint, **nebula compute-bound at 43.8 ms**. Took the safe compute lever first: **coarsened the nebula noise grid step 4→6** (`GW/GH = div_ceil(STEP)+1` so the bilinear's +1 neighbours stay in-grid even when STEP doesn't divide LW — host-verified bounds-safe across all 60 776 pixels, 0 OOB; **2.1× fewer `noise()` calls/frame**, 1825 vs 3888; also now renders the full 142 rows vs the old 2-row bottom skip). Scoped DMA fully (GPDMA1 secure base `0x5002_0000`, SPI1_TX req 7, `CFG1.TXDMAEN` bit 15; 16-bit SPI items make `TSIZE=60776` fit one transaction; CMSIS lacks GPDMA bitfields but the SVD has them) — but at 40 MHz DMA-overlap helps ONLY nebula (hyperspace/horizon are transfer-bound), and it's a from-scratch blind GPDMA+linked-list driver needing on-silicon debug iterations, so it's deferred in favour of the safe compute lever; DMA's real payoff is a future 80 MHz "all-three-faster" push (signal-integrity risk on the LD2-on-SCK dev board). Next on-silicon readout will show how much the grid coarsening recovered (implicitly the field-vs-pixel split) before deciding further compute cuts (step→8 / octaves 3→2) vs the DMA+80 MHz project. |
23702371
| 2026-06-16 | (a) A3.1 verifier ceiling — corrected the "intractable / needs interpreted-hash engine" standing claim | Deep-research (SPHINCS- `/verity` upstream) found the standing A3.1 framing is right about *symbolic-search engines* (Halmos/KEVM fork on every base-w digit ⇒ ~8⁴³ explosion under uninterpreted SHA-256) but **incomplete about the problem**: it omitted the **deductive interpreter-refinement** path. A proof assistant does *induction on loop-iteration count* (two cases per loop) with the hash threaded through a **hash-agnostic** per-step invariant and **never unfolded** — so the digit explosion never happens, with **no** interpreted-hash engine. The upstream **demonstrates** it: `c13_refines_spec : ∀ inputs, execC13 = verifySpec` (`Proofs.lean:12158`), carrying **zero hash axioms** for Keccak; PQSigner already has a half-built `contracts/verity/` interpreter scaffold. The genuine residuals are NOT the explosion but (R1) the model↔deployed-bytecode hand-transcription (shared with upstream; diff-checkable TCB, not a wall) and (R2) SHA-256 needing a **byte-addressed** interpreter memory (the `0x02` precompile's sub-word `mstore` aliasing; the Keccak→SHA-256 bridge is otherwise mechanically portable). Wrote the authoritative analysis `contracts/verification/docs/A3_1_CLOSURE_PATH.md` (technique + scaffold + residuals + ~3-6mo closure path + what it buys: shrinks A3.1's empirical surface from "the whole verifier semantics" to "the Yul→interpreter transcription"); added dated correction pointers to `A3_1_VERIFIER_GAP.md`, `THE_CLAIM.md`, `KONTROL_SCOPING.md`, and `AXIOM_STATUS.json`. No proof-term/`.sol` changes — docs only; `theft_free` untouched. |

0 commit comments

Comments
 (0)