Assurance matrix

RS-Key is not formally verified. This page is generated from the registry and reports what evidence exists, not that a whole-system theorem does. The Definition of done keeps this sentence a requirement until one exists, and scripts/claims_gate.py holds every page naming three or more registered properties to it. What is out of scope and what is accepted: limitations and the threat model.

Which security property is claimed about which buildable image. The rows are the P0-family properties of assurance/properties.toml; the columns are derived from nix/firmware.nix, firmware/Cargo.toml and firmware/boards/, so a new package, feature or board arrives as a column of gap cells rather than as silence. scripts/matrix_gate.py regenerates this page and scripts/check.sh diffs it.

The point of the page is the thing a single-build claim hides: the firmware is not one thing. Four of the nineteen images remove the physical-consent gate the authorization properties are about, one swaps the CTAP large-blob surface with no flake package at all, and the board axis changes the flash geometry on which a whole KV store once survived a “successful” wipe.

These are the committed configurations, not the buildable ones. Every mkFirmware knob falls back to a like-named environment variable and lib.mkFirmware is exported, so FLASH_SIZE=2M nix build --impure .#firmware is an image no column below describes — including under a disposition whose reason says “no cargo feature and no build knob”. What this page disposes of is what the flake ships and what CI builds; a one-off --impure combination is outside it by construction.

The axes

• 19 flake packages (nix/firmware.nix), of which 14 are published by .github/workflows/release-build.yml — the published set is a named subset of the matrix, never the matrix.
• 6 orthogonal cargo features (firmware/Cargo.toml) that no flake package expresses.
• 6 board presets (firmware/boards/*.toml): BOARD=<name> sets the same knobs the flake arguments do, and no cargo feature.

Columns

The last cell is DERIVED, not declared: the per-crate cargo-feature closure this column resolves to, against the default build’s. It is the same derivation the equivalent rule refuses a cell on, so a column reading — there compiles the workspace exactly as the default build does and its whole delta is knobs — and a column that names a crate has that crate’s code moving under every row of its column, which is the fact a gap there is about.

The matrix

40 rows × 31 columns = 1240 cells. Column numbers are the table above.

Dispositions

covered — basis default-build

• columns: firmware
• properties: SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008, SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006, SEC-LAT-001, SEC-LAT-002, SEC-LAT-003, SEC-POL-001, SEC-POL-002, SEC-POL-003, SEC-POL-004, SEC-POL-005, SEC-POL-006, SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-SEAM-006, SEC-ADM-002, SEC-ADM-004, SEC-BOOT-001, SEC-BOOT-002, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• The registry’s evidence is this column’s evidence: the models, Kani harnesses and host tests behind these 37 statements are produced with no firmware/Cargo.toml feature and no build knob, which is what makes this image theirs, and assurance/bundle/SEC-FIDO-001.toml records the column by name. Said that narrowly because the sentence it replaces — “every formal/*.cfg, every Kani harness and every host test scripts/check.sh runs” — is refuted three ways by the tree it is about: 5 of the 216 formal/*.cfg pin AlwaysUvShipped = TRUE, which assurance/assumptions.toml calls the arm the shipped image is NOT about; scripts/kani.sh appends --features kani-soft to every proof run; and 11 run_tests rows carry a cargo feature, 10 of them a firmware one. None of the three moves the disposition — those cfgs and rows are evidence about the columns they name, and kani-soft is declared by the crates/ members and swaps a SHA backend Kani cannot model, so no column derives from it — but all three had the strongest word in the vocabulary resting on a sentence its own tree refutes, which is what a basis is supposed to stop one record type over. It is still the one column where covered needs no argument beyond the derivation, and the one whose evidence says nothing about the other thirty.

out-of-scope — basis crate-absent

• columns: firmware, firmware-no-touch, firmware-fips, firmware-pqc, firmware-fips-pqc, firmware-no-touch-pqc, firmware-no-touch-fips, firmware-no-touch-fips-pqc, firmware-strong-pin, firmware-strong-pin-pqc, firmware-always-uv, firmware-always-uv-pqc, firmware-strict-up, firmware-strict-up-pqc, firmware-pico, firmware-2mb, firmware-16mb, firmware-strict-config, keygen-bench, core1-stats, bench, fido-conformance, ea-conformance-rpid, largeblob-ext, abrobot-16m, abrobot-4m, seeed-xiao, tenstar-usb, waveshare-one, waveshare-touch-lcd
• properties: SEC-DISP-001, SEC-DISP-002, SEC-DISP-003
• rsk-display owns the ceremony and rsk-ui the screen model, and both are dep:-gated behind --features display. The feature resolution the gate re-runs puts neither crate in any of these builds, so there is no ceremony to make a claim about. Note what this does NOT say: waveshare-touch-lcd is the trusted-display BOARD and still lands here, because a board preset sets knobs and never a cargo feature — the panel pins are compiled as inert constants.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: vidpid=Pico)

• columns: firmware-pico
• properties: SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008, SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006, SEC-LAT-001, SEC-LAT-002, SEC-LAT-003, SEC-POL-001, SEC-POL-002, SEC-POL-003, SEC-POL-004, SEC-POL-005, SEC-POL-006, SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-SEAM-006, SEC-ADM-002, SEC-ADM-004, SEC-BOOT-001, SEC-BOOT-002, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical per-crate cargo-feature closure — the gate re-derives it rather than taking this sentence’s word — so the whole delta is the one knob above, which firmware/build.rs resolves to the pair 0x2E8A:0x10FD; the descriptor strings swap only on the Yubico VID. No P0-family statement is about the reported identity: the CTAPHID rules key off channel ids, and the USB_ENABLED mask SEC-ADM-004 is about is a persisted record, not a descriptor. The one consequence that is not purely cosmetic is that the OpenPGP AID vendor follows the effective VID — and no row here depends on it, because SEC-SEAM-001 selects on the RID prefix. build.rs says the rest in as many words: the USB identity is cosmetic, never a security control.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flash.kvmain_kb=1408, flash.size_mb=4, led.kind=ws2812, led.order=rgb, led.pin=16, presence.source=bootsel, usb.vidpid=RSKey)

• columns: waveshare-one
• properties: SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008, SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006, SEC-LAT-001, SEC-LAT-002, SEC-LAT-003, SEC-POL-001, SEC-POL-002, SEC-POL-003, SEC-POL-004, SEC-POL-005, SEC-POL-006, SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-SEAM-006, SEC-ADM-002, SEC-ADM-004, SEC-BOOT-001, SEC-BOOT-002, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure, and every knob listed above is the value firmware/build.rs already resolves to when the knob is unset: VIDPID=RSKey, LED_KIND=ws2812 rgb on GPIO16, BOOTSEL presence, DEFAULT_FLASH_SIZE 4 MB with DEFAULT_KVMAIN 1408 K. BOARD=waveshare-one is the default image under a board name, which is why it is the only board that earns the whole column — and because the delta carries the VALUES, a preset that drifts off one of those defaults stops earning it.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flash.kvmain_kb=1408, flash.size_mb=4, led.kind=ws2812, led.max_leds=4, led.order=grb, led.pin=16, presence.active_high=False, presence.pin=23, presence.source=gpio, usb.vidpid=RSKey)

• columns: abrobot-4m
• properties: SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008, SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006, SEC-LAT-001, SEC-LAT-002, SEC-LAT-003, SEC-POL-001, SEC-POL-002, SEC-POL-003, SEC-POL-005, SEC-POL-006, SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-SEAM-006, SEC-ADM-004, SEC-BOOT-001, SEC-BOOT-002, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure AND the default flash geometry (4 MB, 1408 K KV main), so the axis that could reach a persisted-state property is unmoved. What is left is the LED backend, which reaches no P0-family statement at all, and the presence SOURCE — a GPIO button on 23 instead of BOOTSEL. FOUR rows are deliberately NOT in this list and stay gap: the ones whose statement QUANTIFIES OVER a presence decision — SEC-FIDO-001’s gate, SEC-FIDO-002’s per-transport touch, SEC-POL-004’s confirmed physical press and SEC-ADM-002’s Confirmed operator. Claiming those while the column’s own question asks whether this button has BOOTSEL’s semantics would be the two halves of one cell disagreeing. The four reset clauses used to be refused beside them, on the argument that an operator only ever REACHES a reset through a touch, and that argument is withdrawn as the wrong KIND: it is about reachability, and applied evenly it takes a row this cell already claims — SEC-FIDO-003’s own statement names reset among the invalidations it quantifies over, and it has been in this list since the cell was written. What the four clauses actually say is what a PREFIX of an authenticatorReset leaves in the store, and crates/rsk-fido/src/reset.rs puts the whole presence gate — shows_confirm, then the ceremony — ahead of the first sweep, which samples no button. The source of the press decides whether the sweep RUNS; the write ordering it is torn in the middle of is the same compiled code at the same geometry. The one thing this does not claim is the reverse direction: BOOTSEL sampling stalls XIP and a GPIO read does not, so the column removes a hazard from the reset path rather than adding one.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flashSize=2M, kvmain=896K)

• columns: firmware-2mb
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above: flash geometry, LED wiring, the presence pin, and the panel’s serial link. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

Re-decided when display.spi_freq_hz moved 62.5 -> 80 MHz with the PIO panel transport, because that knob is no longer only a panel knob: the transport takes its wire rate from clk_sys / 2, so this column now runs the whole part at 160 MHz where every other one runs 150. That is a real difference and it is recorded in docs/limitations.md, but it does not reach these six. They are statements about which state survives a selection and how a reassembly buffer is bounded — no clause in RSKeyAppletSeams or RSKeyTransport quantifies over time, a rate, or a deadline, so a core that retires instructions faster cannot make one of them true or false. A property that DID depend on timing would owe a conditional here instead, and none of the six is one.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flashSize=16M)

• columns: firmware-16mb
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above, all of them flash geometry, LED wiring or the presence pin. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flash.kvmain_kb=1408, flash.size_mb=16, led.kind=ws2812, led.max_leds=4, led.order=grb, led.pin=16, presence.active_high=False, presence.pin=23, presence.source=gpio, usb.vidpid=RSKey)

• columns: abrobot-16m
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above, all of them flash geometry, LED wiring or the presence pin. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flash.kvmain_kb=896, flash.size_mb=2, led.kind=ws2812, led.order=grb, led.pin=22, led.power_pin=23, presence.source=bootsel, usb.vidpid=RSKey, usr_led.active_high=False, usr_led.pin=25)

• columns: seeed-xiao
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above, all of them flash geometry, LED wiring or the presence pin. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: flash.kvmain_kb=1408, flash.size_mb=16, led.kind=ws2812, led.order=grb, led.pin=22, presence.active_high=False, presence.pin=15, presence.source=gpio, usb.vidpid=RSKey)

• columns: tenstar-usb
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above, all of them flash geometry, LED wiring or the presence pin. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

equivalent — basis same-cargo-features (same_as = firmware; knob delta: display.bl_pin=16, display.bl_pwm_channel=A, display.bl_pwm_slice=0, display.cs=13, display.dc=14, display.rst=15, display.spi_freq_hz=80000000, display.tp_rst=17, display.wake_active_high=False, display.wake_pin=25, flash.kvmain_kb=1408, flash.size_mb=16, led.kind=none, presence.source=bootsel, usb.vidpid=RSKey)

• columns: waveshare-touch-lcd
• properties: SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003
• Identical cargo-feature closure — the gate re-derives it — so the delta is the knobs listed above, all of them flash geometry, LED wiring or the presence pin. These six statements are about in-RAM state only: the applet security status that lives for the duration of a selection, and the CTAPHID reassembly buffer. Neither reads PK_FLASH_SIZE/PK_KVMAIN_LEN: inside the firmware image firmware/src/flash_storage.rs is their only consumer. Not in the tree — rsk-wipe/src/main.rs reads PK_FLASH_SIZE too, from its own build.rs, which is a separate binary and is what the next sentence is about. Every other row on this column stays gap, because the store IS what the geometry changes: check.sh rebuilds rsk-wipe once per board because a change that stopped BOARD reaching the wiper once left a 16 MB board’s whole KV store standing behind a “successful” wipe. Those rebuilds mean something only because of the row beside them, check.sh: rsk-wipe refuses an unknown flash size, which fails a wiper that links with no board at all — it used to fall back to 4 MB at EXIT=0, so the per-board loop passed whether or not BOARD was reaching it. Cited with the check.sh: prefix because that label carries no parentheses, and the shape rule alone sees 52% of the row namespace.

out-of-scope — basis gate-compiled-out (feature = no-touch; gate: firmware/src/presence.rs; hook: rsk_sdk::UserPresence)

• columns: firmware-no-touch, firmware-no-touch-pqc, firmware-no-touch-fips, firmware-no-touch-fips-pqc
• properties: SEC-FIDO-001, SEC-FIDO-002, SEC-POL-004, SEC-ADM-002
• no-touch replaces the button watcher with an instant auto-confirm (firmware/src/presence.rs), so the physical-consent gate these four statements are ABOUT is not in the image: “the live authorization its own gate requires”, “a presence decision produced for one transport”, “a confirmed physical press”, “a Confirmed operator presence”. The claim is not weakened here, it is not made — and the tree already treats these builds that way. None of the four is published, firmware/Cargo.toml says “Never ship a no-touch build”, and release-build.yml refuses to create a release carrying one. “No-touch image” in the singular is the phrasing that hid four packages.

Open gaps

The middle column is derived, and it is what a gap here costs: the open rows whose OWNING crates — the ones whose production Rust carries the property’s tag — are among the crates the column compiles unlike the default build, above. Outside it, the code the statement is about did not move and the question is whether the rest of the image reaches it; inside it, the statement is about a different compilation. Every P0-family row carries a production tag, so the one direction this number could be wrong in — an untagged row counting as not moving — is empty here.

The two after it are the ledger’s, and they are Stage 0’s last exit bullet: who owes the answer, and what would end the deferral. Settled by is typed rather than dated — evidence is a check.sh row built at this column, absence an out-of-scope argument, sameness an equivalent one, and ruling a decision no derivation can produce, which is the maintainer’s. The gate refuses sameness where the closure delta is non-empty and absence where neither of its bases can reach a row, so two of the four are claims the tree can already disagree with.

Property names