Platform assumptions
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.
The assumptions no model constant can carry. assurance/assumptions.toml holds the other kind — a Boolean TLA constant a configuration assigns both ways — and refuses these by construction: M7-Q2 put there answers in the registry but no configuration assigns it, and so does a board PASS, and so does emulator fidelity. They are statements about a platform, a tool or an abstraction, and there is no other arm to run.
Discharged: 9 of 92. That number is the point of the page. Everything else is an obligation with an owner and a named route, and none of it is evidence about anything yet.
What discharges what
Nothing in this repository can discharge 13 of these rows: their route ends at a board, and AGENTS.md puts flashing and every board operation with the maintainer. A row moves off pending only with artifacts in the tree; a silicon-class row additionally with the stepping it was taken on, any row naming a stepping must name a real one, and a row naming one owes a capture under assurance/board/ — because a rule met by any file that merely exists is met by a README.
Each of those 13 owes a RECORD as well — assurance/board/<id>.toml — split into the half that is knowable before the board is powered (method, boot_config, expected) and the half that is not (board, stepping, firmware_sha256, first_boot_capture, actual, arm_taken). A result field on a run that has not happened is refused, and so is an expected first committed in the same commit as its result. expected is printed here beside the outcome rather than summarised, because the outcome is one word and the criterion is the thing it has to have met: a row whose own arm says it still owes a second instrument reads, in one word, exactly like one that owes nothing. arm_taken is what holds the two together — it names the arm the run took and then reproduces, up to whitespace, the WHOLE of the expected beside it. The whole and not the arm’s own sentence, because criterion prose written after the first label belongs to one arm and is dropped by every other quotation: on the row about the boot ROM’s scratch word, a PASS quoting its own arm leaves behind the sentence saying a vendor erratum settles the row as well as a board does. It is owed wherever the record states an arm under that outcome, which is every PASS and every FAIL.
Two prices this page owes the reader rather than the rule. An arm has to OPEN a sentence — PASS = … after a full stop, colon or semicolon, and not after a comma, a dash, a bracket or an ellipsis, and not written Pass = — so seven honest spellings are a red at planning time, each with its own message saying the label is there and misplaced. And what is enforced about ORDER is smaller than it looks: the gate asks that some commit carry this expected under outcome = "planned", not that the commit predates the run. A record can be re-planned and re-recorded in two commits, neither of them red, which is what it costs to weaken a criterion after the board has spoken. What they say today:
| record | outcome | expected |
|---|---|---|
PLAT-DISPLAY-001 | planned | The photographed card is the one the ceremony armed, and every control responds at the coordinates the hit test claims. PASS = both. FAIL = either — a card the user did not see, or a control at coordinates they did not aim at, is a confirmation of an operation nobody read. INCONCLUSIVE = the panel could not be photographed at the arming instant. |
PLAT-FLASH-001 | planned | Every interrupted write leaves the record readable as the OLD value or refused as corrupt. PASS = old-or-refused at every delay tried, with the delays listed. FAIL = one record that reads back as a well-formed value nobody wrote, which falsifies the store model outright. INCONCLUSIVE = no delay landed inside the program window, which the script cannot tell you on its own – it asserts about the device after the cut, not about the record’s bytes, so classifying the record is a second instrument this row still owes. |
PLAT-INPUT-001 | planned | The PIN entered at the reader’s own pad reaches the card and spends the SAME persistent retry budget the CCID path spends. PASS = a wrong PIN at the pad decrements the counter and a correct one refills it. FAIL = a verify that does not reach the ladder, which is an unmetered guessing channel. INCONCLUSIVE = the reader does not advertise the feature, so nothing was exercised. |
PLAT-MEM-001 | pass | Main SRAM does not survive the drop. PASS = every byte of the dump is zero AND the written pattern reads straight back, which is the script’s settled (exit 3) – both halves, because zeros alone have two causes and the writeback separates them. FAIL = the pattern, or any non-zero live region, which puts an unwrapped seed inside reach of anyone who can hold BOOTSEL. INCONCLUSIVE = zeros with a writeback that does NOT read back (exit 2), or a short dump: picoboot is not serving SRAM and nothing found or not found in it would mean anything. |
PLAT-OTP-001 | planned | A half-written key row is REFUSED, not read as a key. PASS = the derivation fails closed and the device reports unprovisioned. FAIL = a derivation succeeds on partial material, which is the FAKE_MKEK failure mode a real board would mimic silently. |
PLAT-RESET-001 | planned | scratch2 reads as CLEARED on the first boot after the cut, so the soft lock does not ride the power cycle. PASS = cleared or unreadable-as-garbage, because firmware/src/pin_lock.rs:36-37’s tag makes garbage read as clear. FAIL = the tag and the mismatch batch read back intact. INCONCLUSIVE = the read could not be taken on the first boot, which is the only failure mode that does not settle the row either way. |
PLAT-ROM-001 | planned | scratch2 reads back AS THE FIRMWARE LEFT IT. PASS = the tag and batch survive, so the bootloader is not a way out of the lock. FAIL = cleared, which is the security direction and would make the vendor reboot a lock-shedding channel. No datasheet clause states it either way; a vendor erratum settles it as well as a board does. |
PLAT-ROM-002 | pass | The device enumerates as the RP2350 mass-storage bootloader after the command, and the CCID interface is gone. PASS = the drive appears. FAIL = the device re-enumerates as the authenticator, i.e. the command performed a warm reset and the P1 byte is not doing what the applet says. |
PLAT-TIMER-002 | planned | The alarm comparator’s wrap is invisible to everything above it. PASS = across a run of at least two periods with no host traffic inside the window, the recorded LED never stops changing – no interval longer than 10 s in which it holds one value, against an ambient cycle of 1 s on the blinking backends and about 2 s on the breathing one – and the bus capture (or the absence of a host) shows the window was quiet. AND THE BOARD NEITHER REBOOTED NOR LOST ITS SUPPLY: on the bracketed arm no second EV_BOOT in the post-window journal and a closing uptime accounting for the whole recording, on the charger arm a supply shown not to have dropped. That condition sits on the PASS and not only on the FAIL because the mirror is real: a board that browns out every thirty seconds never reaches a crossing at all, and its recording is a render that never stops changing – this row’s PASS over a run that tested nothing. FAIL = one interval of the order of the period itself, up to 71 min 35 s, in which the LED holds a single value and then resumes. That is what a missed match costs: the deadline is not late by a millisecond, it waits for the counter’s low half to bring the same armed value round again, and it is the ONE alarm the whole queue is served by, so what stalls is every timer on the device at once. A FAIL REFUTES THE STATEMENT – scripts/platform_gate.py:1337 maps fail to refuted – so the interval alone is not enough, and two causes that have nothing to do with the comparator produce exactly it. A brown-out that recovers leaves a dead stretch and then repaints the render. A probe that halts a core and resumes it does the same, and TIMER0’s DBGPAUSE makes that a DOCUMENTED way to stop this counter – assurance/board/PLAT-TIMER-003.toml refuses a debugger by name and this row did not. So a FAIL is owed, beside the interval: no debugger attached at any point in the window; a supply shown not to have dropped; and, on the bracketed arm, no second EV_BOOT and a closing uptime accounting for the whole recording. INCONCLUSIVE = a run shorter than two periods; a recording with a gap in it, because a crossing that cannot be shown to have been watched is not a crossing that was survived; ANY host traffic inside the window, because a request re-arms the comparator and would repair a missed match before the LED could show it, which would make the run an observation of the host rather than of the wrap; a debugger attached at any point, since a halted core stops this counter by design and the run is then about the probe; a supply that dropped, or a second EV_BOOT in the post-window journal, or a closing uptime materially shorter than the recording – a reboot, which the second EV_BOOT is what names, both repaints the render and restarts the comparator’s phase, while a short uptime with NO such entry is the counter having stopped, the last arm below; neither the stall nor its absence is this row’s to read on either; the charger arm run with no supply record, which has no reboot instrument at all; and an image or an LED configuration with no animation in it – LED_KIND=none, brightness zero, steady mode – which observes an absent instrument rather than a wrap; and a series that stops and NEVER resumes before the recording ends, which is not this row’s FAIL at all – a comparator whose counter has stopped can be observed neither to miss a match nor to make one, so this row has nothing left to read. WHAT THIS RECORDING SETTLES HERE AND NOT IN assurance/board/PLAT-TIMER-003.toml, which reads the same series for progress. The FAIL above is that row’s PASS: a stall of the order of one period that ENDS is a counter that went on counting and brought the armed value round again. The stall that never ends is that row’s FAIL and this row’s INCONCLUSIVE, above. And the one arm both records answer the same way is a freeze beginning less than a period before the recording ends, inconclusive for both because nothing has yet told the two apart – which is the second thing the second period buys, beside the one the method already names. |
PLAT-TIMER-003 | planned | The counter advances for the whole of a bounded window, and the render is what says so. PASS = the recorded series has NO interval in which the sampled LED takes one value and never changes again – every quiet stretch is followed by more change, right up to the last sample – AND, on the bracketed arm, the uptime of the entry THE CLOSING COMMAND APPENDED is not materially shorter than the wall-clock length of the recording and no second EV_BOOT stands in the window, which together rule out a reboot that repainted the render; on the charger arm a supply shown not to have dropped stands in for both. FAIL = the series stops changing and stays stopped to the end of the recording, with at least one full period, 4294.967296 s, recorded after it stops. That is a counter that quit: every task in the queue is waiting on an alarm that can no longer match, and the three properties this row supports – EveryOpQuiesces, EveryWaitReleases, EveryWalkCloses – are false of every operation in flight and of every one begun afterwards, each being an EVENTUALLY claim on a device where nothing is ever again. THE SECOND WITNESS IS OWED HERE TOO, and was not until 2026-09-05: this arm sat under a PASS carrying an uptime condition and carried none itself, while a FAIL REFUTES the statement (scripts/platform_gate.py:1337 maps fail to refuted). So a FAIL needs, beside the frozen series: on the bracketed arm a closing uptime materially shorter than the recording and no second EV_BOOT saying the board rebooted, and on the charger arm a supply shown not to have dropped. WITHOUT IT THE ARM IS SATISFIED BY A HALTED PROGRAM RATHER THAN A STOPPED COUNTER, which is the nearest thing this tree has to this row’s own failure and is reachable in it: firmware/Cargo.toml:75 is panic-halt = "1" and nothing arms a watchdog reset anywhere – WATCHDOG appears only as the scratch register firmware/src/pin_lock.rs:54 writes – so a panicking render task freezes the frame for ever with the counter in perfect health. AND IF THE CLOSING COMMAND DOES NOT COME BACK, that is a reading rather than a gap: a stopped counter wedges everything that awaits a Timer, so a device that still ENUMERATES and will not answer the close answers this arm the same way a short uptime does. A device that does not enumerate at all is the INCONCLUSIVE arm below instead, because a halted core produces that too and nothing outside the device tells the two apart. INCONCLUSIVE, and every arm of it but the last is about the RUN. That matters because the last one IS about the configuration and could otherwise be read as this row forbidding its own PASS: it does not, because the image boot_config names takes none of these arms – the shipped default compiles a render task, animates it out of the factory EF_LED_CONF, needs no debugger and no host, and so produces the PASS above on any supply that holds. The arms: a recording with a gap, since a stretch nobody watched cannot be shown to have been a stretch of change; the device does not enumerate after the window, which is the halted program’s other half and an arm of its own rather than a note on the one above – a panic takes USB down with the render, so the second witness is unreadable at exactly the moment the reading calls for it, and a frozen frame with no journal behind it does not tell a stopped counter from a stopped program; a freeze beginning inside the last period, which is PLAT-TIMER-002’s stall and this row’s failure with nothing yet to tell them apart; a debugger attached, since DBGPAUSE makes a halted core a documented way to stop this counter and the run would then be about the probe; a supply that dropped, or a SECOND EV_BOOT in the post-window journal, since a reboot repaints the render and reads as continued progress – and it is that entry and not a short uptime that names a reboot, because a stopped counter shortens the uptime as well and THAT case is this row’s FAIL above, not this arm; a recording sampled at or near the ambient cadence, which aliases into a held value; and an image or an LED configuration with no animation in it, which observes an absent instrument. WHAT THE SHARED RECORDING DOES NOT SETTLE HERE, said because a reader who has just read the other record will carry its verdict across. PLAT-TIMER-002’s PASS is not this row’s: it is satisfied by a counter that stops one second after the recording ends. PLAT-TIMER-002’s FAIL is this row’s PASS, since a stall that resumes is a counter that went on counting. Only the never-resuming stall is this row’s FAIL, and it leaves that row INCONCLUSIVE rather than joining it. |
PLAT-TOOL-002 | planned | The board’s session agrees with the emulator’s at every recorded boundary. PASS = no divergence. FAIL = any boundary where the board gates differently, which makes every trace-linked claim a claim about the emulator. INCONCLUSIVE = the session could not be driven to the same boundaries on the board. |
PLAT-TRNG-002 | planned | The raw source clears the floor the shipped whitening needs at the sample spacing the product uses, and the floor is THIS RECORD’S OWN rather than a vendor’s. WHY HALF A BIT PER RAW BIT, argued here because the record this replaces cited a datasheet figure that does not exist, and argued in the direction a review had to correct once already: a von Neumann debiaser emits AT MOST one bit per two raw bits, so if h is the raw min-entropy per bit and R the balancer’s output-per-input rate, the input min-entropy standing behind one whitened bit is h/R, and R is at most one half. At h = 0.5 that is at least one full bit, AT EVERY RATE THE BALANCER CAN ACHIEVE, and at a slower real rate more. SO THE FLOOR IS SUFFICIENT FOR THAT COUNTING BOUND AND IT IS NOT NECESSARY, which is the opposite of what this field said first: below 0.5 the bound stops holding, the device does not, and a real source at h = 0.25 sits at R near 0.13 and still clears one bit per whitened bit. Von Neumann’s output is exactly uniform for any fixed bias, so bias alone never starves it; what does is CORRELATION between consecutive samples, which is the thing sample_count was raised to reduce and the thing the non-IID track is chosen to see. That is why the verdict is read off the capture at the SHIPPED spacing and not off the bootrom’s period-0 one. It is deliberately not derived from §12.12.1’s approximately 7.5 kb/s of entropy, which is a rate and not a per-bit figure. PASS = the SP800-90B §6.3 non-IID estimator suite, run over at least 1,000,000 consecutive raw samples captured with all three bypass bits SET and SAMPLE_CNT1 AT THE SHIPPED 1000, returns a minimum-over-estimators min-entropy of at least 0.5 bits per raw bit, AND the period-0 control capture and the AUTOCORR_STATISTIC readings at sample_count 25 and at 1000 were TAKEN over the two equal-time windows method names — trip count and block count both — and are recorded in actual. THE SECOND CONJUNCT IS A RECORDING OBLIGATION AND NOT A COMPARISON, and that is deliberate rather than loose: on a healthy unit the autocorrelation check may trip zero times at BOTH settings, so a clause demanding a strict decrease from zero would be a route no passing world walks — which is the defect this whole split exists to remove, reintroduced one conjunct further in. What the two numbers are for is the row’s prose and not its verdict: a trip rate that does not fall at 1000 says the raise firmware/src/main.rs:609 made bought something other than what its comment claims, and that is worth recording whichever way it comes out. FAIL = the SHIPPED-SPACING capture’s estimate comes back below 0.5 bits per raw bit, on the die this project owns and at the conditions it runs at. That refutes this row’s statement in the statement’s own terms — the floor is what the row claims and the floor is what was missed — and it deliberately claims no more. What it costs the device stays OPEN: the counting bound the floor secures is sufficient and not necessary, so a real balancer rate below one half spends more raw bits per whitened bit and may still carry a full bit into each, and nobody here has measured that rate. It is not a small open question, because every key, nonce, blinding factor and pinUvAuthToken drawn after boot rests on the seed either way and PLAT-TRNG-001’s three continuous checks pass such a source by construction. A FAIL here is a demand for the rate measurement, not a proof the device is broken; overstating it is how the record this replaces came to name a figure nobody published. A FAIL is gate-forced to refuted (scripts/platform_gate.py:1337 maps fail to refuted), so it owes two things beside the number: TRNG_DEBUG_CONTROL and SAMPLE_CNT1 READ BACK after the capture and recorded, and the capture’s own hash. A bypass write that did not take yields a WHITENED capture, and a whitened capture estimating low is a broken instrument rather than a weak source, which is the nearest thing to this row’s failure that is reachable by accident. INCONCLUSIVE = any run that is not about the source at the spacing the statement names, and each arm is one way to get there: a verdict read off the period-0 CONTROL capture rather than the shipped-spacing one, which is a stream the device never draws and the mismatch this record was rewritten to remove; a capture shorter than the length the estimator suite is specified over; a capture taken through the shipped image, or with any bypass bit clear on read-back, which is whitened output and is the very test the statement says cannot answer this; a capture whose EHR_DATA5 read was not last on every block, since that read is what clears the result registers and a stale block repeats itself into the stream; an estimate taken on the IID track over a capture that fails SP800-90B §5’s permutation tests, which is the flattering-number shape; a run at a temperature or a supply outside desk conditions, which is PLAT-TRNG-003’s question and not this one’s; and a result ASSEMBLED FROM MORE THAN ONE BOARD, because this row is one die: a spread across parts is PLAT-TRNG-003’s claim and not this one’s, so a second board is a second run of this row and never a wider one. |
PLAT-XIP-001 | planned | Core 1 is halted for the whole of every erase and program, and resumes. PASS = no XIP fetch inside the window and a clean resume. FAIL = either a fetch during the array write — a hard fault or worse, silently wrong data — or a pause that is never released, which is a wedge. |
The candidates are DERIVED — 136 of them, from the slice bundles and design pages, the model registry, the suites no runner in this tree can pass, every unsafe SITE in first-party Rust, and the semantics a crate-ledger row says its model abstracts. An unclaimed candidate reddens scripts/platform_gate.py; so does a claim on a candidate that no longer exists. 31 of them are unsafe sites, keyed by their own code rather than by a position, so that a site inserted above another cannot renumber a row onto a different one — and where two sites agree, the key spends MORE of their own words rather than numbering them, because a ~2 re-points on a reorder and that is the same defect one layer down.
Which sites go under which row is not the registry’s to choose alone. docs/unsafe.md numbers its justifications, each heading names the row it enumerates, and the numbering has to partition the runtime sites with each row’s section spanning exactly the sites that row covers. Every row also has to NAME, in its own words, the file of each site it claims. Without those two, covers was checked only for existence in both directions: collapsing all 31 site keys onto one discharged row and emptying the eleven others was byte-identical output at exit 0.
The registry
| ID | Class | Statement | Status | Discharged by | Owner | Supports |
|---|---|---|---|---|---|---|
PLAT-AUVGATE-001 | model-abstraction | ResetKeepsTheAlwaysUvGate has no falsifying state wherever AlwaysUvShipped = TRUE, so the three green configurations on that arm assert it vacuously. gate.alwaysUv has two writers: ConfigOp (RSKeySecurityState.tla:1115), which sets snap' = NoSnap in the same action and so cannot leave the clause’s antecedent standing, and ResetSweepGates (:1438-1439), guarded by gate.alwaysUv # AlwaysUvShipped and assigning that constant — which on the TRUE arm can only RAISE the flag. | pending | A configuration that arms BugResetGatesFirst at AlwaysUvShipped = TRUE and is recorded on this clause, which would exhibit the vacuity rather than argue it. No such configuration exists: measured over all 210, the five taking that arm (AlwaysUv.cfg, PermWide.cfg, ForceChange.cfg, PermWideMut_BugConsumeKeepsMcGa.cfg, PermWideMut_BugStopUsingKeepsPerms.cfg) and the five arming that switch are disjoint sets. Until one is written the discharge is a reading of the two writers, which formal/gen-configs.sh:211-225 also carries and which is why clauses=1 is on Shipped.cfg and on no other baseline. | contributor | SEC-FIDO-006, SEC-FIDO-006B |
PLAT-AUVGATE-002 | model-abstraction | The model’s consequent for this clause is the alwaysUv FLAG and the Rust α’s is the EF_ALWAYS_UV RECORD’s presence, and the two coincide only while the compiled default is off — so every Rust-tier artifact for SEC-FIDO-006B is evidence about a record, not about a gate. | pending | Either a cfg(feature = "always-uv") arm in crates/rsk-fido/src/reset_assurance.rs that makes the α’s consequent the EFFECTIVE state, or a stated narrowing that the clause is about the record. Neither exists today: git grep 'feature = "always-uv"' crates/rsk-fido/src returns crates/rsk-fido/src/config.rs:315 and crates/rsk-fido/src/conformance/config.rs:77 and nothing in the reset family. The cost is measured — the six reset_assurance tests report 6 passed; 0 failed on BOTH feature arms, against two different test binaries. crates/rsk-fido/src/config.rs:351-359 is the site that makes the coincidence hold on the default build and break on the other. | contributor | SEC-FIDO-006B |
PLAT-BUILD-001 | build-configuration | The DEFAULT image is built without --features always-uv, so gate.alwaysUv is a free state variable a platform toggles rather than the compiled default every reset restores. firmware-always-uv is a published package and is the other arm, not a counterexample. | discharged | The build itself: firmware/Cargo.toml’s default feature set does not name it, and docs/assurance-matrix.md carries the firmware-always-uv column separately. Both arms run — every configuration the shipped image is about pins the constant FALSE, and AlwaysUv.cfg runs the whole invariant set with it TRUE. | contributor | SEC-FIDO-001, SEC-FIDO-004, SEC-FIDO-006, SEC-FIDO-006B |
PLAT-BUILD-002 | build-configuration | ea-conformance-rpid’s enterprise-attestation allowlist is a conformance fixture and not an authorization gate, so the authorization properties are unchanged in that column. | pending | The settling question docs/assurance-matrix.md already carries for that column, answered against the two production sites that read the allowlist. | contributor | SEC-FIDO-001 |
PLAT-BUILD-003 | build-configuration | The display build implements the one-hold-one-ceremony latch SOMEWHERE ELSE: it compiles ButtonWait out entirely and the panel’s own release debounce takes over, so the model keeps a defence that build has in a different place rather than one it does not have. | pending | The firmware-display and waveshare-touch-lcd matrix cells, which are gap for this property today. firmware/src/presence.rs:99-101 gates the button backend on not(feature = "display") and :163-166 swaps Presence to crate::display::TouchPresence; crates/rsk-display/src/presence.rs:45-48 clears the stale cancel in the panel’s OWN loop, not in ButtonWait::wait, and crates/rsk-display/src/lib.rs:131-134 gives the trait a no-op set_up_pending. formal/RSKeySecurityState.tla:473-477 states the direction: NARROWER than the display build. No configuration and no harness in the tree runs the display build’s version of this rule. | contributor | SEC-FIDO-002 |
PLAT-BUILD-004 | build-configuration | On the four no-touch images no presence DECISION is produced at all — the arbiter is still compiled in, but nothing can reach the wait that would consume one — which is why this property’s cells there are out-of-scope and not gap. | pending | Reading the cfg arms, and it is decided rather than open. firmware/src/presence.rs:202-258: request and request_ceremony return Presence::Confirmed unconditionally under feature = "no-touch", poll_pressed returns false, and ButtonPresence::wait is cfg(not(feature = "no-touch")) so ButtonWait::wait — the sole caller of set_up_pending(true) on a non-display build — is never called. Arbiter itself, and the three Refines-tagged functions on it, ARE in those images; what is absent is the decision, not the arbitration code. firmware/Cargo.toml says “Never ship a no-touch build” and release-build.yml refuses to release one. | contributor | SEC-FIDO-002 |
PLAT-BUILD-005 | build-configuration | Every shipped image is built with CONSTANT_MEMORY_ACCESS_PATTERN 0, and that is a DEFERRAL with a price rather than a default nobody read. The vendored header defaults it to 0 and recommends that value for Cortex-M (crates/rsk-rsa/csrc/bignum_config.h), and crates/rsk-rsa/build.rs passes no -D for it, so there is no build knob: turning it on is a source edit. Read out of the source, the other arm does two things. It replaces table_entry = temp + four_bits * modulus_length_bytes with a call to bignum_table_select, which scans ALL sixteen entries branchlessly on usub8/sel and copies the chosen one into scratch; and it prepends an in-place cycle-following transpose that re-lays the table into 8-word blocks for that scan. Neither has ever been built here, and not merely never exercised: bignum_table_select sits inside #if CONSTANT_MEMORY_ACCESS_PATTERN in crates/rsk-rsa/csrc/bignum_asm.S, so at 0 it is not assembled at all, and the transpose is under the same guard in crates/rsk-rsa/csrc/bignum_high_level.c. | accepted-risk | A build and a board, in that order, and neither has been taken — every number below is COUNTED FROM THE SOURCE and none of it is a measurement. (1) Build firmware with the flag defined and confirm bignum_table_select is in the image. That is minutes, and it settles the size cost, which is not only flash: both halves are RAM-resident by section — the C carries BIGNUM_RAMFUNC, which is section(".data.bignum_hl"), and the asm’s whole translation unit is .section .data.bignum_asm — so the flag spends SRAM on a part whose stack ceiling is already the binding one. (2) A board, because nothing else can run it: crates/rsk-rsa/build.rs compiles the C and the asm only for target_os = "none", so no host test and no tools/emu run reaches this arm at all, and the transpose’s correctness is exercised by an on-card RSA sign at each of the three widths and by nothing else. The Bellcore check in crt::private_op turns a wrong transpose into a refused signature rather than a bad one, so a passing on-card sign IS the proof — and a failing one is a key that stops working, which is why this may not be turned on blind. (3) Time one PIV GENERAL AUTHENTICATE or one OpenPGP PSO:CDS on each arm for the real cost. Counted from the instruction mix, bignum_table_select reads 16 x half bytes per window where the shipped arm reads half, against a window that already spends four squarings and one multiply, so the overhead is of the order of a tenth of the private operation and is LARGER at RSA-2048 than at RSA-4096 — the multiply cost grows quadratically in the width and the table scan only linearly. WHAT TAKES THE DEFERRAL OFF, since an accepted-risk row may carry no revalidated_by: PLAT-CRYPTO-002 being re-opened by any of its triggers, or a board becoming available for the three widths — whichever comes first. The flag is the fix; this row exists so that not taking it is a decision with a price rather than a header default. | contributor | — |
PLAT-CRED-001 | model-abstraction | r \in store.rpent is read as the EF_RP record for r is reachable by the management surface, and in the shipped tree it means only that the record exists: both browse surfaces additionally require the read to succeed, the count byte to be positive and the rpId to unseal. | pending | Either a second model variable separating the record exists from the record lists, or a test at each surface that drives a refused EF_RP read and a record whose domain will not unseal and asserts what the owner is shown. The six arms are crates/rsk-fido/src/credmgmt.rs:364, :368, :402 and crates/rsk-fido/src/passkeys.rs:113, :117, :122, and the two surfaces do not agree on the third: enumerate_rps answers CtapError::Other for the whole walk, so one unsealable record hides every other relying party from the host, while for_each_rp skips that one record and lists the rest. | contributor | SEC-FIDO-005 |
PLAT-CRED-002 | model-abstraction | No action of RSKeySecurityState can fail a flash write: the model’s only tears are PowerCut and ResetAborts between two writes that succeeded, so an Fs::put returning Err — and a best-effort rollback that itself fails — is outside every configuration the FIDO properties are checked on. | pending | Either a failing-write action in formal/RSKeySecurityState.tla (which needs the rollback modelled with it, and the rollbacks are best-effort BY CONSTRUCTION — each is itself a flash write), or a bounded proof over rsk-fs’s Fs with a symbolic write/delete outcome per step. CHANGELOG.md [0.4.11] Still open, same class, and named here names five open sites of exactly this class; all five strand an EF_RP entry over a missing credential, which is the direction store.cred \subseteq store.rpent does not constrain, so the cost falls on the opposite direction — asserted by SEC-STORE-006 NoSilentOrphan, on a different model. | contributor | SEC-FIDO-005 |
PLAT-CRED-003 | model-abstraction | KeepOpen equates the seed that opens it is gone with the record is not there, so a reset that leaves an undecryptable EF_CRED record behind is store.cred = {} in the model. | pending | A model that carries the record and its openability apart — the same second variable PLAT-CRED-001 wants, one layer down. formal/RSKeySecurityState.tla:310-314 defines store.cred as the records that still OPEN and empties both fields when the last seed copy goes, while docs/threat-model.md’s TM-HOST-CRED-REVOCABLE says of the wipe that a torn wipe can still strand a credential, and what the ordering buys is that the survivor is undecryptable rather than that it does not exist. The two agree in substance and differ in what a record IS. | contributor | SEC-FIDO-005, SEC-FIDO-006 |
PLAT-CRED-004 | model-abstraction | FixSweepDropsCredsBeforeRpEntries — the counterfactual repair the model carries for the reset half of NoUnmanageableCredential — is assigned TRUE by exactly one configuration, and that arm has now been RUN: the model has checked whether the repair holds the invariant, and it does. | discharged | DISCHARGED BY THE RUN THIS ROW WAS WAITING FOR, and by nothing else that changed. The emit call it asked for exists — formal/gen-configs.sh:322 is emit Historical_E76.cfg BugSeedDoesNotLead TRUE TRUE, over Shipped.cfg’s constants — and formal/runs.toml’s safety tier now records that configuration GREEN over a complete search. Measured over formal/*.cfg: the constant is TRUE in exactly one file and FALSE in 95, where it was FALSE in every one of them and TRUE in none. So the conjunct at formal/RSKeySecurityState.tla:1412 is load-bearing AND observed: the file is GREEN only because the repair closes E76, and the one-line control that deletes the conjunct’s effect — Mut_BugSeedDoesNotLead.cfg, diff a single hunk at line 48 — is RED on this very invariant. WHAT THIS DOES NOT SAY: the run answers the model’s question, not the firmware’s. 0x08BF took a different repair, and no artifact here compares the two. The counts, the depth and the clock are formal/runs.toml‘s and the results tables’ to print — this row names the configuration and not the numbers, for PLAT-MODEL-010’s reason. One arm short of a standing assumption, still: the constant is outside assurance/assumptions.toml, so the assumption gate’s both-arms rule does not reach it, and the FALSE arm is observed only through the control above rather than through that gate — unlike FixPpuatRequiresPin, whose FALSE arm Historical_E77.cfg runs. | contributor | SEC-FIDO-005 |
PLAT-CRYPTO-001 | crypto-primitive | The HMAC-SHA-256 under pinUvAuthProtocol is correct as a MAC; the harnesses replay one concrete tag and say nothing about it. | pending | rsk-crypto’s own vectors, and the soft backends the Kani rows force. A primitive’s correctness is a different obligation from the protocol’s, and this row exists so that the second does not read as the first. | contributor | SEC-FIDO-001, SEC-FIDO-003 |
PLAT-CRYPTO-002 | crypto-primitive | The RSA private operation’s secret-indexed window lookup is a LOW residual, and what makes it low is the OBSERVATION rather than the code. The nibble that picks the window is a nibble of dP/dQ; it lands in the BASE ADDRESS of a fixed-size contiguous read and nowhere else, so the instruction sequence, the operand widths and the call counts per window are the same for all sixteen values. Four command surfaces reach it — PIV GENERAL AUTHENTICATE (crates/rsk-piv/src/auth.rs, slot_key_op’s RSA arm), OpenPGP PSO:CDS (crates/rsk-openpgp/src/pso.rs, try_pso), INTERNAL AUTHENTICATE (crates/rsk-openpgp/src/internalaut.rs, try_internal_aut) and PSO:DECIPHER (crates/rsk-openpgp/src/keys.rs, rsa_decipher), all through crt::private_op — and per-operation blinding does not cover it: all three blind_pair sites randomise the BASE, and dp/dq go to the asm untouched. Nor is there a cache to carry it — both ends of the access are SRAM in the shipped image and the RP2350’s cache sits in front of QSPI flash. It is LOW and not CLOSED because reading the window sequence needs a TIME-RESOLVED observation inside one operation, and the only attacker holding one is the power/EM prober docs/threat-model.md declares out of scope; a host that can time whole operations only sees one scalar per signature, over an exponent that never changes. | accepted-risk | Two halves, and the split is what keeps this row honest. (1) The in-scope half is readable and is a contributor’s: whether any USB-visible surface hands a host a time-resolved observation inside one private operation. None does today: on all four surfaces the private operation runs to completion before any response byte leaves — slot_key_op fills its buffer and only then calls dyn_auth_resp, and the 61xx / GET RESPONSE chaining that may follow is transport-level (crates/rsk-device/src/ccid.rs) over a buffer already computed. So the host measures one end-to-end latency per operation, and the exponent is fixed for the life of the key, which makes that latency the same scalar for every signature and empty of per-window information. A response that streamed, chunked or progress-reported from inside the modexp would refute it, and so would a second observer on the same operation. (2) The silicon half is a board measurement, named here and deliberately not registered as a second maintainer-owned row: whether an RP2350 SRAM read costs a different number of cycles for a different address at all. That is unmeasured in BOTH directions, and what stands in for it is arithmetic rather than a measurement — the sixteen entries are temp + k * half with half a multiple of 32 bytes (crates/rsk-rsa/src/lib.rs, sign_crt), so every entry shares its address bits below 32 and every read is a contiguous multiple-of-32-byte run. A striped organisation whose period divides 32 bytes cannot tell the entries apart, and a bank selected by high address bits holds the whole table, which is at most 4 KiB. That bounds the mechanism; it does not measure it. WHAT RE-OPENS IT, since an accepted-risk row may carry no revalidated_by: a private-operation response a host can observe more than once (streaming, chunking, a progress indicator, an interrupt-driven partial reply); a build in which core 1 or a DMA channel runs against this modexp on a USB-reachable path, which today only keygen does (firmware/src/core1.rs takes prime-search jobs and nothing else); a measurement that an RP2350 SRAM read’s cycle count follows its address; or a change to the window table that stops the sixteen entries sharing a 32-byte-multiple stride. PLAT-BUILD-005 being taken retires the residual instead of re-opening it. | contributor | — |
PLAT-DISPLAY-001 | display | A panel update completes before the firmware treats the card as shown, and the panel’s orientation and geometry are the ones the hit test was computed for. | pending | A touch board: photograph the panel at the moment the ceremony arms, and drive each control at the coordinates the hit test claims. crates/rsk-ui’s render tests prove what the model would paint and nothing proves the panel painted it; the trusted-display properties are stated over the ceremony, not over the glass. | maintainer | SEC-DISP-001, SEC-DISP-002, SEC-DISP-003 |
PLAT-FLASH-001 | flash | The silicon’s program/erase tear behaviour under a real supply cut is the one the store model assumes: a torn write leaves the old record or a detectably bad one, never a plausible wrong one. | pending | A recorded PASS of tests/29_reset_power_cut.py on a throwaway board with a real supply cut. formal/README.md already says it in as many words: the HIL column records an OWNED test, not a claim that a board run passed. | maintainer | SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006 |
PLAT-GRANT-001 | model-abstraction | NoAccessibleSecretWithoutGate’s ghost clause is DEAD by construction in every configuration that could carry it but one: PpuatGuard is gate.ppuat /\ pin.set wherever FixPpuatRequiresPin is TRUE, so CmBeginViaPpuat — the clause’s only writer — adds the empty set by construction. | pending | A configuration in which the ghost is REACHED. formal/Historical_E77.cfg is the only one that weakens the guard (FixPpuatRequiresPin = FALSE, and grep -l finds no second), and its recorded verdict is the STRUCTURAL clause at depth 13, not the ghost: viol = {} in the final state of the counterexample. Either a configuration that keeps the producer honest and the consumer weak — BugPpuatIsAGate = FALSE with FixPpuatRequiresPin = FALSE, which formal/gen-configs.sh does not emit — or a SoloClause_*.cfg naming this clause alone, in the shape the same script already uses for the three clauses of ResetNeverWeakensSurvivingState. | contributor | SEC-FIDO-004 |
PLAT-GRANT-002 | model-abstraction | The C-tier reset bridge cannot express this property, and a field for the grant would not change that: gate.ppuat => pin.set reads the grant a platform was HANDED, and the flash holds only the record. Since 0x09CB ensure_seed writes EF_PAUTHTOKEN with no PIN behind it, so a store with the record and no EF_PIN is the factory state and the state after every completed reset — persistent_grant => pin asserted over ResetPersistentView would be falsified by correct firmware. | pending | Split it where the store splits it. The consumer half has a flash image: authorized_by_ppuat refuses a record with no EF_PIN behind it (crates/rsk-fido/src/credmgmt.rs:263-265), held by the host test a_persistent_grant_does_not_outlive_its_pin, and a harness over it needs the Ctx PLAT-MODEL-013 records Kani cannot yet build. The issuance half — no platform holds a grant with no PIN behind it — has no stored image at all and stays the model’s structural clause. crates/rsk-fido/src/reset_assurance.rs:11 still imports six FIDs without EF_PAUTHTOKEN, and adding it buys only the falsified implication above. | contributor | SEC-FIDO-004 |
PLAT-GRANT-003 | model-abstraction | FixPpuatRequiresPin’s FALSE arm is unobserved: the one configuration that takes the consumer fix out reports a verdict the producer switch alone produces, so no recorded run in this tree depends on that constant’s value. | pending | Run the arm where it can decide something. formal/Historical_E77.cfg arms BugPpuatIsAGate AND FixPpuatRequiresPin = FALSE; its counterexample is byte-identical to formal/Mut_BugPpuatIsAGate.cfg’s, which has the fix ON — measured, diff over the two recorded logs is the fingerprint line, the two timestamps and the state totals, and the 404-line trace body has the same md5. A configuration with the producer fix intact and the consumer weak, or the SoloClause_* shape of PLAT-GRANT-001, is what would make the constant answer for itself. | contributor | SEC-FIDO-004 |
PLAT-INPUT-001 | input | A PC/SC reader’s FEATURE_VERIFY_PIN_DIRECT layer carries the PIN to the card without the host seeing it, so the pinpad path spends the same retry budget the CCID path does. | pending | A run of tests/53_ccid_pinpad.py against a DISPLAY board through a real PC/SC stack — the standard build leaves bPINSupport = 0x00 and refuses PC_to_RDR_Secure, so the row cannot be answered on the default image at all. Interactive, and the emulator’s socket has no reader layer to exercise. | maintainer | SEC-LAT-002 |
PLAT-MEM-001 | memory | SRAM does not survive the drop to BOOTSEL, so a seed unwrapped in RAM is not readable through the bootloader. | discharged | TAKEN BY control ALONE, on the maintainer’s ruling of 2026-09-04, over a run of 2026-09-03. python tests/54_sram_residue.py control was driven against an image whose UF2 and ELF sha256 are both kept — assurance/board/PLAT-MEM-001-2026-09-03-control.log and assurance/board/image-2026-09-03.txt — and reproduced the 2026-08-05 outcome, tests/54_sram_residue.py:48, exactly: 4 KiB of .text byte-exact against the ELF, the whole 532480-byte dump zero at one distinct value, and the 256-byte pattern written through picoboot reading straight back. Those two are the halves assurance/board/PLAT-MEM-001.toml’s expected calls PASS, and that expected was committed before the board was powered, which is what makes this a discharge rather than a criterion fitted to a result. The second arm is RETAINED, not met: residue has no reader of its own — it calls the same check_readable and settled raises out of it ahead of the region scan, ahead of the verdict and ahead of --expect — so it is a demand on a boot configuration where SRAM SURVIVES the drop and not on a re-run of this board, and the better the platform behaves the more certainly it refuses to answer. WHAT THE NARROWED ROUTE STILL REFUSES: a mismatching .text window is a FAIL and catches the wrong image, which is the mix-up the control exists for; zeros with a write-back that does not come back are INCONCLUSIVE, the picoboot-only-answers-zeros case; a short dump is INCONCLUSIVE, because regions the verdict covers went unread; and a .data window zero over a dump that is not is INCONCLUSIVE, the partial clear that would leave the stack and the keygen heap intact. PASS needs both halves and zeros alone are not one of them. WHAT IT DOES NOT SETTLE: that worker::reboot’s scrub works. The platform cleared main SRAM, not our code, and a dump that is zero everywhere cannot tell those apart — this is a platform result about this silicon and this boot configuration, and nothing here is evidence about the firmware’s own wipe. | maintainer | SEC-FIDO-007 |
PLAT-MODEL-001 | model-abstraction | PermSets’s five subsets are a SCOPE and not a description: a host can obtain all sixteen, and the missing eleven are covered by WidePerms’s other arm rather than by the claim that they cannot arise. | pending | Two halves, and stage 2 п.7’s choice between symmetry, a wider finite domain and a separate source obligation is answered by taking the last two. (1) The domain: WidePerms = TRUE in PermWide.cfg draws ps from SUBSET Perms and checks the whole invariant set – GREEN, so the eleven reach no violation at that scope. That arm is falsifiable now rather than a pass with nothing beside it: PermWideMut_BugStopUsingKeepsPerms.cfg and PermWideMut_BugConsumeKeepsMcGa.cfg run the same widening with one defect armed each, and formal/floors.txt requires each of them RED. What the pair does not buy is that the widening is load-bearing – no switch in the roster is killed only under the wide arm, so what it says is that the arm’s observers can fail. Symmetry was not taken: ConfigGuard names "acfg" and OpGuard is called with "mc"/"ga", so a permutation of Perms is not a symmetry of this spec, and the wide arm made the question moot at a measured 493 s. (2) The alphabet: be, lbw and pcmr are not elements of Perms at all and the 0x09/0x06 admission rules over them are cross-bit, so no widening of a four-element Perms can express them – that half is a source obligation, the exhaustive 512-case sweep in crates/rsk-fido/src/clientpin_perms_tests.rs, which also measured the 48 cases where the shipped path and CTAP 2.1 §6.5.5.7.2 disagree. | contributor | SEC-FIDO-001, SEC-FIDO-003, SEC-FIDO-004 |
PLAT-MODEL-002 | model-abstraction | One credential per relying party is enough to carry the authorization and management properties; the shipped cardinality is MAX_RESIDENT_CREDENTIALS. | pending | The store slice of stage 5, which is where a cardinality argument can be made rather than assumed. | contributor | SEC-FIDO-001, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A |
PLAT-MODEL-003 | model-abstraction | The model’s ram is FidoState::keydev_dec.is_some() and nothing else in the tree is a second copy of the seed the model would have to see. | pending | A recorded session that performs a vendor UNLOCK. The projection is written once — crates/rsk-device/src/ctap.rs maps the field into keydev_ram_raw, and formal/TraceSecurity.tla’s R4aRawRefinesB equates it with ram at every boundary — so the comparison exists; what is missing is a session in which it is ever TRUE. Measured: keydev_ram_raw is false in all 40 pre and all 40 post snapshots of formal/traces/security-phase4.jsonl, so the true arm has never run. | contributor | SEC-FIDO-007, SEC-TRACE-001 |
PLAT-MODEL-004 | model-abstraction | One store.seed boolean stands for two flash records, so the soft-locked device — EF_KEY_DEV_ENC present, EF_KEY_DEV gone — is a state the seed invariants cannot tell from an unlocked one. | pending | A second model variable, or a proof that the collapse preserves the invariants that read it. The code keeps the two apart already: crates/rsk-fido/src/seed.rs defines the lock as exactly has_key(EF_KEY_DEV_ENC) && !has_key(EF_KEY_DEV), and crates/rsk-fido/src/reset_assurance.rs carries owner_seed and owner_locked_seed as separate fields; formal/TraceSecurity.tla is where they merge. | contributor | SEC-FIDO-007, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006C |
PLAT-MODEL-005 | model-abstraction | DeviceUnlock’s store.seed conjunct is what makes RamNeverOutlivesFlashSeed true, and the production unlock has no such conjunct — it gates on mse_ready, a 32-byte lock key and lock_engaged, which requires the PLAIN record ABSENT. | pending | A boolean model constant pinning the conjunct, emitted both ways by formal/gen-configs.sh — the shape AlwaysUvShipped already has — after which this row moves to assurance/assumptions.toml and stops being one of these. It is the only row of this set that could join the first registry, and the obstacle is writing the constant, not the gate. By construction the FALSE arm goes RED: Idle and no flash seed and no RAM copy is reachable through ResetAborts once ResetSweepSecrets has deleted the record. | contributor | SEC-FIDO-007 |
PLAT-MODEL-006 | model-abstraction | RamNeverOutlivesFlashSeed is INERT on the shipped configuration: it has no falsifying reachable state by construction, so its GREEN carries no information beyond PLAT-MODEL-005’s guard. | pending | Not by a run — by a second reset producer. formal/README.md records the measurement: dropping SeedReachable’s ram disjunct leaves the state set identical and flips no verdict, and two of the three ram' = FALSE assignments are dead. The page names what would make it bite — Fs::factory_wipe, the second reset path, still unmodelled — if its reboot were ever separated from the wipe. | contributor | SEC-FIDO-004, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-007 |
PLAT-MODEL-007 | model-abstraction | The C-tier reset bridge cannot be reused as bounded evidence for the seed-ordering invariant: it is deliberately WIDER and admits the state the invariant forbids. | pending | Either a conjunct added to crates/rsk-fido/src/reset_assurance.rs’s well_formed — which changes what the four SEC-FIDO-006 harnesses prove and is stage 4’s call — or a harness of this property’s own. Today well_formed constrains volatile.owner_seed only while a reset is in progress, and crates/rsk-fido/src/reset_refinement_kani.rs draws it as a free kani::any() beside an equally free persistent seed, so all four harnesses run over states where the RAM copy outlives the flash record. | contributor | SEC-FIDO-007, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C |
PLAT-MODEL-008 | model-abstraction | DeviceUnlock is WIDER than the firmware in two directions and both are sound: the model has no device lock, so it does not require the seed to be stored WRAPPED — only a locked device has an EF_KEY_DEV_ENC to open — and it omits AUT_DISABLE, which only ever CLEARS the RAM copy. | accepted-risk | Nothing to run: a wider action reaches a superset of states, so a safety invariant proved over the model holds of the firmware, and the omitted action removes only a way for the copy to disappear. What this row buys is not a discharge but a READER: the argument lived in a comment above the action in formal/RSKeySecurityState.tla, where no gate sees it, and stage 2 п.3 asks exactly for the move. It stops being sound the moment a LIVENESS or coverage claim is made over the same action, which is why the failure direction below is not none. | contributor | SEC-FIDO-001, SEC-FIDO-004, SEC-FIDO-006, SEC-FIDO-007, SEC-FIDO-L01 |
PLAT-MODEL-009 | model-abstraction | EF_MINPINLEN’s FLOOR (byte 0) and its RP-id disclosure list (bytes 2..) are outside RSKeySecurityState because neither can admit an operation: the floor is read only where a NEW PIN verifier is written and by setMinPINLength’s own monotonic guard, and the list is read only to disclose the floor to a listed RP. A floor that reads too low stores a weaker PIN of the owner’s own choosing; it never authorizes a request. Byte 1, forceChangePin, is NOT covered by this argument — it refuses token issuance after a correct PIN, and belongs in the model. | pending | A source audit of the EF_MINPINLEN read sites, re-run when one is added: git grep -n 'min_pin_length\|current_min_pin\|rp_min_pin_len\|EF_MINPINLEN' -- crates, checking that no new site sits on a grant path. The argument holds per BYTE, so a reader of byte 1 is a different question and this row does not cover it. | contributor | SEC-FIDO-001, SEC-FIDO-003, SEC-FIDO-006, SEC-FIDO-006B |
PLAT-MODEL-010 | model-abstraction | EF_MINPINLEN’s forceChangePin byte IS a gate: clientpin.rs refuses getPinToken with PinInvalid and both permissions-based doors with PinPolicyViolation when it is set, AFTER the PIN has verified. PinAttemptEnabled and PinAttemptPolicy carried three conjuncts where the code has four, so a defect that waives the pending change was a live token the model could not see — and one has shipped (bcd 0x09AE). | discharged | Modelled, and THREE of the four sentences the route this replaces wrote were wrong — each found by review, none by a gate. gate.forceChange is set by ConfigOp (config.rs:483 refuses it without a PIN) and cleared by changePIN. It is NOT cleared by setPIN: store_new_pin (clientpin.rs:945-969) touches no EF_MINPINLEN byte, and the route’s cleared by both PIN writes (store_new_pin, clientpin.rs:1260) was wrong twice over — :1260 is inside store_local_pin, the panel flow, which this module has no action for. Setting the flag also ENDS the session token and the persistent grant (config.rs:500-503); the first model had them UNCHANGED, which is the shipped tree carrying its own defect at the third of three sibling sites. The route also promised the code twin already exists in the suite; it did not, and was built here (formal/comutants.toml [BugForceChangeIgnored], phase2_count 30 -> 31) and killed. What held: BugForceChangeIgnored drops the guard and goes RED on NoAuthorizationBypass at depth 8 in both configurations, and the counterexample is a token ISSUED over a standing gate, not a refusal wearing another code. ForceChange.cfg is GREEN, and its states, distinct count and depth are the results table’s to print — this row names the configuration and not the numbers, because a hand-typed copy of a generated count is the one thing this registry cannot keep true. | contributor | SEC-FIDO-001, SEC-FIDO-003, SEC-FIDO-004 |
PLAT-MODEL-011 | model-abstraction | EF_DEVICE_PIN is outside RSKeySecurityState because the SURFACE it gates is outside it, not because it is inert. It carries a second independent persistent retry ladder, and its host-visible reader is the PIN half of the vendor seed-export / attestation / audit gate — and neither that gate, the MSE channel, nor its EF_PIN half is modelled. For the RESET family the omission is sound on its own: it is a phase-2 gate record, phase 2 cannot begin until phase 1 has provably emptied the store, and the seed leads phase 1, so no prefix that drops it leaves a secret it could have gated. | pending | Model the vendor gate itself — MSE readiness plus the two-armed PIN factor — as a stage-4 action; EF_DEVICE_PIN then enters as one Boolean inside it, and its ladder can wait for a mutant that needs it. Until then this is an open scope obligation, not a proof. | contributor | SEC-FIDO-004, SEC-FIDO-006C |
PLAT-MODEL-012 | model-abstraction | gate.ppuatStale has no counterpart in the firmware. The model carries the persistent grant as THREE booleans — gate.ppuatRec (EF_PAUTHTOKEN exists), gate.ppuat (a platform was handed it, a fact about the ceremony and not a record) and gate.ppuatStale (it was handed out and is no longer honoured) — and the last state is one no shipped code path can produce: clear_ppuat (crates/rsk-fido/src/seed.rs:337) is a force_delete of the record, so the code has present-and-live or absent, and nothing between. ppuatStale exists so that a MUTANT can build the state the invariant forbids. | pending | Nothing to run, and that is the point of registering it: the third conjunct of NoTokenAfterInvalidation (~(gate.ppuat /\ gate.ppuatStale)) is UNFALSIFIABLE on the shipped tree by construction, exactly as RamNeverOutlivesFlashSeed is for SEC-FIDO-007 (PLAT-MODEL-006). What would settle it is a second EF_PAUTHTOKEN writer that could leave a stranded record — Fs::force_delete returning an error the caller drops would be one — measured against the four clear_ppuat call sites. | contributor | SEC-FIDO-003 |
PLAT-MODEL-013 | model-abstraction | The two Kani harnesses named for this property cover the SESSION token only. crates/rsk-fido/src/state_kani.rs::no_token_after_invalidation and credmgmt_kani.rs::no_token_after_invalidation_at_call_site drive FidoState in RAM; the persistent pcmr grant lives in EF_PAUTHTOKEN, needs a Ctx with flash behind it, and both harness headers say so in as many words. So the second conjunct of the invariant is bounded-proved and the first and third are not. | pending | A harness over clear_ppuat and write_pin_verifier with a Ctx, which is the p256-in-the-reachable-set problem credmgmt_kani.rs’s own header records: Kani 0.67.0 aborts in codegen on crypto-bigint 0.7.5 UintRef::lowest_u64. Until that is answered the persistent half is held by host tests (crates/rsk-fido/src/clientpin_tests.rs:2055 and its neighbours) and by the model, not by a proof. | contributor | SEC-FIDO-003 |
PLAT-MODEL-014 | model-abstraction | The relational pre-state this property compares against is a GHOST in both tiers — snap in RSKeySecurityState and ResetSnapshot in crates/rsk-fido/src/reset_assurance.rs — and no shipped image holds it. So nothing in the firmware can observe, let alone enforce, the property at runtime: the write ORDER is the whole implementation, and a device that had reordered its phases would answer every command exactly as one that had not. | accepted-risk | Nothing to run, and that is the content. What supports the claim is the other direction: scripts/check.sh:199-248 (assurance-trace image identity) builds the default image twice, poisoning reset_assurance.rs and reset_refinement_kani.rs before the second, and requires the two loadable images to be byte-identical — so the abstraction is provably absent from every firmware, which is why it cannot also be the enforcement. A discharge would be a runtime check the device could fail closed on, and none is proposed: the ordering IS the mechanism. | contributor | SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C |
PLAT-MODEL-015 | model-abstraction | RSKeyBootHardening treats the lazy re-key as ATOMIC in thirteen of its fifteen configurations. LazyRekey writes the re-keyed record and re-arms request_rescrub in one step, so the ORDER of the two flash appends is not represented and no defect in it is visible to those thirteen rows. The firmware makes two separate appends, and a reset between them leaves EF_HARDENED set over a superseded copy. | pending | The two Historical_Boot* rows, once a recorded tier run holds them: RekeyOrderModelled = TRUE splits the action into RekeyBegin/RekeyFinish and BugRecordWriteBeforeRearm picks the order, so the write-then-rearm arm is expectedly RED on MarkerNeverLies and the rearm-then-write arm GREEN. Until formal/runs.toml records both, the split is observed only by hand-run single configurations, which is why this row is pending rather than discharged. What it will still NOT say: the thirteen atomic rows stay atomic on purpose — they are where every other boot property is checked, and pinning rekeying to {FALSE} there is what keeps their state spaces comparable to the recorded ones. | contributor | SEC-BOOT-001 |
PLAT-ORACLE-001 | model-abstraction | Below the model tier nothing can report ResetKeepsThePinGate rather than ResetKeepsTheAlwaysUvGate: fuzz/fuzz_targets/power_cut.rs:202 folds both gates into one conjunct (fs.has_data(EF_PIN) && fs.has_data(EF_ALWAYS_UV)) and tests/29_reset_power_cut.py:527-530 asserts one refused assertion for both, so a red run on either rung says a gate went and not which one. | pending | Splitting either oracle: a second boolean in reset_property_holds, or a second assertion in tests/29_reset_power_cut.py reading getInfo’s options.alwaysUv — which the script already fetches and prints in its failure message but does not test. Both are small; neither has been done. Both files NAME all three clauses in their doc comments, and the columns are not wrong — assurance_gate counts FILES — which is why nothing in the apparatus reports the gap. The backup-seal clause is separable on both rungs and is the sibling this does not cover. | contributor | SEC-FIDO-006A, SEC-FIDO-006B |
PLAT-OTP-001 | otp | OTP read permissions, lock state and the chaffing layout behave as the datasheet describes across a partial MKEK provisioning, so a half-written fuse row is refused rather than read as a key. | pending | A fuse-burning procedure this tree does not have. tests/90_otp_mkek_migration.py deliberately validates the migration WITHOUT touching a fuse, on a FAKE_MKEK/FAKE_DEVK build, so it exercises the kbase path and not the read-permission, lock-state or chaffing behaviour this row is about. Irreversible by construction — AGENTS.md puts fuse writes with the maintainer and nowhere else. | maintainer | — |
PLAT-PINGATE-001 | tool-fidelity | SEC-FIDO-006A’s only bounded evidence carries a non-vacuity guard that does not guard the conjunct it omits: reset_keeps_the_pin_gate’s kani::cover! names three of the clause’s four antecedent conjuncts and puts the clause’s CONSEQUENT where snapshot.credential belongs, so a witness it accepts may be a state at which the clause holds vacuously. | pending | One conjunct in crates/rsk-fido/src/reset_refinement_kani.rs:133-138, and it was priced by measurement rather than argued. Driven on a scratch copy of the workspace with cargo-kani 0.67.0: the shipped condition conjoined with !reset.snapshot.credential is SATISFIED (1.08 s), which is the defect; conjoined with reset.snapshot.credential instead it is SATISFIED at 0.98 s against a 0.99 s baseline, which is the repair at no cost. The guard is not inert — under a real vacuity mutation, both credential draws forced false, the shipped condition goes UNSATISFIABLE (0.94 s) — so what it misses is the route through the snapshot draw alone. crates/rsk-fido/src/reset_assurance.rs:144-151 is why the two routes differ: begin is the only writer of snapshot.credential and takes it from persistent.credential. The sibling harnesses at :142 and :162 have the SAME shape and were not driven. | contributor | SEC-FIDO-006A |
PLAT-PINGATE-002 | model-abstraction | SEC-FIDO-006A’s isolated RED is a localisation and not a demonstration of unique reach: its falsifying state also falsifies NoAccessibleSecretWithoutGate, and the two properties share one model switch and one production function. | pending | A configuration or a witness exhibiting a state where this clause falls and NoAccessibleSecretWithoutGate holds, and the recorded tier contains none. Measured: SoloClause_ResetKeepsThePinGate.cfg’s State 16 has store.cred = {r1}, SeedReachable, pin.everSet TRUE and pin.set FALSE, so formal/RSKeySecurityState.tla:1796 is false there too; assurance_gate.co_refuted credits BugResetGatesFirst to both names; and the two Refines tags sit at crates/rsk-fido/src/reset.rs:227 and :245, on is_fido_gate_fid and the is_fido_gate_record it wraps. The converse IS witnessed — Solo_NoAccessibleSecretWithoutGate.cfg falls on the stranded-grant conjunct at formal/RSKeySecurityState.tla:1807 where snap.surv is empty and this clause is vacuous — so the pair is asymmetric rather than redundant. What would settle it is a switch that breaks the snapshot comparison without touching the steady-state ghost everSet, and the model has none. | contributor | SEC-FIDO-006A, SEC-FIDO-004 |
PLAT-PRES-001 | model-abstraction | Owners — the four SCOPE_* bytes plus Panel, the model-only split of SCOPE_NONE — is the whole domain a presence decision can be produced for or applied to, so a wait owner outside those five does not exist. | pending | Reading the byte and its writers. crates/rsk-device/src/presence.rs:26-32 defines exactly four SCOPE_* constants and firmware/src/worker.rs:434, :528, :663, :665 are every set_wait_scope call site in the tree; formal/RSKeySecurityState.tla:127-144 maps them and splits SCOPE_NONE into NoOwner and Panel because request_cancel refuses in both while only one can be ENDED by a touch. What would falsify it is a fifth interface that opens a wait: the byte is a u8, nothing bounds it, and a new transport arrives as an owner no configuration and no harness checks. | contributor | SEC-FIDO-002 |
PLAT-PRES-002 | model-abstraction | No API in the tree can originate a cancel from SCOPE_CCID or from an on-panel flow, so a CCID or panel ceremony is uncancellable by ABSENCE of a producer rather than by a guard anything checks. | pending | A whole-tree measurement, and it is a grep rather than a proof: git grep -n 'cancel_requested.store(true' is exactly two sites, crates/rsk-device/src/presence.rs:120 (request_cancel, gated on SCOPE_FIDO) and :131 (cancel_otp_wait, gated on SCOPE_OTP), and the only other writer is set_cancel_requested, whose six production call sites (crates/rsk-device/src/presence.rs:196, :233 and crates/rsk-display/src/pin.rs:317, :441 + crates/rsk-display/src/presence.rs:47, :58) all pass a literal false, the two cfg(feature = "display") forwarders at firmware/src/presence.rs:269 and firmware/src/display.rs:198 reaching only those; the one site that passes true is crates/rsk-device/src/presence_kani.rs:158, a harness. The Kani cancel harness rests on this: board.attempted[SCOPE_CCID] stays false because the harness raises only the two cancels that exist, so ‘a CCID wait cannot be cancelled at all’ is the harness’s construction and not its conclusion. A third writer added anywhere in the tree falsifies it with every harness still green. | contributor | SEC-FIDO-002 |
PLAT-PRES-003 | model-abstraction | NoCrossTransportTouchConsumption’s structural conjunct — (pres.granted = "cancel") => (pres.cancelBy = pres.scope) — is INERT on the current module: no reachable state falsifies it that TouchCancel’s ghost write has not already marked in the same step. | pending | A configuration that checks the conjunct alone, which the tree already has a family for (formal/SoloClause_*.cfg, three of them today) — or the module changing. ARGUED FROM THE MODULE TEXT AND NOT RUN: TouchCancel (formal/RSKeySecurityState.tla:444-455) sets granted = "cancel" and writes viol in the same step; every other writer of pres either requires WaitOpen (granted = "none"), or is ClosedWait/OpenWaitFor/VolatileCleared, all of which set granted back to "none"; and viol is only ever grown. So the conjunct’s arm can be reached by nothing the ghost has not already caught. It is a backstop for a producer that does not exist yet, which is the same shape as an assumption constant nothing branches on. | contributor | SEC-FIDO-002 |
PLAT-RESET-001 | reset | A real RP2350 power-on reset clears WATCHDOG.scratch2, so the PIN soft-lock the previous cycle recorded does not ride through it. | pending | A board measurement: write a known value to WATCHDOG.scratch2, cut power at the supply — not a warm reset, because firmware/src/pin_lock.rs writes the word on every CBOR dispatch, so the read must come from the first boot after — and read it back. tests/54_sram_residue.py is the shape; the register is not SRAM, so it needs its own probe. | maintainer | SEC-BOOT-002 |
PLAT-ROM-001 | boot-rom | M7-Q2: the boot ROM’s BOOTSEL return path leaves WATCHDOG.scratch2 as the firmware left it, so a drop to the bootloader is not a way to shed the soft lock. | pending | A board measurement on the same rig as PLAT-RESET-001, with the vendor applet’s reboot-to-BOOTSEL in place of the supply cut, and the read taken on the boot after the bootloader is left. No datasheet clause states it either way; a vendor erratum would settle it as well. | maintainer | SEC-BOOT-002 |
PLAT-ROM-002 | boot-rom | The vendor applet’s reboot really reaches the bootloader: tests/51_secure_reboot.py has no runner in this tree, because the emulator has no bootloader to fall into. | discharged | TAKEN on 2026-09-03, and the reading is deliberately not the script’s. tests/51_secure_reboot.py --bootsel ran against a no-touch board — the plain run drives P1=0x00, the warm reset, and only --bootsel takes the P1=0x01 path this row is about — and exited 0 over SELECT vendor AID -> 9000 and REBOOT (P1=0x01) -> 9000. That is not the discharge: its last line reads secure-reboot PASS (BOOTSEL requested), and a request is not an arrival — the same line would print over a warm reset, which is the FAIL this row names. What settles it is the host afterwards, read separately and captured under assurance/board/: the device re-enumerated as the RP2350 mass-storage bootloader, its drive mounted, and the PC/SC reader list came back empty, so the CCID interface is gone. Both halves, because expected names the drive and the interface, and it is the interface half that rules out the warm reset. The board was re-dragged with a UF2 afterwards, which is why the run wants a throwaway board and not the provisioned one. | maintainer | SEC-ADM-001 |
PLAT-SEAL-001 | model-abstraction | EF_BACKUP_SEALED is one byte on flash and every tier models it as one boolean, so a marker that is present but unreadable — a third state the runtime reader has and the model does not — cannot be described by any configuration, harness or twin. | pending | Either a second model variable, or the argument that the byte’s VALUE is never read. The second is nearly available and is not the same claim: every consumer tests presence rather than content (crates/rsk-fido/src/vendor.rs:1045 and the display side’s has_data), and both writers write the same one byte. What is left over is the read that FAILS, which crates/rsk-fido/src/vendor.rs:1035 deliberately answers true for because the absent arm hands out the master seed — and which the model has no state for at all. PLAT-FLASH-001 assumes that state away at the medium; this row says the model could not describe it if it happened. | contributor | SEC-FIDO-006C |
PLAT-SEAL-002 | tool-fidelity | This clause’s model verdict and its co-refutation credit both come from a configuration arming a PAIR of switches — BugBackupSealedNotAGate with its companion BugSeedDoesNotLead — so what the clause-isolating configuration isolates is the CLAUSE and never the defect. | pending | A recorded run of the switch armed alone, which no configuration in formal/ performs. The model text says it would be GREEN and the argument is derivable: the demoted marker’s disjunct in ResetSweepSecrets is guarded by SeedLeadsTheWipe => ~store.seed, the only clearer of store.seed assigns snap' = KeepSurv(snap, ram), and KeepSurv at formal/RSKeySecurityState.tla:315-316 retires snap.seed whenever ram is FALSE — which it is from ResetConfirmed onward wherever BugStateResetAfterWipe is off. But that is an argument about the model and not a verdict, and comutate.armed_subject accepts the pair on a NAME lookup in gen-configs.sh’s companion_bug rather than on it. A recorded GREEN of the switch alone would discharge this and make the argument checkable at the same time. | contributor | SEC-FIDO-006C |
PLAT-SEAL-003 | model-abstraction | The TLA+ clause and its Rust abstraction do not state the same sentence: formal/RSKeySecurityState.tla:1867-1868 has no reachability conjunct in the antecedent, and crates/rsk-fido/src/reset_assurance.rs:122-128 adds owner_seed_reachable, which makes the Rust statement strictly weaker. The two sibling clauses carry that conjunct on both sides and have no such gap. | pending | Either the conjunct added to the model’s clause or the disjunct removed from the abstraction — and the direction says which way the gap is safe. The model’s clause is the STRONGER of the two, so its GREEN carries to the abstraction and the harness proves less than the configurations do. That is sound for citing them together and unsound for reading the bounded row as an independent confirmation of the model one, which is what a kani column of one invites. Removing the disjunct changes what the harness proves and is stage 4’s call. | contributor | SEC-FIDO-006C |
PLAT-SEAL-004 | build-configuration | The shipped image is built without --features fips-profile. On that build backup_export returns NotAllowed before the seal is ever read, so one of this clause’s two consumers is gone and the property guards a surface that column does not have. | pending | Reading the cfg arms, and the reading is the content rather than a run: crates/rsk-fido/src/vendor.rs:842-845 refuses export under cfg!(feature = "fips-profile") ahead of the seal check, and the on-device recovery-phrase reveal is disabled on that profile too. The direction is unusual and worth stating: the property is WEAKER there, not stronger, because a torn reset that drops the marker re-opens nothing over USB — so a GREEN measured on the default column is not evidence about that one. No configuration and no harness runs it. | contributor | SEC-FIDO-006C |
PLAT-SEAL-005 | build-configuration | The marker’s SECOND consumer — the on-device recovery-phrase reveal at crates/rsk-display/src/backup.rs:47 — exists only on a display build, so on that column this clause guards two disclosure surfaces and every rung of its ladder checks it as if it guarded one. | pending | The display columns of the assurance matrix, which are not covered for this property. crates/rsk-display/src/backup.rs:47 conjoins !st.sealed into can_reveal; formal/RSKeySecurityState.tla has one gate.backupSealed and no consumer at all; fuzz/fuzz_targets/power_cut.rs tests one record’s presence; and tests/29_reset_power_cut.py drives the host path only. The uncovered surface is not the marginal one — the reveal is the case where the host is outside the trust path entirely, which is what docs/threat-model.md’s seed-backup clause exists for. | contributor | SEC-FIDO-006C |
PLAT-SOURCE-001 | model-abstraction | The revoke-before-write ORDER that the first conjunct of NoTokenAfterInvalidation is about is owned by ONE function, write_pin_verifier (crates/rsk-fido/src/clientpin.rs:831), which clears the grant at :840-842 before fs.put at :852. The two functions the tree tags as this property’s owners — set_pin (:175) and change_pin (:229) — hold a redundant OUTER clear_ppuat, and formal/comutants.toml [comutant.BugSetPinKeepsPpuat] records that deleting set_pin’s left all 668 rsk-fido tests green over three runs. | pending | A Refines RSKeySecurityState!NoTokenAfterInvalidation — SEC-FIDO-003 tag on write_pin_verifier, and the review of the third caller store_local_pin (clientpin.rs:1256) and the device-PIN caller (:1287) that a tag there forces. NOT a column move: clientpin.rs is already one of the three files assurance_gate.grep_word counts, so rust stays 3 and no gate reddens for the absence — which is why this is a registry row and not a gate rule. | contributor | SEC-FIDO-003 |
PLAT-SOURCE-002 | model-abstraction | Three of the citations that carry this property’s model-to-code bridge name code the surrounding prose is not about, and scripts/citation_gate.py is GREEN over all three: formal/RSKeySecurityState.tla:65 cites state.rs:584-599 for stopUsingPinUvAuthToken and that span is retire_sequences_except; formal/README.md:99 cites seed.rs:323-324 for clear_ppuat and that span is the last two lines of the function ABOVE it; and the bare :300-304, written three times at formal/RSKeySecurityState.tla:89, formal/RSKeySecurityState.tla:829 and formal/RSKeySecurityState.tla:1772, is four lines short of the clear_ppuat call it is cited for AND is matched by no rule of the gate, because the module writes it without the backticks CITE’s continuation alternative requires — measured by running citation_gate.citations over the module, which returns none of the three. | pending | Re-point the three and re-lock. The measurements behind them, so the fix is checkable: state.rs:584-599 WAS exactly stop_using_token at commit 250be31 and the function is at :547-562 today; :300-304 WAS the §6.5.5.6-step-15 comment through clear_ppuat(ctx.fs) at commit c9bdc5b and that block is at :305-309 today, which is the span formal/README.md already uses for the same claim; and seed.rs:323-324 was r.map(|()| tok) and } at 5e3abef, the commit that INTRODUCED it, so it has never named clear_ppuat. | contributor | SEC-FIDO-003 |
PLAT-STORE-001 | model-abstraction | The tear guarantee PLAT-FLASH-001 makes about the silicon holds one layer up too, in the KV library: a torn append or remove leaves the old record or a detectably bad one, never a plausible wrong one. This is a property of the VENDORED FORK, not of sequential-storage 8.0.0. | pending | Two things, and neither is in the tree. First a recorded verdict for fuzz/fuzz_targets/kv_durability.rs, the target that FOUND the upstream defect: third_party/sequential-storage.patch item 3 records that upstream’s remove_item_inner erased pages from find_first_page(PartialOpen).unwrap_or_default(), which falls back to page 0 in the normal steady state of a closed frontier page plus an open buffer page. That inverted the oldest-first erase order, so a power cut mid-remove erased the NEWEST copy first and left an OLDER copy live, which fetch_item then returned — exactly the plausible wrong one PLAT-FLASH-001 rules out, false in the library until this fork fixed it, and no board run of tests/29_reset_power_cut.py could have discharged it because the defect sits ABOVE the medium. Second a rule that the fork is what actually builds: [patch.crates-io] is wired in three manifests (Cargo.toml:177, fuzz/Cargo.toml:443, tools/emu/Cargo.toml:84) and nothing holds the three together, so a workspace that missed one would link upstream 8.0.0 with the defect back and every host test still green. | contributor | SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006 |
PLAT-STORE-002 | model-abstraction | The backend’s enumeration-completeness flag is honest: for_each_key answering complete means every committed key was yielded, which is what lets Fs::scan decide the whole FID space and read a cold absence O(1) instead of probing for it. | pending | A test driving a SELECTIVE, single-page read fault at the Storage seam and asserting for_each_key answers false. The UNCONDITIONAL case is already covered and an earlier draft of this row said it was not: crates/rsk-store/src/tests.rs:395-404 a_faulted_walk_reports_itself_incomplete mounts a store, writes a live key, sets fail_reads and asserts the walk answers false; it predates this row and scripts/check.sh:514 runs it on every gate. What that test cannot reach is the shape the defect had. The mock says so itself at crates/rsk-store/src/tests.rs:59-62: fail_reads fails every read unconditionally and for every address — which no torn write produces, so it stands for a chip or bus fault, and a walk whose FIRST read fails is refused before it can report a truncated set as complete. Item 2 of third_party/sequential-storage.patch is the other shape: upstream’s page-advance loop swallowed a page-state Err via _ => continue, so ONE unreadable page mid-ring was skipped and the walk still reached the None terminator and reported complete. Only a fault that answers for one address and not the rest distinguishes the fork from upstream, and no test in this tree can pose one. The claim itself is stated only in two COMMENTS, crates/rsk-fs/src/fs.rs:100-106 and crates/rsk-fs/src/fs.rs:295-302, each arguing it from the backend’s internals rather than from anything that runs. The fork tells Corrupted (a fully-migrated source, safe to skip) from a genuine read fault and aborts on the second — so the guarantee is the FORK’s, which is what PLAT-STORE-001 carries. crates/rsk-store/src/lib.rs:179-181 ANDs the two partitions’ walks, so the flag is only ever as honest as the weaker ring. | contributor | SEC-STORE-002 |
PLAT-STORE-003 | model-abstraction | GIVEN a medium that tears the way PLAT-FLASH-001 asserts, a reboot recovers the committed store: after any number of power cuts every key whose write or remove returned cleanly reads back exactly, and only the operation the cut interrupted is ambiguous — its old value or its new one, never a third older one. The GIVEN is the whole narrowing and it is what makes this row dischargeable by a mock; the medium half is PLAT-FLASH-001’s and is not restated here. firmware/src/main.rs:555 runs Fs::scan once at boot, and every later absence answer is that one walk’s. | pending | A run record naming a verdict, which is the half that does not exist. The CONTRACT is asserted already: fuzz/fuzz_targets/kv_durability.rs states it in as many words in its header and drives one MapStorage partition directly, and fuzz/fuzz_targets/power_cut.rs torments the whole rsk-fs stack over the same power-cuttable mock. Both are on the weekly roster — scripts/fuzz-all.sh:41 takes it from cargo fuzz list rather than a hand-written table, so neither can silently fall off it. What nothing does is READ those verdicts: kv_durability appears in no workflow, no docs page, no script and no assurance file, so its result is a green shard nothing cites. Why this row is model-abstraction and not flash, decided by measurement rather than by taxonomy: the class is the whole difference between a discharge that must name silicon and one that need not. Marked discharged with evidence = ["fuzz/fuzz_targets/kv_durability.rs"] this row is exit 0 under model-abstraction and exit 1 under flash — PLAT-STORE-003: a flash discharge records no 'board_revision'. As the statement stood before the GIVEN, flash was the honest class and the row was mis-classed. Narrowing the statement is the better repair: classing it flash would oblige a stepping for a defect that sits ABOVE the medium, which is exactly the mistake PLAT-STORE-001 exists to undo — a software question parked behind hardware that cannot answer it — and this row’s discharge_owner is contributor, who under AGENTS.md may not produce a board revision at all. What the narrowing does NOT buy, in the reading this row carried until the hole was closed: model-abstraction accepted any path that existed, so evidence = ["README.md"] on this row was also exit 0, measured. That half is now check_evidence’s PROSE_PAGE rule and it belongs to every row of the class rather than to this one: a .md that no generator both CLAIMS and MARKS is refused as evidence anywhere in the registry, whatever its case, and so is a directory and any spelling git’s listing does not have — docs, README.MD, and a generator-claimed page with its own header line deleted, were each exit 0 after the rule’s first version, measured. So is a page rendered FROM this registry, which that version admitted through its own carve-out: evidence = ["docs/platform-assumptions.md"] on this row was exit 0 while that page prints this row’s discharge verbatim. What the rule still does not buy is relevance: an artifact of legal shape and no bearing on the claim, deny.toml, is exit 0 on this row today, measured, and only a reader stops that. Nor does it stop a *_gate.py DECLARING a page it does not write, because nothing here runs a generator — that move now costs a second edit, since the page must carry the marker too. | contributor | SEC-STORE-001, SEC-STORE-002 |
PLAT-STORE-004 | model-abstraction | is_counter_fid is a correct routing table over every FID the firmware persists: a record is read back from the partition it was written to, and the counter/main split never leaves a live FID on the other side. | pending | A derivation reading the FID constants out of the applet crates and holding them against the table, which scripts/partition_routing_gate.py is: it takes the constant NAMES out of the doc comment over is_counter_fid, resolves each to a const … : u16 in a crate that is not rsk-store, and holds all four copies to the values that come back. What it does NOT settle is this row’s statement, and that is why the status has not moved: the ROSTER is that doc comment, so a hot record declared at its home and named nowhere over the table derives nothing and no copy is measured against it — over every FID the firmware persists stays a judgement rsk-store makes and a reader checks. Before that row existed: crates/rsk-store/src/lib.rs:88 is a hand-written matches! over four bare literals (0xC000, 0xC001, 0x0093, 0xCC01) whose named homes are in other crates: EF_COUNTER at crates/rsk-fido/src/consts.rs:333 and EF_CRED_CTR at crates/rsk-fido/src/consts.rs:340. Table and constants therefore drift without a compile error, and the set HAS moved once — EF_CRED_CTR joined it at 0x0821 after 0x081D had been writing that FID to main. crates/rsk-store/src/lib.rs:145-152 records what the resulting state costs: a copy in the wrong partition is invisible to read yet yielded by every for_each_key, so authenticatorReset’s sweep loops on it until its progress bound gives up. FOUR hand-written copies of the set, not two, and an earlier draft of this row missed the one that matters. git grep -l is_counter_fid reaches nine files — this registry and its generated page, assurance/crates.toml, CHANGELOG.md, docs/assurance-vector.md, formal/README.md, the two rsk-store sources, and fuzz/fuzz_targets/power_cut.rs. That last one is the fourth copy: fuzz/fuzz_targets/power_cut.rs:76-78 spells the same four literals into a FIDS array, and its own comment at :67-75 records that the set has ALREADY drifted there twice — the mirror it replaced listed three of the four and missed EF_CRED_CTR (0xC001, rewritten on every getAssertion), and the selector was & 7 over nine entries, so 0xCC01 could never be written by any input while the sweep asserted it absent on every one. A whole partition routing was in the roster and out of the fuzzer’s reach. So this row’s subject is not hypothetical drift; it is drift that has happened twice in the copy the row was written without. What holds the table today is crates/rsk-store/src/tests.rs:244-264, which lists the same four numbers a third time and would move WITH a wrong edit — and which names the power_cut miss at :250-251, so the two copies that drifted are the two nothing derives. | contributor | SEC-STORE-002 |
PLAT-THREAT-001 | threat-model | A CTAPHID channel id is a routing label the sender writes, so channel ownership is a scoping rule and never an authentication one. | pending | A clause in docs/threat-model.md, which assurance/threat_clauses.toml would then derive. crates/rsk-fido/src/state.rs states it in prose beside the walk owner today, which is the wrong place for a threat-model premise. | contributor | SEC-FIDO-001, SEC-FIDO-002, SEC-TRANS-001 |
PLAT-THREAT-002 | threat-model | A PIN-derived record stays rooted in the public chip serial until its own reference is PRESENTED after the burn. The boot passes move every record sealed under the key base alone; re-keying a PIN-derived one needs the secret, so it happens in check_pin’s fallback (crates/rsk-openpgp/src/pin.rs:277). PW1 is presented by ordinary use; PW3 gates only the admin surface and may not be presented again after provisioning, and an OpenPGP resetting code may never be. Until then a flash dump plus the public serial opens the DEK copy behind that reference — every OpenPGP private key and the AES key with them — and a PW3 still on its published default needs no search at all. PIV’s PUK is the same shape one crate over (crates/rsk-piv/src/lib.rs:1328), without a DEK behind it. | pending | Three routes, and the smallest one that CLOSES it is the third. (1) The operator: present PW3 once and set the resetting code again after the burn, which is what docs/production.md now says — a cure, not a guarantee. (2) An arm byte in the verifier record, which is cheaper than it sounds: PIN_FORMAT_V1 is written at crates/rsk-openpgp/src/pin.rs:775 and read by nothing, so the arm can ride that byte with no length change, and an older build ignores it — but a FOURTH byte would fail check_pin’s length test while verifier_unusable still called the record usable, which refuses TERMINATE DF’s escape hatch. It tells the card what it cannot otherwise know: a verifier is an opaque hash, so a code set before the burn and one set after are indistinguishable. The burn BOOT is not the unknown — crates/rsk-fido/src/seed.rs:535 already computes it — what stops a deletion there is that it destroys a recovery credential the owner configured. (3) Seal the DEK copies under an outer device-rooted layer that a boot pass can move, as crates/rsk-oath/src/seal.rs:42 and crates/rsk-otp/src/seal.rs:55 already do for their key-base-rooted blobs. The verifier stays brute-forceable and becomes worth nothing without the card; a downgrade fails CLOSED, because every reader gates on the format byte (crates/rsk-openpgp/src/pin.rs:340). That is a persistent-format change and the maintainer’s call. | contributor | SEC-BOOT-001 |
PLAT-TIMER-001 | build-configuration | The timebase every timeout is measured against is a 1 MHz 64-bit tick count that no run can wrap: embassy_time::Instant is a u64 of ticks, embassy-rp’s driver reads RP2350 TIMER0’s NATIVE 64-bit counter rather than extending a 32-bit one in software, and the image pins the rate at 1 MHz — so the roll-over the timeout arithmetic would have to survive is 2^64 microseconds, about 584,542 years. That the counter also ADVANCES is a DIFFERENT claim and PLAT-TIMER-003’s, not this row’s. | discharged | READ on 2026-09-05, and it is the first half of the route this row used to carry; the second half is PLAT-TIMER-002 because no run walks the one written here. FOUR READINGS AND ONE DIVISION. (1) embassy_time::Instant is ticks: u64 and nothing narrows it. (2) The driver reads the silicon’s own 64-bit value: now() takes timerawh, then timerawl, then timerawh again and retries while the two high reads disagree, concatenating (hi as u64) shifted 32 | lo. That is a TORN-READ guard over a hardware 64-bit counter, not a software roll-over extension — the halves are joined, never accumulated, and the SVD the PAC is generated from marks TIMERAWH and TIMERAWL read-only. The revision is pinned in Cargo.lock: embassy-rp 0.10.0, embassy-time 0.5.1 and embassy-time-driver 0.2.2 all at git rev 6c28443489ad5940ab8c1824c090b1f8a7233bf6. (3) The rate is 1 MHz twice over. firmware/Cargo.toml:13 enables embassy-rp’s time-driver, whose feature body is embassy-time-driver?/tick-hz-1_000_000; no manifest in this tree names a tick-hz-* feature of its own — git grep tick-hz -- '*Cargo.toml' exits 1 — so the driver crate’s own no-feature fallback, TICK_HZ = 1_000_000, would give the same answer. firmware/src/presence.rs:137 asserts it at COMPILE time. TWO THINGS ABOUT THAT READING ARE NOT WHAT THEY LOOK LIKE, and both are here because nothing else in the tree says them. The grep is SCOPED because the unscoped one falsifies itself: this sentence used to say that git grep tick-hz over the tree answers nothing else, which was true of the tree it was written against and false of the tree it now sits in — three hits, every one of them this row’s own prose and the page generated from it. A claim about what the tree contains cannot be spelled so that writing it changes the answer. And the citation to the manifest is INVISIBLE to the citation gate, so that gate’s green says nothing about it: scripts/citation_gate.py:556 sets EXTS to rs|sh|txt|py, and no .toml line reference anywhere in this tree is therefore pinned or re-checked. A pre-existing class with other members — assurance/properties.toml:101, assurance/threat_clauses.toml:216-218 and formal/runs.toml:66 among them — which this row names rather than closes; read that line by CONTENT. (4) The boot configuration is the default one: firmware/src/main.rs:524 takes embassy_rp::config::Config::default() and edits only the XOSC startup delay, so the clocks are ClockConfig::crystal(12_000_000) with ref_clk from XOSC at div 1, hence clk_ref 12 MHz, and embassy’s RP2350 arm writes TICKS.timer0_cycles = clk_ref / 1_000_000, which is 12. THE DIVISION: 2^64 ticks at one per microsecond is 18446744073709.55 s, 213503982.33 days, 584,542.05 years of 365.25 days. The route this row used to demand is refused by arithmetic and not by cost. THREE THINGS THIS DOES NOT SETTLE, and one of them is owned by nothing. The compile-time pin is not on every arm: firmware/src/presence.rs:137 sits under cfg(all(not(feature = "no-touch"), not(feature = "display"))), so the display build and the no-touch builds rest on the feature alone. That the counter ADVANCES is unread here and is PLAT-TIMER-003’s, and this sentence read unregistered anywhere until that row was opened on 2026-09-05: it was true, and it sat beside a supports over three liveness properties that need progress and not rate, which is the defect the third row exists to close. Nothing in this tree’s CODE would still notice a stopped tick — no assert, test or proof covers it — and the honest instrument remains a recording of an alarm-driven cadence, since a counter that stopped would freeze that render permanently; what changed is that PLAT-TIMER-003 asserts on it, over the recording PLAT-TIMER-002’s run already produces. And the counter is NOT the read-only part an earlier reading of this row took it for: RP2350 TIMER0 at 0x400b0000 exposes TIMEHW and TIMELW as WRITE-ONLY halves of the same 64-bit value (the SVD’s own words are to change time write to timelw before timehw), beside PAUSE, LOCKED and SOURCE. So the 64-bit wrap is unreachable by a RUN and reachable by a WRITE; what this tree has is no user of any of them, in the firmware or in embassy-rp. | contributor | — |
PLAT-TIMER-002 | timers | The 32-bit alarm comparator survives its own wrap. embassy-rp arms TIMER0.ALARM0 with the LOW 32 bits of a deadline — TIMER.alarm(n).write_value(timestamp as u32) — so once per 2^32 microseconds, 71 min 35 s, the value armed is numerically BELOW the counter’s running low half and the match can only arrive after that half has wrapped. What makes the truncation safe is that it is paired with a full 64-bit re-read: check_alarm compares the stored u64 deadline against now() before it wakes anything. This firmware arms a short alarm continuously — 2 ms or 5 ms in the LED render, 16 ms in the worker — so exactly one such truncated arm straddles every crossing, and a bounded run reaches it without arranging anything. | pending | A board run long enough to cross the COMPARATOR’s wrap, which is the only wrap a bounded run can cross — the 64-bit counter’s is 584,542 years out, and that is PLAT-TIMER-001. THE SPECIFICATION IS THE DRIVER’S OWN COMMENT, at the TIMER.alarm(n).write_value(timestamp as u32) in set_alarm: Note that we're not checking the high bits at all. This means the irq may fire early if the alarm is more than 72 minutes (2^32 us) in the future. This is OK, since on irq fire it is checked if the alarm time has passed. — and check_alarm’s else arm: Not elapsed, arm it again. This can happen if it was set more than 2^32 us in the future. 72 minutes is that comment’s rounding; the register is 2^32 microseconds, 4294.967296 s, 71 min 34.97 s, and the run has to be timed against the exact figure and not the rounded one. THE RUN, in assurance/board/PLAT-TIMER-002.toml: a DEFAULT-image board powered and LEFT ALONE for two full periods, with its LED recorded. Two things about it are the opposite of what the first version of this record asked for, and both were measured rather than argued. Its observable is BOARD-SCOPED: firmware/src/led.rs:618 and firmware/src/led.rs:692 re-arm a 5 ms and a 2 ms alarm for as long as the board has power, needing no host and no finger, and one of them — or firmware/src/worker.rs:307’s 16 ms button poll — is the earliest deadline in the queue at every instant, so the arm that straddles each crossing is one of them. And the run is QUIET: a CTAPHID or CCID request arms a fresh short alarm as it lands (crates/rsk-usb/src/ctaphid.rs:775, crates/rsk-usb/src/ccid.rs:408), which re-arms the comparator and repairs a missed match in microseconds, so wire traffic MASKS this defect instead of producing it — and the keepalives the first version wanted flowing are inside those per-request loops, so an idle board makes none of them anyway. ONE PERIOD IS WHAT GUARANTEES A CROSSING, not two: a run of length L from phase p crosses iff L > 2^32 - p, so the worst phase costs one period. The second period is there because the first crossing lands at most one period in, so two leave a full period AFTER it — and the failure below is a stall of up to a whole period, which a run ending at the crossing could not tell from a run that stopped. WHAT THE RUN DOES NOT REACH, said here because a PASS read as covering it would be read wrong: check_alarm’s else arm — Not elapsed, arm it again — runs only when the IRQ fires while the stored deadline is still in the future, which needs a deadline at least 2^32 microseconds out. The longest alarm anything in this tree schedules is 600 ms, and the only deadline that far out is the u64::MAX the queue’s next_expiration returns when nothing is pending — which this firmware never produces, because the LED render and the worker keep the queue populated. So a PASS here is compatible with that arm being wholly broken; its route is a driver-level test or a firmware that arms a long alarm, and not a board run. WHAT IT DOES NOT SERVE, said here because the row it was split out of claimed it and could not: NOT SEC-FIDO-L01, L02 or L03, and this row carries no supports for that reason. They are PLAT-TIMER-003’s, which reads THIS row’s recording for a different question — whether the counter advances at all — so the recording is shared and the claims are not. A stall of the order of one period that ENDS is this row’s FAIL and that row’s PASS, since only a running counter brings the armed value round again; a series that stops and never resumes is that row’s FAIL and leaves this one INCONCLUSIVE, since a comparator whose counter is dead can be observed neither to miss a match nor to make one; and only a freeze beginning less than a period before the recording ends is inconclusive for both, which is the second reason the run is two periods and not one. The presence window is a busy poll — crates/rsk-device/src/presence.rs:215 compares board.now_us().wrapping_sub(start) against the timeout and spaces its polls with block_for, which spins on Instant::now() and arms no alarm at all — so it is wrap-immune by construction and the comparator is not in it. The pinUvAuthToken and stateful-walk windows are saturating_sub over a u64 millisecond count, checked when a command ARRIVES rather than by a timer, and the longest window the firmware ever measures is crates/rsk-fido/src/consts.rs:392’s PUAT_MAX_USAGE_PERIOD_MS at 600000 ms — 7.16 times SHORTER than the wrap this row is about. This row tests the comparator, not Instant. | maintainer | — |
PLAT-TIMER-003 | timers | The timebase ADVANCES: RP2350 TIMER0’s counter keeps counting for as long as the board has power, so every deadline armed against it is eventually reached and every spin on Instant::now() eventually ends. This is the condition the three liveness properties rest on and PLAT-TIMER-001’s RATE reading is not: EveryOpQuiesces, EveryWaitReleases and EveryWalkCloses are EVENTUALLY claims, so a tick twelve times slow still releases every wait and closes every walk twelve times later, and only a tick that STOPS falsifies them. Nothing in this tree asserts it — firmware/src/presence.rs:137 pins the RATE at compile time and on one build arm of three, and no assert, test or proof anywhere covers progress. | pending | PLAT-TIMER-002’S RECORDING, READ FOR A DIFFERENT QUESTION, and shared deliberately rather than thriftily: the alternative is a second unattended two-hour run producing the same series. THE INSTRUMENT, AND WHY IT WITNESSES PROGRESS — per backend, because the first version of this sentence gave one mechanism to three and only one of them has it. What all three share is the STEP: each advances one step per Timer await and per nothing else — firmware/src/led.rs:618 (ws2812, the default), firmware/src/led.rs:727 (pimoroni) and firmware/src/led.rs:692 (the gpio soft-PWM’s 2 ms period). WHAT DIFFERS IS WHAT THE STEP PAINTS. Only ws2812’s frame is a function of the loop’s own counter: firmware/src/led.rs:589 declares it, firmware/src/led.rs:596 advances it once per await, firmware/src/led.rs:607 is the only thing that reads it, and firmware/src/led.rs:536’s effect_sparkle re-rolls it every eight steps. GPIO AND PIMORONI TAKE THEIRS FROM THE CLOCK: both call Blinker::tick (firmware/src/led.rs:353) — at firmware/src/led.rs:695 and firmware/src/led.rs:719 — which compares Instant::now() against a stored phase end at firmware/src/led.rs:361 and flips the phase when it is reached. THE CONCLUSION SURVIVES THE CORRECTION, and twice over rather than by luck: a stopped counter never returns the await, so no backend takes a step at all; and a clock-driven frame that somehow did step would read a frozen Instant::now() and paint the same colour anyway. So on all three a frame that CHANGES is a witness that the await returned, and an await returns only when the counter reached the value set_alarm armed; a stopped counter holds the last frame for ever and nothing on the device repairs it. THE CHAIN, named so that a reader can see what produces the observable and what reads it: XOSC at 12 MHz drives clk_ref, which firmware/src/main.rs:524’s default ClockConfig selects; clk_ref drives the TICKS block embassy enables with timer0_cycles = 12; that block increments TIMER0’s counter once per microsecond; the counter reaches ALARM0; TIMER0_IRQ_0 runs check_alarm; the queue wakes the render task spawned at firmware/src/main.rs:1022, firmware/src/main.rs:960 or firmware/src/main.rs:968; the task writes a frame; and a camera or a photodiode is what reads it. No host, no finger and no command appears anywhere in that chain. WHY NO READING DOES IT, and the trait contract is the part that surprises: Driver::now’s own documentation promises monotonic in the sense of a greater or equal value than earlier calls, which a stopped counter satisfies exactly — the contract does not contain this claim, so reading it cannot establish it. The hardware guarantee is a datasheet clause about the very silicon a run would be taken on. And the last in-tree reading — that no code writes TIMER0’s PAUSE, SOURCE, LOCKED or the write-only TIMEHW/TIMELW halves, in this firmware or in embassy-rp — already sits inside PLAT-TIMER-001, and it is a reading of what the image does NOT do, which cannot establish what the silicon DOES. Of those four only PAUSE stops the count: SOURCE swaps the tick for clk_sys cycles, which is a RATE change and PLAT-TIMER-001’s axis, and LOCKED only freezes write access. What no reading reaches at all is the clock underneath — a dead XOSC, or a TICKS block that quits, leaves every register this tree can name unwritten and the counter still. WHAT THE SHARED RECORDING SETTLES HERE AND NOT THERE, because two rows on one recording is where a reader stops telling them apart: this row reads the series for a stall that NEVER ENDS, PLAT-TIMER-002 for a stall of the order of one period that DOES end, and the verdicts do not move together. A stall that resumes is this row’s PASS and that row’s FAIL. A series that stops and never resumes is this row’s FAIL and leaves that row INCONCLUSIVE rather than joining it. The one arm they share is a freeze beginning less than a period before the recording ends, inconclusive for both, and assurance/board/PLAT-TIMER-003.toml makes it a condition on the reading rather than only on the length. | maintainer | SEC-FIDO-L01, SEC-FIDO-L02, SEC-FIDO-L03 |
PLAT-TOKEN-001 | model-abstraction | RSKeySecurityState’s tok.live is FidoState::paut.in_use and its pin.set is Fs::has_data(EF_PIN); no second live token and no second PIN record exists that the model would have to carry a field for. | pending | A recorded session that asserts the implication, which the corpus can already carry and no configuration checks. Both halves are projected today: crates/rsk-device/src/ctap.rs:221 and :235 record token_in_use_raw and pin_set, formal/TraceSecurity.tla:44 and :32 map them into B, :60 and :52 map the model side, and R4aRawRefinesB equates all four at every boundary. Measured over formal/traces/security-phase4.jsonl: token_in_use_raw is TRUE in 24 of 40 pre and 24 of 40 post snapshots, pin_record_len == 35 in 28 of each, and the boundaries where the antecedent holds and the consequent does not number ZERO. So unlike PLAT-MODEL-003, whose field is carried and never exercised, this projection runs its TRUE arm 48 times and the only thing missing is a line in an INVARIANTS block. | contributor | SEC-FIDO-008 |
PLAT-TOKEN-002 | model-abstraction | One pin.set boolean stands for one record. EF_DEVICE_PIN, the trusted-display build’s second PIN verifier, is not it, so a state where the device PIN stands and EF_PIN is gone is one this model cannot distinguish from a factory-fresh device. | pending | A source audit of the two verifiers, re-run when a third issuance door is added: crates/rsk-display/src/gates.rs:11 states that the backing record and the floor differ between them, crates/rsk-display/src/pin.rs:752 that the FIDO PIN goes to EF_PIN as the same verifier the host uses, and :455 that a host authenticatorReset clears both. What makes the single boolean sound TODAY is that built-in UV verifies EF_PIN and not the device PIN (crates/rsk-fido/src/clientpin.rs:574 and :612), so both doors to a live token are gated on the record the model has. A pad-only issuance path reading EF_DEVICE_PIN would end this row. | contributor | SEC-FIDO-008 |
PLAT-TOKEN-003 | model-abstraction | clientpin::issue_token is the only production maker of a live pinUvAuthToken, so the one Refines … — SEC-FIDO-008 tag in the tree is the whole antecedent side of the invariant. | pending | An enumeration a derivation already in the tree can re-run, and it was re-run rather than read: git grep -n begin_using_token gives 28 hits, all but two in files assurance_gate.production_rust drops by name, and of the two remaining crates/rsk-fido/src/conformance/mod.rs:165 is reported by assurance_gate.cfg_excluded as lib.rs declares mod conformance under cfg(test). That leaves crates/rsk-fido/src/clientpin.rs:425, inside the tagged function. A second in-image caller ends this row, and the derivation that would find it is the one just named. | contributor | SEC-FIDO-008 |
PLAT-TOKEN-004 | model-abstraction | reset() is the only modelled deleter of EF_PIN and it is not the only deleter: rsk_fs::Fs::factory_wipe bypasses it entirely, and no configuration in this tree runs that path. | pending | Modelling the second path, or a stated argument that its reboot makes the question vacuous. crates/rsk-fido/src/reset.rs:180 and :213 both say in as many words that Fs::factory_wipe bypasses that file and needs the same rule; the entry point is crates/rsk-fs/src/fs.rs:477 and its live callers are crates/rsk-device/src/ccid.rs:311, crates/rsk-display/src/pin.rs:717 and firmware/src/worker.rs:397. It is the SAME unmodelled path PLAT-MODEL-006 names as what would make RamNeverOutlivesFlashSeed bite, reached from the other side: here the question is whether the wipe kills the session before the record, and worker.rs:397 answers it with a reboot the model does not represent either. | contributor | SEC-FIDO-008 |
PLAT-TOKEN-005 | model-abstraction | No existing bounded proof can be reused as evidence for this invariant, so kani = 0 on SEC-FIDO-008 is correct rather than merely unfilled: the reset bridge names no token field, and the four harnesses that do drive begin_using_token never delete the PIN record. | pending | Either a harness of this property’s own, or a conjunct added to an existing bridge — and the second changes what the SEC-FIDO-006 harnesses prove, which is stage 4’s call. Today crates/rsk-fido/src/reset_assurance.rs constrains the reset’s survivors and names no token field, so those harnesses run over states where a token is live and the record is gone; and crates/rsk-fido/src/credmgmt_kani.rs:77, :158, :348 and :416 with crates/rsk-fido/src/state_kani.rs:86 do call begin_using_token, but each drives a permission or cursor question with the PIN record fixed present. None models a deletion, which is the only step that can falsify this implication. | contributor | SEC-FIDO-008, SEC-FIDO-006 |
PLAT-TOOL-001 | tool-fidelity | A green tools/emu run is a protocol result, not a device result: the emulator’s own README enumerates what it does not emulate — secure boot, fuses, the anti-rollback epoch, the partition table, glitch detectors, side channels, the TRNG, the flash medium’s physics, USB packetisation and the worker’s sequencing. | pending | Not dischargeable as written — it is the standing scope of every emulator result. It shrinks when a named half moves into the shared crates, the way the applet wiring and the flash backend already did. | contributor | — |
PLAT-TOOL-002 | tool-fidelity | tools/emu implements the same authorization gates as the firmware, so a recorded session is evidence about the firmware. | pending | A board recording of the same session, compared boundary by boundary against formal/traces/security-phase4.jsonl. | maintainer | SEC-REF-004, SEC-TRACE-001, SEC-TRACE-002, SEC-TRACE-004, SEC-SEAM-001, SEC-SEAM-002, SEC-SEAM-003, SEC-SEAM-004, SEC-SEAM-005, SEC-SEAM-006 |
PLAT-TOOL-003 | tool-tcb | Kani/CBMC is sound for the arithmetic its harnesses bound, and the solver that ran is the pinned one. | pending | Not the recorded identity, which is what an earlier reading of this row proposed and what re-measuring it refutes. This row’s STATEMENT is a conjunction — Kani/CBMC is sound for the arithmetic its harnesses bound AND the solver that ran is the pinned one — and an identity record settles the second conjunct only. The precedent is measured, not argued: the sibling row PLAT-TOOL-004 already HAS the identity half whole — tlaplus 1.7.4 pinned by flake.lock, formal/run-tlc.sh recording the jar’s sha256 prefix — and is still pending, because in its own words what is not dischargeable by any of that is the soundness of the checker itself. Flipping this row on an identity record would leave the two tool-TCB rows answering differently about the same shape of claim, so it stays pending and this field records why. WHAT WAS MEASURED, on the maintainer’s machine, with the commands: ls ~/.kani/ → one bundle, kani-0.67.0; ~/.kani/kani-0.67.0/bin/cbmc --version → 6.8.0 (cbmc-6.8.0), and the banner a run prints is CBMC version 6.8.0 (cbmc-6.8.0) 64-bit arm64 macos; bin/kissat --version → 4.0.1; strings bin/cbmc, grepped for ^cadical-, → cadical-2.0.0, the back end --sat-solver cadical selects; cat rust-toolchain-version → nightly-2025-11-21-aarch64-apple-darwin; cat rustc-version → rustc 1.93.0-nightly (53732d5e0 2025-11-20). bin/ ships cbmc, goto-analyzer, goto-cc, goto-instrument and kissat as PREBUILT binaries and toolchain as a symlink into ~/.rustup. TWO CLAIMS THIS FIELD CARRIED ARE CORRECTED RATHER THAN DELETED. kissat appearing nowhere in the repository is false: grep -rI kissat answers five files, of which three are assurance/bundle/SEC-FIDO-001.toml:258, SEC-FIDO-002.toml:344 and SEC-FIDO-003.toml:338, each writing beside kissat 4.0.1 in the cbmc row’s provenance. And the three bundles no longer disagree: every [[tool]] name = "cbmc" row now carries one reconciled version measured off the install, where SEC-FIDO-001.toml:257 wrote the one cargo-kani 0.67.0 ships; CaDiCaL 2.0.0 as the SAT back end, SEC-FIDO-003.toml:337 the same sentence with the SAT version dropped, and SEC-FIDO-002.toml:343 the CBMC banner naming no SAT back end at all. Of the three, CaDiCaL 2.0.0 was the only claim checkable off the binary, and it checks out. THE VERSION HALF is pinned and now held twice: KANI_VERSION: "0.67.0" at .github/workflows/ci.yml:155, .github/workflows/deep-checks.yml:354 and :446, against the line docs/testing.md:307 tells a reader to run. The caveat this field used to carry — that scripts/kani_gate.py read only deep-checks.yml, so an edit to ci.yml:155 alone was invisible — is CLOSED: scripts/kani_gate.py:389-409 reads every workflow’s env: block and scripts/kani_gate.py:697-708 refuses a disagreement, and assurance/toolchain.toml’s cargo-kani row holds the same three literals against a pin. Measured both ways: moving ci.yml:155 alone is rc=1 at both rows, and with the disagreement clause deleted alone it is rc=0 again. WHAT WOULD SETTLE THE IDENTITY HALF, and why it is not a sentence in this file: a hash of the fetched bundle, recorded where a gate RE-READS it. assurance/toolchain.toml’s cbmc row stays unpinned for a reason this measurement does not move — cargo kani setup fetches the bundle into ~/.kani/, outside the tree, so no file here is one a provenance could open, and a hash whose only source is the moment somebody typed it is what that registry’s own header refuses. Recording today’s five strings as a pin would be exactly that. HERMETICITY IS DELIBERATELY NOT PART OF THIS ROW: cbmc and kissat are prebuilt binaries inside the fetched bundle, not built by the cargo install a flake input would replace, so packaging cargo-kani would not settle it either. Making the shell hermetic is a real and separate obligation and belongs to whichever row states one. The SOUNDNESS half is not settleable here at all, which is why this row, like PLAT-TOOL-004, exists rather than being folded into a run record. | contributor | SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-STORE-002, SEC-TRANS-001, SEC-TRANS-002, SEC-TRANS-003 |
PLAT-TOOL-004 | tool-tcb | TLC is sound for the finite configurations it checks, and the verdict recorded for a configuration is the verdict that run produced. | pending | A pinned checker and a recorded run. tlaplus 1.7.4 IS pinned by flake.lock and formal/run-tlc.sh records the jar’s sha256 prefix, which is the half PLAT-TOOL-003 does not have for cargo-kani; formal/runs.toml keeps each tier’s own TLC lines beside the runner’s, and scripts/run_count_gate.py holds one against the other. What is NOT dischargeable by any of that is the soundness of the checker itself, which is why this row exists rather than being folded into the run record. | contributor | 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 |
PLAT-TOOL-005 | tool-tcb | Kani proves the presence arbiter’s cross-executor flags under a SEQUENTIAL reading of their atomics: the tool says so itself, and the interleaving the harnesses check is one the harness scripts rather than every schedule the two executors can produce. | pending | Either a checker that models the memory ordering, or a source-level argument that the arbiter’s four flags admit no schedule the harness’s own interleaving does not already cover. Measured rather than assumed: cargo kani -p rsk-device --features kani-soft prints warning: Kani currently does not support concurrency. The following constructs will be treated as sequential operations: - atomic_load (6) - atomic_store (6), and the arbiter’s own doc says why that matters — crates/rsk-device/src/presence.rs:72-77, one instance in a static, reached by the interrupt executor (CTAPHID/keyboard) and the thread executor (the worker), &self on every method for exactly that reason. The seven harnesses drive the transports’ cancels from inside Board::block_for_ms, which is a chosen schedule; Ordering::Release/Acquire on cancel_requested and Ordering::Relaxed on cancel_otp_wait’s write are proved by nothing here. | contributor | SEC-FIDO-002 |
PLAT-TOOL-006 | tool-fidelity | The fuzz axis counts a FILE that names the invariant, not a run of it. fuzz/fuzz_targets/fido_session.rs:1432 asserts ONE clause — getPinToken re-issuing the standing token — and assurance_gate.derive reads the axis with grep_word over fuzz/fuzz_targets/*.rs, so fuzz = 1 is one file mentioning the name and says nothing about coverage, corpus or execution count. | pending | A recorded cargo fuzz run fido_session with its execution count and corpus size, filed the way docs/testing.md files the other targets. The weekly deep-checks matrix runs the target; no verdict for it is recorded in this tree. | contributor | SEC-FIDO-003 |
PLAT-TOOLCHAIN-001 | toolchain | The compiler on the path is the pinned rustc and its output is what the proofs are about; Kani proves over MIR, not over the emitted image. | pending | Stage 11’s source-to-binary work. Nothing in the tree bridges MIR to the image today, and saying so is the whole content of this row. | contributor | — |
PLAT-TOOLCHAIN-002 | toolchain | docs/unsafe.md is the enumeration of the first-party unsafe sites: every site the tree carries has a justification there, and every justification is about a site the tree still has. What that enumeration does NOT establish is that any one justification is CORRECT — that is a reading per site, and the twelve PLAT-UNSAFE rows below are where each one is written down and can be refuted. | pending | Two halves, and only the first is mechanical. MEMBERSHIP is derived: scripts/platform_gate.py produces one candidate per unsafe site and refuses both an unclaimed site and a claim on a site that is gone, and it compares that page’s own Runtime sites count and its file list against the tree. The READING half is the twelve rows that refine this one; this entry is settled when they are. It deliberately covers no candidate of its own, so that it cannot stand in for a site nobody read. | contributor | — |
PLAT-TRACE-001 | model-abstraction | A trace-linked claim rests on the fields the recorded session VARIES; 31 of the committed trace’s 81 fields are constant across all 40 events, and a conjunct whose antecedent is one of them was never exercised by the replay. | pending | Sessions that vary them, and there is no substitute: a conjunct is checked by the replay only where its antecedent is true somewhere in the recording. Measured on formal/traces/security-phase4.jsonl — soft_lock_raw, warm_boot_raw, token_user_present_raw, backup_sealed_record, seed_encrypted_record and the four cm_*_raw counters are false or fixed in every event (persistent_grant_record left the list when provisioning started minting the record — the recording opens with one and setPIN deletes it — though the ISSUED grant gate.ppuat is FALSE in every replay state, so no conjunct that reads it is exercised), and token_user_present_raw together with soft_lock_raw are the antecedents of BOTH conjuncts of NoAuthorizationBypass. Two members of this class already had rows of their own — PLAT-MODEL-003 for keydev_ram_raw and formal/README.md’s paragraph for builtin_uv — and the class is what those two are instances of. | contributor | SEC-TRACE-001, SEC-TRACE-002, SEC-TRACE-004, SEC-REF-004 |
PLAT-TRACE-002 | tool-fidelity | No recorded session reaches this property. grep -lw NoTokenAfterInvalidation formal/*.cfg returns every configuration that names the invariant and not one of them is a TraceSecurity* row, so the trace axis reads 0 of 0 — the honest value, and not a gap waiting to be filled by inheritance from a refinement property. | pending | A TraceSecurity* configuration that checks this invariant, over a recording that performs the operations it is about: a changePIN, a stopUsingPinUvAuthToken and a panel PIN entry. formal/traces/security-phase4.jsonl is the existing recording and none of its 40 pre/post snapshot pairs contains one. | contributor | SEC-FIDO-003 |
PLAT-TRNG-001 | build-configuration | The RP2350 TRNG’s three health checks are CONTINUOUS, this image leaves all three armed, and they fail CLOSED: embassy_rp::trng::Config::default() clears every bypass bit and Trng::new writes them into TRNG_DEBUG_CONTROL, firmware/src/main.rs:609 edits sample_count and nothing else, and on a failed check the part presents no result and every EHR_DATA register reads zero. So a source that has DIED cannot be drawn from: at boot that stalls before the USB pull-up goes up, and at the 64 KiB DRBG reseed (firmware/src/handler.rs:78) it wedges or halts the operation in flight. That the surviving source has ENTROPY is a DIFFERENT claim and PLAT-TRNG-002’s, not this row’s: three continuous checks are a dead-source detector, never an entropy estimator. | discharged | READ on 2026-09-05, and it is the reading half of a route that used to carry three claims of very different reachability under one id. FOUR READINGS. (1) ALL THREE CHECKS ARE ARMED, and the image WRITES that rather than inheriting a reset value: embassy_rp::trng::Config::default() sets disable_autocorrelation_test, disable_crngt_test and disable_von_neumann_balancer all false, and Trng::new’s initialize_rng writes those three bits into TRNG_DEBUG_CONTROL (0x138) on every construction. firmware/src/main.rs:601 takes that default, firmware/src/main.rs:609 edits sample_count alone, and firmware/src/main.rs:610 is the tree’s ONLY Trng::new, and no first-party Rust assigns any of the three bypass fields: git grep -E 'disable_autocorrelation_test|disable_crngt_test|disable_von_neumann_balancer' -- 'firmware/*.rs' 'crates/*.rs' 'tools/*.rs' exits 1. THE THREE NAMES AND THE PATHSPEC ARE BOTH THE POINT, not tidiness. Unscoped, that grep answers this row’s own prose and the page generated from it, so a claim about what the tree contains would be falsified by writing it down — PLAT-TIMER-001 records that trap one row over. And disable_ alone over the same pathspec is NOT empty, which is why the command is the three field names and not the prefix — and the count is worth getting right, because the first version of this sentence got it wrong: FOUR hits in TWO files, two test names in crates/rsk-fido/src/vendor_tests.rs and two disable_raw_mode calls in tools/tui/src/main.rs, because git’s pathspec matching lets tools/*.rs cross a /. The revision is pinned in Cargo.lock: embassy-rp 0.10.0 at git rev 6c28443489ad5940ab8c1824c090b1f8a7233bf6. (2) THEY ARE CONTINUOUS, AND THERE IS NO START-UP TEST. RNG_ISR (0x104, RP2350 datasheet of 29 July 2025, p.1217) carries VN_ERR — 32 identical consecutive bits — CRNGT_ERR — two equal consecutive 16-bit blocks — and AUTOCORR_ERR, and each is evaluated as a block is produced rather than once at reset — AUTOCORR_ERR latching after four failures in a row rather than on the first, which the driver’s own comment quotes from the register description. That datasheet describes no start-up test and no Adaptive Proportion Test, which is worth writing down because SP800-90B’s health-test vocabulary makes a reader expect both: what this part gives is a per-block continuous test and nothing else. (3) THEY FAIL CLOSED AND LOUDLY, which is the half the row this was split from had backwards. §12.12.3 p.1213: on failure no results are presented and the EHR_DATA registers all read as 0, so TRNG_VALID.ehr_valid stays low and no byte reaches the caller; AUTOCORR_ERR is LATCHED — in the datasheet’s own words the RNG then ceases functioning until the next reset — and the interrupt-clear register does not lift it: what the driver does instead is assert TRNG_SW_RESET and re-initialise, which is the loop below and not a recovery. This firmware’s boot draw is the BLOCKING one: firmware/src/handler.rs:63 takes the Trng and firmware/src/handler.rs:65 fills 48 bytes through blocking_fill_bytes, whose not-valid branch soft-resets and re-samples on AUTOCORR_ERR and panics on anything else. Either way the boot does not finish — it is the 30-105 s stall firmware/src/main.rs:602-608 records, taken before the bus pull-up (firmware/src/usb_attach.rs:8) — and a device that never enumerates is not a device handing out predictable keys. AND THE BOOT IS NOT THE ONLY DRAW, which the first version of this reading missed: firmware/src/handler.rs:78 calls the same blocking_fill_bytes again on every RESEED_INTERVAL (firmware/src/handler.rs:57, 64 KiB of DRBG output), so a source that dies AFTER boot meets the same loop on an ENUMERATED device, inside whatever operation asked for the bytes. Loud in a second way — a wedged command or a panic-halt freeze rather than a device that never appears — and still not a quiet weak key, which is the claim. (4) WHAT sample_count = 1000 DOES, AND WHAT IT DOES NOT. SAMPLE_CNT1 (0x130, p.1218) is the number of rng_clk cycles BETWEEN two consecutive ROSC samples, so 25 -> 1000 buys DECORRELATION and costs generation time; it does not change the 192 bits an EHR block carries and it adds no entropy to any of them. Why it was raised is on record and was measured on hardware at 2cdcc282e9605d601631b4b06727b2f746325727: at 25 the autocorrelation check failed on nearly every block on one Waveshare unit and the driver soft-reset in a loop, an inverter-chain change did NOT help, and 1000 gives a seed in about a second and a half. THREE THINGS THIS DOES NOT SETTLE. That the surviving source has ENTROPY — the checks catch a source that has DIED and a merely DEGRADED one passes all three, which is the single failure this row’s statement deliberately leaves open and PLAT-TRNG-002’s whole subject. WHICH loud arm a CRNGT or VN failure takes: blocking_wait_for_successful_generation branches on autocorr_err alone and panics otherwise, and whether the part drops TRNG_BUSY with ehr_valid low on those two is a clause this reading does not have — a stall and a panic-halt freeze are both loud and neither is a quiet weak key, so the claim survives either answer while the answer stays unread. And NOTHING IN THIS TREE BACKS THE FAIL-CLOSED CLAUSE: the driver’s read_ehr_registers_into_array copies EHR_DATA0 through EHR_DATA5 with no zero check and firmware/src/handler.rs:63 does not inspect the seed it gets, so no byte reaches the caller rests on the datasheet’s promise that ehr_valid stays low and on no code here — a part that ever raised that flag over zeroed result registers would seed the DRBG with 48 zero bytes and nothing would say so. And the CORNERS: everything above is about what this image configures at desk conditions, and temperature, supply and process are PLAT-TRNG-003’s. TWO THINGS THE READING FOUND AND THIS CHANGE REPAIRED, because they were firmware comments rather than registry entries and they were two copies of ONE claim: firmware/src/handler.rs:44 told the reader the block was drawn only through a working ROSC config with the chain at zero, and firmware/src/handler.rs:61 repeated it as a draw through the ROSC config the caller set on the Trng. No such configuration ever existed on this branch: 2cdcc282e9605d601631b4b06727b2f746325727 replaced the inverter_chain_length = InverterChainLength::None assignment with the sample_count = 1000 one and dropped the InverterChainLength import, and left both sentences standing — so from 2026-06-18 the shipped image ran the driver’s DEFAULT chain length while its own doc comment called that setting catastrophic, and git grep inverter_chain_length answered with no Rust at all. Both lines now say what the code does — the draw finishes because of sample_count, and the chain length is the driver’s — which is what that commit’s own message already recorded when it wrote that an inverter-chain change did NOT help. THE BEHAVIOUR WAS NEVER WRONG AND THE EXPLANATION OF IT WAS, for eleven weeks, which is why this belongs in a reading’s discharge rather than in a fix: nothing about the image changed when the sentences did. | contributor | — |
PLAT-TRNG-002 | trng | The RAW ring-oscillator source clears the floor the shipped whitening needs — at least half a bit of min-entropy per raw bit, measured AT THE SAMPLE SPACING THE PRODUCT USES, on the die this project owns and at desk conditions. HALF A BIT IS SUFFICIENT AND NOT NECESSARY, and which way round is the point rather than a hedge: a von Neumann debiaser emits at most one bit per two raw bits, so at 0.5 bits per raw bit every whitened bit is backed by a full bit of input min-entropy AT EVERY RATE THAT BALANCER CAN ACHIEVE, and at a slower real rate by more. Below the floor the BOUND stops holding, not the device — von Neumann’s output is exactly uniform for any fixed bias, so bias alone never starves it and what actually threatens it is CORRELATION between samples, which is what sample_count buys (PLAT-TRNG-001) and what the non-IID estimators are chosen to see. Neither of the two things this tree already has can answer it: the three continuous checks PLAT-TRNG-001 reads detect a source that has DIED and pass a degraded one, and a statistical test of the WHITENED output passes over a stuck source, which is what whitening is for. What rests on the floor is the 48-byte DRBG seed firmware/src/handler.rs:64 declares and firmware/src/handler.rs:65 fills at every boot, and every key the device mints afterwards. | pending | A BENCH IMAGE AND SP800-90B, and the route is REACHABLE — the first thing this split corrects, because the row it came from said the raw source needs an image this tree does not ship and left a reader picturing an exotic rig. The raw pre-whitening samples are readable in software on a stock part: TRNG_DEBUG_CONTROL (0x138, RP2350 datasheet of 29 July 2025, p.1219) exposes AUTO_CORRELATE_BYPASS, TRNG_CRNGT_BYPASS and VNC_BYPASS, and that datasheet’s own bootrom listing at §12.12.4.1 p.1214 sets sample_cnt1 = 0 and trng_debug_control = -1u and reads EHR_DATA to stream raw TRNG ROSC samples — shipping pico-sdk does the same in src/rp2_common/pico_rand/rand.c. THE RUN, in assurance/board/PLAT-TRNG-002.toml: that bypass configuration on one board, at least 1,000,000 consecutive raw samples captured and hashed into the record, then the SP800-90B §6.3 non-IID estimator suite over them. AT THE SHIPPED SAMPLE_CNT1, AND THAT IS A CORRECTION rather than a detail: the bootrom listing sets the sample period to 0 because it wants throughput, and 0 is the MOST correlated setting this part offers, while the product spaces its samples 1000 cycles apart. A verdict taken at 0 would be about a stream the device never draws, and this row’s own FAIL is gate-forced to refuted — so the criterion is read off the 1000 capture and the 0 capture is kept beside it as the correlated control, which is also what makes the pair say whether the spacing bought anything. AND A SECOND HALF THE SAME SESSION CAN TAKE: AUTOCORR_STATISTIC (0x134, p.1218) read with the checks re-enabled at sample_count 25 and at the shipped 1000 on the same unit, which is the only way this project can put a RATE behind firmware/src/main.rs:609 — what stands behind it today is one wall-clock observation of a boot on one Waveshare unit at 2cdcc282e9605d601631b4b06727b2f746325727, and a boot time is not a health-check failure rate. WHY THE CRITERION NAMES NO DATASHEET FIGURE, said here because the row this was split from named one and there is none. §12.12.1 p.1212 makes a bare compliance assertion and gives approximately 7.5 kb/s of entropy, which is a RATE and not min-entropy per bit; §12.12.2 p.1213 records that software does not configure the ROSC length and sample count settings provided by the Arm characterisation procedure, so the vendor declined the procedure that would have produced one; and the part holds no NIST ESV or ENT listing. PASS = min-entropy at or above the datasheet figure was therefore a clause no passing world could walk. The record names its own threshold and justifies it there instead, which is the whole of what changed. WHAT THIS RUN DOES NOT REACH, said because a PASS read as covering it would be read wrong: one die, one desk, one temperature and one supply — the corners are PLAT-TRNG-003’s — and the whitening itself, since the capture bypasses it, so this measures the SOURCE and says nothing about how many raw bits the shipped path spends per EHR block. | maintainer | SEC-FIDO-003, SEC-FIDO-008 |
PLAT-TRNG-003 | trng | Nothing in this project qualifies the raw source at the TEMPERATURE, SUPPLY and PROCESS corners. PLAT-TRNG-002 is one die on one desk, and a ring oscillator’s entropy is a function of the jitter its corner leaves it, so a source that measures well at room temperature on a bench supply is not thereby a source that measures well in a warm pocket, on a hub that sags, or on the next wafer. The gap is ACCEPTED here rather than scheduled, and its severity is UNKNOWN rather than low. | accepted-risk | ACCEPTED, and the two routes are dead for DIFFERENT reasons — which is what makes this something other than an ordinary expensive row. THE EQUIPMENT: a thermal chamber, a programmable supply and enough parts for a process spread, none of which this project has, and hardware is the maintainer’s alone under AGENTS.md. That much is only cost. THE REFERENCE IS THE HALF THAT DOES NOT COME BACK: there is no vendor number a corner result could be held against. §12.12.2 p.1213 of the RP2350 datasheet of 29 July 2025 records that software does not configure the ROSC length and sample count settings provided by the Arm characterisation procedure — the vendor declined the procedure — §12.12.1 p.1212 publishes a generation rate and no min-entropy per bit, and the part holds no NIST ESV or ENT listing. So even a fully instrumented corner run would produce a number with nothing to compare it to except a threshold this project chose for itself, which is a self-consistency check and not a qualification. WHY THIS IS NOT PLAT-CRYPTO-002’S SHAPE, and the difference is the reason this is a row instead of a sentence inside that one: that row accepts a residual it argues LOW, and it argues it FROM EVIDENCE IN THIS TREE — four command surfaces read for whether any hands a host a time-resolved observation, and arithmetic over a window table whose stride is in the source. THIS ROW CAN MAKE NO SUCH ARGUMENT AND MUST NOT LOOK AS THOUGH IT DOES. It has no in-scope half to read, no vendor figure to lean on and no measurement in either direction, so sitting under the same status word is the only thing the two have in common. WHAT WOULD TAKE THE ACCEPTANCE OFF, since an accepted-risk row may carry no revalidated_by: Raspberry Pi publishing a characterisation or a min-entropy figure for this ROSC; an ESV or ENT listing appearing for the part; an independent corner qualification of an RP2350 TRNG published by anyone; or this project acquiring the chamber and the supply, at which point the row becomes a maintainer-owned board obligation with a record of its own — and not before, because a planned record for a run no equipment can take is the dead route this split exists to remove. | vendor | — |
PLAT-UNSAFE-001 | toolchain | InterruptExecutor::on_interrupt is called only from the interrupt the executor was started on: EXECUTOR_HIGH.start(interrupt::SWI_IRQ_1) is the only starter in the tree, and the #[interrupt] handler SWI_IRQ_1 is its only caller. | discharged | Read both sides in firmware/src/main.rs and count them: one EXECUTOR_HIGH.start, which names interrupt::SWI_IRQ_1, and one on_interrupt call, inside the handler of that same name. Done, and the counts are what make it refutable — a second starter, a second caller, or a start naming a different interrupt refutes it, and each is one grep. | contributor | — |
PLAT-UNSAFE-002 | toolchain | SendUsb is sound: embassy_usb::UsbDevice is !Send only for the &mut dyn Handler control-request handlers it holds, and every stateful handler this firmware registers keeps its state in a critical-section static, while the wrapper itself is constructed once and moved into exactly one task on one executor. | pending | Two readings, and only one is done. The OWNERSHIP half is read and holds: firmware/src/main.rs constructs SendUsb at one place and hands it to usb_task on the high-priority executor, and nothing else names the type. The HANDLER half is what is owed — a walk of every Handler the USB builder is given, asking of each whether its state is a zero-sized type or a Sync static. A handler with plain interior mutability refutes the row. | contributor | — |
PLAT-UNSAFE-003 | toolchain | HEAP.init runs exactly once, over a static buffer nothing else touches, and before the first allocation the image can make. | pending | Read firmware/src/main.rs for the first two — one HEAP.init, one HEAP_MEM, both inside one block — which hold. The third is what is owed and is not visible from the call site: no allocating call on the path from the reset vector to that line, including inside embassy_rp::init and any StaticCell or dependency initialiser that runs before it. An allocation before the allocator is initialised refutes it. | contributor | — |
PLAT-UNSAFE-004 | build-configuration | Each of the eight build-selected GPIOs handed to AnyPin::steal has exactly one owner at runtime: no two of them name the same pad, none of them is a pad another driver claims, and the LED data pin a host can re-aim cannot be pointed at any of them. | pending | The compile-time asserts in firmware/build.rs and the boot-time filter in firmware/src/main.rs, read TOGETHER with the presence button’s own steal in firmware/src/presence.rs and against the five board files under firmware/boards. The asserts reject a build that collides LED_POWER_PIN, USR_LED_PIN, WAKE_PIN or the four panel control lines with each other, with the LED data pin, or with the hard-wired SPI1 and I2C1 lines; the filter drops a host-written data pin naming one of them back to the build default. What is owed is the PAIRWISE table: that the assert set covers every pair of the eight rather than the pairs somebody thought of. One uncovered pair refutes it. | contributor | — |
PLAT-UNSAFE-005 | toolchain | The two static mut prime sieves are single-core-exclusive: CORE0_SIEVE is taken by reference only on core 0 and CORE1_SIEVE only on core 1, and the end-of-search scrub is issued by the core that owns the sieve it scrubs, so the two exclusive references never alias. | pending | A source audit of the three access sites in firmware/src/core1.rs, each read for WHICH core reaches it: two on core 1 (the search, and the scrub on its STOP edge) and one on core 0, in run_rsa_search. The partition is structural rather than locked, so it is refuted by a fourth access, by a scrub issued from the reboot path on core 0, or by run_rsa_search becoming reachable from core 1. | contributor | — |
PLAT-UNSAFE-006 | toolchain | Each core programs MSPLIM once, on the core that owns that stack, before any frame has been pushed below the value it writes: core 0 with the linker’s _stack_end, core 1 with its own stack base. | pending | Read the two write sites against the entry points that reach them — arm_stack_limit in firmware/src/main.rs from the first statement of main, and the firmware/src/core1.rs write from the top of the core-1 entry — and against the linker script that defines _stack_end. Whether the register TRAPS is a fact about ARMv8-M silicon and is deliberately NOT this row: no board result in this tree records it, and PLAT-UNSAFE rows are readings, not measurements. | contributor | — |
PLAT-UNSAFE-007 | toolchain | The three FFI calls into the vendored ARM assembly pass fully owned, length-checked buffers on both sides, so no routine can write past what the caller sized. | pending | A call-by-call reading of the three calls in crates/rsk-rsa/src/lib.rs against crates/rsk-rsa/csrc/bignum_high_level.h: for each pointer, the buffer it names, the length the caller passes, and the length the C side writes. The containment already in place does not settle it and is worth being plain about — the power-on KAT gates key generation and every signature is Bellcore-checked, so a WRONG answer cannot leave the card, but neither check can see an out-of-bounds write. | contributor | — |
PLAT-UNSAFE-008 | toolchain | The wiper’s two ROM flash sequences run with interrupts off and XIP disabled for their whole extent, and no part of rsk-wipe is linked into the firmware image. | pending | Two readings. That both sequences sit inside one critical_section::with from connect_internal_flash through flash_enter_cmd_xip, with nothing between them that could fetch from XIP — a reading of the two functions in rsk-wipe/src/main.rs. And that rsk-wipe is a workspace member built as its own binary that no firmware target depends on, which the manifests settle: firmware/Cargo.toml names it nowhere. | contributor | — |
PLAT-UNSAFE-009 | toolchain | Both env::set_var calls run in a build-script process that has spawned no thread, so there is no concurrent environment reader for the call to race, and nothing either of them sets reaches the firmware image. | discharged | Read both build scripts, which is the whole argument: cargo runs each as its own process, so the only code that could hold a concurrent getenv is the script and its build dependencies. Neither script names a thread, a spawn or a parallel iterator; both calls sit inside the script’s own main, the rsk-rsa one directly and the firmware one through a closure defined there. firmware/Cargo.toml declares NO build dependencies at all, and crates/rsk-rsa/Cargo.toml declares one, cc, which the script first calls after the set_var. Refuted by either script spawning a thread, or by a build dependency called before the set_var doing so. | contributor | — |
PLAT-UNSAFE-010 | build-configuration | The two link_section image-definition statics are placed by the linker at an address the boot ROM reads as the RP2350 image definition, and #[used] keeps them in the image. | pending | Read firmware/memory.x and the cortex-m-rt link script the build uses for a .start_block output section at the image base, and check that both statics — firmware/src/main.rs’s and rsk-wipe/src/main.rs’s — carry #[used]. The section NAME is half the claim and it is now half the site key too, so renaming .start_block re-keys both candidates and reddens this row; before that it was a string literal the gate’s lexer blanked, and any name at all was exit 0. This one fails LOUDLY rather than silently — a section the linker does not know places the block wherever it likes and the ROM then finds no image definition, which is a device that will not start — so the reading is owed for completeness rather than because a silent failure is plausible. | contributor | — |
PLAT-UNSAFE-011 | build-configuration | The small-prime table and the sieve step are placed in .data.small_primes and .data.sieve_step, which the link script collects into .data in SRAM, so the sieve executes and reads out of RAM rather than through the XIP cache. | pending | Read the link script’s .data input-section pattern for .data.*, then confirm on a built image that both symbols of crates/rsk-rsa/src/lib.rs land in the RAM region — nm over the ELF settles it in one command, and no artifact in this tree records that today. This row exists because the two sites were on NO line of docs/unsafe.md before the derivation moved to sites: they were the half of that page’s enumeration nothing was holding. Both section names are part of the site keys now, so .data.small_primes or .data.sieve_step renamed is a red row rather than the byte-identical exit 0 it was. | contributor | — |
PLAT-UNSAFE-012 | toolchain | The three unsafe extern blocks declare what they name: the RSA assembly signatures match the vendored C header, and the two firmware blocks declare linker symbols that are taken as addresses and never read as data. | pending | A signature-by-signature reading of the crates/rsk-rsa/src/lib.rs block against crates/rsk-rsa/csrc/bignum_high_level.h, and of the two firmware/src/main.rs blocks against the symbols firmware/memory.x and the cortex-m-rt script define. The ADDRESS half is already visible at the call sites and holds — kvmain_range, kvcnt_range and arm_stack_limit each take addr_of! or &raw const and none dereferences — so what is owed is the ABI half, which no compiler on either side can check. | contributor | — |
PLAT-XIP-001 | multicore-xip | Core 1 is paused for the whole of every flash erase or program, so no instruction is fetched from XIP while the array is unreadable, and the inter-core FIFO makes progress so the pause is released. | pending | A board measurement: core 1 executing from XIP across a store write, with the pause instrumented. firmware/src/core1.rs carries the two unsafe sites this rests on and docs/unsafe.md justifies them as Rust invariants — which is a different question from whether the silicon behaves as the pause assumes, and that difference is why this row is not PLAT-TOOLCHAIN-002’s. | maintainer | SEC-STORE-002 |
Freshness
A settled row records the commit its result was taken at, and 9 of these do. An input is COVERED when the commit that last touched it is an ancestor of that one; a row behind any of its inputs is stale, and the claims resting on it inherit that. The inputs are derived, not listed: a row’s evidence, plus every in-tree path its own revalidated_by names — which is how formal/gen-configs.sh reaches PLAT-CRED-004, whose whole discharge rests on an emit in that file and whose evidence does not mention it.
Committed history only, so an uncommitted edit to an input is invisible until it lands — the same hole docs/assurance-vector.md names about itself. Stale is not a red: 9 of 9 are stale right now, and a gate red in its resting state is one nobody reads. What it costs instead is this page — a row going stale is a diff.
That price is worth stating for the unsafe rows, because the input is a whole FILE and the claim is two lines of it. PLAT-UNSAFE-001 is anchored on firmware/src/main.rs, so ANY commit touching that file flips it stale and owes this page a regeneration — including the many that cannot touch what the row is about. The site-level axis such a row wants is already elsewhere: its covers keys are the sites’ own code, so a site that is rewritten reddens the row outright rather than dating it. Re-anchoring freshness on the site would mean git log -L over a line range — keyed on line numbers that shift, for a second answer to a question covers already answers by content.
| ID | Taken at | Freshness | Behind | Claims that inherit it |
|---|---|---|---|---|
PLAT-BUILD-001 | bd1cff7 | stale | docs/assurance-matrix.md, firmware/Cargo.toml | SEC-FIDO-001, SEC-FIDO-004, SEC-FIDO-006, SEC-FIDO-006B |
PLAT-CRED-004 | 0eb2a5f | stale | formal/RSKeySecurityState.tla, formal/gen-configs.sh, formal/runs.toml | SEC-FIDO-005 |
PLAT-MEM-001 | 7904f01 | stale | assurance/board/PLAT-MEM-001-2026-09-03-control.log, assurance/board/image-2026-09-03.txt, firmware/src/worker.rs, tests/54_sram_residue.py | SEC-FIDO-007 |
PLAT-MODEL-010 | f5577ab | stale | formal/RSKeySecurityState.tla, formal/comutants.toml | SEC-FIDO-001, SEC-FIDO-003, SEC-FIDO-004 |
PLAT-ROM-002 | 7904f01 | stale | assurance/board/PLAT-ROM-002-2026-09-03-enumeration.txt, assurance/board/PLAT-ROM-002-2026-09-03-reboot.log, assurance/board/image-2026-09-03.txt, firmware/src/worker.rs | SEC-ADM-001, PLAT-MEM-001, PLAT-ROM-001 |
PLAT-TIMER-001 | 4f2b659 | stale | Cargo.lock, firmware/Cargo.toml, firmware/src/main.rs | PLAT-TIMER-003 |
PLAT-TRNG-001 | 578a924 | stale | Cargo.lock, firmware/src/handler.rs, firmware/src/main.rs | PLAT-TRNG-002 |
PLAT-UNSAFE-001 | 709cb52 | stale | firmware/src/main.rs | — |
PLAT-UNSAFE-009 | 709cb52 | stale | firmware/Cargo.toml, firmware/build.rs | — |
Where the accepted risks are published
5 rows accept a risk rather than discharging it, and an accepted risk that is not published is a decision only this file knows about. docs/limitations.md is where the project publishes them; a row the page names pins the section back, and the pin and the page must agree about which section that is.
| ID | Published as |
|---|---|
PLAT-BUILD-005 | Cryptography |
PLAT-CRYPTO-002 | Cryptography |
PLAT-MODEL-008 | not published there |
PLAT-MODEL-014 | not published there |
PLAT-TRNG-003 | Hardware / physical |
The 2 unpublished rows are model OVER-APPROXIMATIONS whose discharge route reads nothing to run, and that page opens by saying it covers feature and hardware gaps. An anchor minted for them would publish a proof-scope note as a user-facing limitation, so the status word is what is carrying two different things here, and splitting it is a decision and not a generated table’s.
The graph
Stage 1B п.3’s link vocabulary, less contradicts: no pair here contradicts another, and a link kind with no instance is a rule whose only exercise is its own mutation.
| From | Link | To |
|---|---|---|
PLAT-BUILD-001 | discharges | AlwaysUvShipped |
PLAT-BUILD-005 | depends_on | PLAT-CRYPTO-002 |
PLAT-MEM-001 | depends_on | PLAT-ROM-002 |
PLAT-MODEL-001 | discharges | WidePerms |
PLAT-MODEL-003 | refines | PLAT-TOOL-002 |
PLAT-MODEL-005 | depends_on | PLAT-MODEL-004 |
PLAT-MODEL-010 | discharges | ForceChangeModelled |
PLAT-MODEL-015 | discharges | RekeyOrderModelled |
PLAT-RESET-001 | discharges | PowerOnClearsScratch2 |
PLAT-ROM-001 | depends_on | PLAT-ROM-002 |
PLAT-STORE-001 | depends_on | PLAT-FLASH-001 |
PLAT-STORE-002 | depends_on | PLAT-FLASH-001 |
PLAT-STORE-002 | depends_on | PLAT-STORE-001 |
PLAT-STORE-003 | depends_on | PLAT-FLASH-001 |
PLAT-STORE-003 | depends_on | PLAT-STORE-001 |
PLAT-TIMER-002 | depends_on | PLAT-TIMER-003 |
PLAT-TIMER-003 | depends_on | PLAT-TIMER-001 |
PLAT-TOKEN-004 | depends_on | PLAT-MODEL-006 |
PLAT-TOOL-002 | refines | PLAT-TOOL-001 |
PLAT-TOOL-005 | refines | PLAT-TOOL-003 |
PLAT-TRNG-002 | depends_on | PLAT-TRNG-001 |
PLAT-TRNG-003 | depends_on | PLAT-TRNG-002 |
PLAT-UNSAFE-001 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-002 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-003 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-004 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-005 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-006 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-007 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-008 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-009 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-010 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-011 | refines | PLAT-TOOLCHAIN-002 |
PLAT-UNSAFE-012 | refines | PLAT-TOOLCHAIN-002 |
supports is in the table above, on 70 of 92 rows. A property it names is CONDITIONAL on that row while the row is pending; nothing here upgrades a property’s evidence.
What this page may not be read as
- that any of these 92 statements is known to be true — 78 are
pending, which means no artifact in this tree records a result for them.pendingcovers two states this page cannot tell apart: a run nobody took, and a run that happened and whose capture never reached a record. A row in the second says so in its own discharge route, because nothing here can derive it. - that the list is complete. 5 derivations produce it, and stage 10’s inventory names eleven categories — a category with no candidate source is a category this page cannot see.
- that a discharged row makes a property proved. It removes a condition; the property’s own evidence is
docs/assurance-vector.md’s.