Skip to content

PQC P0: pin libs/mlkem v0.6.0, place it behind PQ_HYBRID=1 (link-only) - #313

Merged
JC-000 merged 7 commits into
masterfrom
feat/pqc-p0-placement
Oct 17, 2026
Merged

JC-000 merged 7 commits into
masterfrom
feat/pqc-p0-placement

Conversation

@JC-000

@JC-000 JC-000 commented Oct 17, 2026 •

Copy link
Copy Markdown
Owner

PQC P0: pin libs/mlkem v0.6.0 and place it behind PQ_HYBRID=1

Placement only; nothing in the protocol calls ML-KEM. Rebased on master 7b1ed07 (#312).

Delivery (user decision 2026-10-13): loads at $A000, boot copies to $E000

ML-KEM code+rodata LOADS in the PRG at $A000 and RUNS at $E000. The file bytes under it are CRYPTO_COLD_SHADOW's BSS zero fill, which exist anyway, so the PRG is unchanged in size, ends at $BFFF (uci) / $CFFF (comb), and test_prg_io_range stays green. No #288 relaxation.

  • cfg: ld65 cannot put a ro segment and the BSS at the same addresses of one area, so the shadow is two areas over $A000-$BFFF: CRYPTO_COLD_SHADOW (RAM view, file="", all BSS, unchanged names/addresses/symbols) and COLD_FILE (file view, file=%O zero fill, hosts the load image). Unset, the PRG is byte-identical on all seven profiles (hashes below). LIB_MLKEM_CODE/RODATA: load = COLD_FILE, run = MLKEM_CODE_RAM, align_load = $40.
  • Asserts (mlkem_link.s): image loads at the head of COLD_FILE ($A000), runs at $E000, load layout == run layout (one block copy), fits the 30-page copy, ends inside COLD_FILE (the PRG's file content), run image below the $FFFA vectors.
  • Boot copy: mlkem_boot_init (NET_CODE) is called from boot.s right after sei, before the $A000-$BFFF zeroing; an assembler assert pins that order (it compares labels; the linked test is the real guard). BASIC is already out, so $A000 reads RAM; writes to $E000 land in RAM under the KERNAL. It decides on the one-byte tail marker, not a nonzero-byte gate: flag already set -> nothing; marker at the load address -> copy; no marker but one at $E000 -> resident, flag re-armed; else REFUSE (red border, pq_mlkem_* return A=$FF C=1). 'Q' does not touch $E000 or the vectors (code is not secret; no scrub span there). The flag is not scrubbed.
  • Vectors (finding 4): $FFFA/$FFFC/$FFFE (RAM with the KERNAL out) all point at one RTI in NET_CODE, written FIRST on every path of mlkem_boot_init, so every $01=$34 window (the boot's, the scrub's, a call's) has a valid target. A RESTORE NMI returns. IRQ/BRK share the RTI, which is safe only because every call runs under sei: the RTI acknowledges nothing, so the sei is what prevents a level-triggered IRQ livelock.
  • Entry (finding 1): pq_mlkem_call (A/X = entry) is the only way in: php/sei, $01=$34, mlkem_arith_init, the entry, restore. test_mlkem_placement.py fails on any other reference to a library entry. The mlkem_arg_* block lives in the same window X25519 rebuilds: fill it after the last X25519/fp_mul.

Review round (adversary #313): what changed

  • S1 _prg_load.py allows non-zero bytes ONLY in [__LIB_MLKEM_CODE_LOAD__, tail marker + 1) from build/labels.txt, and only when the labels carry pq_mlkem_call. A knob-off image with a byte at $A000/$B000/$BFFF refuses again; so does a PQ image with a byte just past its end; the PQ image itself is accepted. test_prg_load.py (13/13) restores the refusal list and pins all three cases; test_mlkem_placement also checks the real PQ PRG against the loader.
  • S2 Named wrappers pq_mlkem_keygen and pq_mlkem_decaps_seed (a client needs KeyGen and Decaps-from-seed only; Encaps and Decaps-with-dk have no wrapper because nothing calls them). The entry rule now reads the map's export list: ANY source outside mlkem_link.s naming a symbol the linker puts in $E000-$FDFF fails (27 symbols, e.g. keccak_f1600, mlkem_poly_ntt), and the wrappers are callable from anywhere. Red cases for both directions in the suite.
  • S3 Docs: RULE 3, the scrub header and engineering-notes describe the vector stub; IRQ text corrected: sei is LOAD-BEARING (CIA1 IRQ is level-triggered and unacknowledgeable with I/O out, so an IRQ reaching the RTI would livelock). Byte figures removed from the docs (CLAUDE.md: margins are measured, not written down); they live here.
  • N1 The I flag is checked on return with it clear (cli) and set (sei); mutant (d), php/plp replaced by nops, now goes RED (P=$34 for the cli case).
  • N2 The lda $A000 / beq gate is gone. A one-byte tail marker (LIB_MLKEM_MARK, $5C, last byte of the load image) is checked before the copy. No marker at the load address: if $E000's marker is there the image is resident (flag clobbered after 'Q') and the flag is re-armed; otherwise REFUSED: border red, mlkem_copied stays 0, pq_mlkem_* return A=$FF, C=1 and run nothing. Tested both ways in VICE (a PRG with the marker zeroed; flag cleared with the stage gone).
  • N3 Comment at the boot.s assert: it compares labels, the test is the real guard.
  • N4 Only the PRG is identical with the knob off. labels.txt/the memory policy on knob-off builds gain the __MLKEM_{CODE,BSS,POLY}_RAM_*, __COLD_FILE_* and __LOADADDR_* symbols, and __CRYPTO_COLD_SHADOW_FILEOFFS__ moves, so _memory_policy reserves $B100-$BBFF, $D000-$DFFF, $E000-$FDFF and $07FF-$0800 there. Harmless today (no rig scratch lives in those); not avoided because the areas must exist in the cfg.
  • N5 rig_mlkem_hw.py takes its scratch from labels.txt (cert_buf, cert_buf_size, tcp_recv_buf) and the page-3 arbiter; test_rig_scratch now covers it (PQ fixtures uci-onchip-pq, uci-comb-pq added to tools/rig_scratch_profiles.json, 18/18). Both rig phases run AFTER 'Q', so no in-session call (KeyGen between the menu and a connection) is proven yet: that is P4's job.
  • src/constants.inc, next to the dk rule: the 64 B d||z seed needs a home and a scrub span (P5), and ML-KEM never interleaves with X25519/fp_mul.

Review round 2: what changed

  • SF1 The loader's labels are now bound to the PRG: the span is allowed only if THIS PRG carries the tail marker ($5C) at the labels' marker address; otherwise no span is allowed (knob-off image + PQ labels, planted $A000/$B000/$BFFF: refused; labels for another image: refused; PQ image with no labels: refused, the false red that rigs avoid by passing their own labels). boot_check.py, rig_https_refetch.py and rig_mlkem_hw.py (the PRG-override callers; the rest use the repo's own build/) pass the labels next to their PRG. test_prg_load.py 13/13 carries the cases as red/green.
  • SF2 The entry ban scans *.inc as well as *.s and exempts nothing by prefix (__LIB_MLKEM_CODE_RUN__ and friends count; 33 symbols). Red cases: an .import in an .inc, a __LIB_MLKEM_* reference. A second check reads the ld65 map's Imports list: no module outside mlkem_link.o and the library's own archive members may import a banned symbol; a real probe module using .import .ident(.concat("mlkem_","keygen")) links, is missed by the source scan and is caught by the Imports check (zz_probe.o). Known gaps, accepted: a literal address (jsr $E123) and arithmetic on a non-banned symbol (__LIB_MLKEM_CODE_LOAD__+$4000).
  • SF3 On comb the precompute block restored the border after the refusal had set it red; boot.s now re-asserts red when mlkem_copied is 0. test_mlkem_linked.py --comb boots the comb PQ image with the marker zeroed in VICE with -reu (~140 s) and checks $D020. The comb refusal is guarded ONLY under --comb (the default run does not). The border mutant (boot.s without the re-assert) was a MANUAL run, not automated: RED ($D020=E; the adversary reproduced it, 28/29), green with the fix.
  • SF4 Success must return C=0: asserted in KeyGen and in both I-flag stubs (which enter with C set); mutant (e), the clc deleted, is RED.
  • N5 The marker's load address sits in live sqtab after boot, so a stale-RAM collision would re-copy over a good image. A link assert keeps the marker inside the table's planes, and the placement test computes the table byte there (n*n/4) and fails on a collision; the known collisions $BC67/$BD99 are red cases. The real marker load address is $BD41 (run $FD41, stage [$A000,$BD42)) on all four PQ profiles; there the table holds sqtab_lo[321] = $A0, not the marker. The test reads the address from labels.txt. Known limit, not fixed: case 3 ("resident") cannot tell which build left the image.
  • N7 Vectors first (above). N6 Docs: no byte figures in CLAUDE.md/engineering-notes, old gate and "moot" text corrected, test_mlkem_linked docstring lists mutants a-e and the refusal phases.
  • N8 Knob-off labels.txt also gains boot_zbss_first (all backends, ip65 too) and mlkem_copy_site is PQ-only; the PRG bytes are unchanged.

Earlier content of this PR (unchanged)

libs/mlkem at tag v0.6.0 (a00444a1) + build_mlkem.sh (discovered members, od65 checks, #124-style stale-checkout probe); PQ_HYBRID=1 on uci onchip / comb, with or without TRUST_STORE, $(error) on ip65, uci-m3, uci REU (its fp_mul DMA lands in mul_dma). Polys $D000 (4,096 B), LIB_MLKEM_BSS $B100-$BAF0 (2,545 B) over X25519_TABLES + $B900 hole + mul_dma; dk scratch mlkem_dk_scratch = tcp_recv_buf with ring >= 2,400 asserts (comb's COLD_IMAGE at $C000 is dead after cold_bank_init; the trust store/bundle also stage in the ring, so KeyGen goes after trust_pre); ZP $40-$4F (only co-tenant X25519 fe_wide); shared sqtab $BC00; scrub spans for window / polys (under sei, $01=$34) / dk.

Known gaps (not fixed here)

  • The LIB_SHARED_SQTAB_BASE baked into a sibling archive cannot be checked (never exported, immediates): editing the wrapper's 0xBC00 links clean. This is a known gap across all three siblings (nistcurves, x25519, mlkem).
  • The library's sqtab guard cannot pass CRYPTO_COLD_SHADOW/COLD_FILE (the window is c64-https's own table); mlkem_link.s asserts the equivalent and a test fails on any area with neither.
  • No ML-KEM caller exists yet, so the rule "KeyGen after trust_pre, zero dk before the first net_poll" is a comment at the equate.
  • _prg_load.py can no longer prove the $A000 stage before the run (BASIC ROM view) nor $E000 after it (KERNAL view); it now counts and names the staged bytes and rig_mlkem_hw.py proves the copy.

Byte identity, knob unset. Compared against NEW master 7b1ed07 (all seven identical)

profile sha256 (master 7b1ed07 == this branch, knob off)
ip65 reu 3fccbeb13d343b55d5a9a4fc7a59e9a4a09b9a3aaee26b65c497bc8f34a4354e
ip65 onchip e69bfce7b552e765df02cb253b4ff12cecaca3e978669376b7af5ffad9343dce
uci reu fe3b6c204d95fcdb3e818fcdc43275b72bd8ec5adc14fb28f7dfe26902846d20
uci onchip 9e11f570f219e7fcb6bd9ba0f8398ce8fee28f930d8022941c74d6c7f1f1f9e6
uci comb ad85797b67320b81441d6a651c12c164465e642c26fea346fc4e3d55a13e4a14
uci onchip TRUST_STORE=1 TRUST_RELEASE=1 1e82434885d87aa4e7a34d57230dc805759ddf18d3a081d95a5c7e85d353e70b
uci comb TRUST_STORE=1 TRUST_RELEASE=1 fee4d5b107b2f848bdaa41b6855aef3f2a2032920cf5a893fe8c71b2fa3e2f2b

PQ_HYBRID=1 PRGs: uci-onchip 6733fe2577358fce6e04d28fb6acd25d5147a89e06e0c464e49f781df478aa6f, uci-comb 667befa60939ac1cda2411d2696fa3738d4125f9a90d9b881e45c7d2f284591d, onchip-store 5dc459c2bc038399c36b821b00a28b5f3e7fb75d86c4e85b692c70fc69e4c418, comb-store e83f2c16cf48ab55eaea7f000c3ddf9290e8768eb7b948ae283b42b8f89b62b8. Knob-off hashes re-proved against master 7b1ed07 after this round: all seven identical (table above); the only knob-off change is the extra boot_zbss_first label.

Margins (measure_margins.py --build, tail free bytes; each table's PRG hash above)

region uci-onchip-pq uci-comb-pq onchip-store-pq comb-store-pq
LOADER 592 165 570 50
NET_CODE 389 381 389 243
NET_BSS_TAIL 1,375 1,375 1,375 1,375
CRYPTO_OVERLAY 2,578 325 372 55
CRYPTO_HOT 509 1,387 196 1,259
CRYPTO_COLD_SHADOW 0 0 0 0
MLKEM_CODE_RAM ($E000-$FDFF) 190 190 190 190
COLD_IMAGE - 3,670 - 1,697
COLD_RUN_UI / COLD_RUN_TRUST - / - 1,622 / - - / - 1,622 / 75

ML-KEM's measured cost against the same master: LOADER 24 B (uci) / 34 B (comb) (616->592, 199->165, 594->570, 84->50 on comb: the boot.s call, the scrub spans and, on comb, the border re-assert), NET_CODE 149 B (538->389, 392->243; boot copy, marker logic, vectors, wrappers, pq_mlkem_call). (#312 itself cost ~197 B of NET_CODE.) measure_margins.py now reports the RAM/file views as one region and the MLKEM_CODE_RAM run area.

Red-green evidence

tools/test_mlkem_placement.py 194/194 (cfg shape, knob matrix, 5 green links each also running the map-based entry rule (*.s and *.inc, no prefix exemption), the loader check and the marker/sqtab collision check, 18 mutants each failing with its own assert text, stale-checkout probe, restored relink).

tools/test_mlkem_linked.py 38/38 with --comb (34/34 without) (VICE, onchip with C64_VICE_NO_REU=1; comb with -reu): image == the PRG's $A000 bytes, vectors -> RTI, re-run harmless, flag re-armed from the $E000 marker, the I flag survives a call (clear and set) and success returns C=0, X25519 -> KeyGen (ek, dk exact) -> X25519 -> Decaps_seed (K exact; flipped ct differs), $01 restored, a marker-less PRG is refused (flag 0, red border, nothing copied, A=$FF C=1) on onchip AND on comb (border survives the precompute). Mutants, all RED: (a) no copy call, (b) copy after the zeroing, (c) no mlkem_arith_init, (d) no php/plp, (e) no clc; plus the comb border mutant (boot.s without the re-assert: $D020=E).

Other suites

  • BACKEND=uci USE_NISTCURVES_ONCHIP=1 PQ_HYBRID=1 tools/run_all_tests.py: 448/448, 3 suites skipped (net, reu_row_abi, ip65_exports; by design).
  • test_quit_basic_exit.py PQ: 74/74. test_prg_load 13/13, test_rig_scratch 18/18, test_measure_margins 19/19, test_device_prep 35/35, test_build_flags_stamp 21/21, test_pins, test_prg_io_range, test_runner_coverage, test_pytest_boundary 0 failures.

Hardware (U64E 10.43.23.81, DeviceLock, 48 MHz)

  • rig_mlkem_hw.py, PQ uci-onchip 6733fe25...78aa6f: 7/7. PQ uci-comb 667befa6...84591d: 7/7 (REU enabled by the prep). Both: image == the PRG's $A000 bytes, vectors, KeyGen ek/dk and Decaps_seed K match the reference. Both phases run after 'Q', so no in-session call is proven yet (P4).
  • Not rerun this round: boot_check.py and rig_https_local.py (earlier rounds passed; the boot path changed by a handful of bytes, covered by the rig's boot).

🤖 Generated with Claude Code

JC-000 and others added 4 commits October 16, 2026 22:21
Link-only: nothing calls ML-KEM. Code+rodata linked at $E000 (file="", not
in the PRG: #288), LIB_MLKEM_POLY_BSS at $D000, LIB_MLKEM_BSS at $B100 over
X25519_TABLES + hole + mul_dma, dk scratch in the TCP ring, ZP $40-$4F,
shared sqtab at $BC00. Asserts in src/crypto/mlkem_link.s, scrub spans for
all three secret homes, tools/test_mlkem_placement.py mutation-proves them.
Unset, all seven profiles are byte-identical to master.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… entry

Implements the 2026-10-13 decision: LIB_MLKEM code/rodata LOADS in the PRG
at $A000 (the file bytes under CRYPTO_COLD_SHADOW's BSS, which boot zeroes
anyway) and RUNS at $E000. No #288 relaxation: the PRG still ends at $BFFF
(or $CFFF on comb).

- cfg: CRYPTO_COLD_SHADOW becomes the RAM view (file=""), COLD_FILE the file
  view over the same $A000-$BFFF; unset, the PRG is byte-identical (all seven
  profiles). LIB_MLKEM_CODE/RODATA: load = COLD_FILE, run = MLKEM_CODE_RAM.
- mlkem_link.s: load/run/size asserts (head of COLD_FILE, same layout as the
  run image, fits one 30-page block copy, ends inside the PRG's file content,
  below the $FFFA vectors); mlkem_boot_init (copy + RAM vectors -> RTI, skip
  unless fresh: flag AND nonzero stage); pq_mlkem_call, the only entry (banks
  $01=$34 under sei, runs mlkem_arith_init, jsrs the entry).
- boot.s: jsr mlkem_boot_init right after sei, before the zeroing loop, with
  an assembler assert on the order.
- tools/test_mlkem_linked.py: VICE boot of the PQ image, compares $E000.. to the
  PRG's $A000.. image, KeyGen and Decaps_seed against the reference across
  X25519 runs; three mutants go red.
- measure_margins.py: RAM/file view aliasing, align_load, MLKEM_CODE_RAM row.
- test_quit_basic_exit.py: the code and vectors survive 'Q'.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…on hardware; _prg_load allows the staged image span

The $A000-$BFFF stage cannot be read back before the run (BASIC ROM) nor
$E000 after it (KERNAL), so rig_mlkem_hw.py parks the CPU with all RAM banked
in and compares. _prg_load counts and names the staged bytes instead of
refusing them; $D000+ and other non-zero tails still refuse.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@JC-000
JC-000 force-pushed the feat/pqc-p0-placement branch from 343a4f7 to 7281ac4 Compare October 17, 2026 03:45
JC-000 and others added 3 commits October 16, 2026 23:30
…ed wrappers + map-based entry ban, tail marker, I-flag test

S1 _prg_load: non-zero bytes allowed only in [CODE load, tail marker + 1) from
labels.txt and only on a build with pq_mlkem_keygen; $A000/$B000/$BFFF refuse
on knob-off images again. S2 pq_mlkem_keygen/decaps_seed wrappers; any source
outside mlkem_link.s naming a symbol the map puts in $E000-$FDFF fails. S3 docs
(IRQ: sei is load-bearing). N1 I-flag restore test + mutant. N2 tail marker
(LIB_MLKEM_MARK) replaces the $A000 gate; a cut-short LOAD is refused (red
border, A=$FF/C=1). N3 comment. N5 rig_mlkem_hw takes scratch from labels and
the arbiter; test_rig_scratch covers it with PQ fixtures.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mbols, comb refusal border, C=0 and sqtab-collision checks

SF1 loader keeps the stage span only if the PRG carries the tail marker at the
labels' address; boot_check, refetch and rig_mlkem_hw pass their own labels.
SF2 entry ban scans *.inc and exempts nothing by prefix. SF3 boot.s re-asserts
the red refusal border after the comb precompute (VICE-tested, red without the
fix). SF4 success C=0 asserted, mutant (e). N5 marker address vs sqtab bytes
(link assert + collision check). N7 vectors written first. N6 docs.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…try check, m3 labels, docstring

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@JC-000
JC-000 marked this pull request as ready for review October 17, 2026 05:51
@JC-000
JC-000 merged commit 10ccf25 into master Oct 17, 2026
@JC-000
JC-000 deleted the feat/pqc-p0-placement branch October 17, 2026 12:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant