diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a71a747f..4a21effb2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,6 +38,19 @@ tag: the USB `bcdDevice` build counter (bumped on every behavior change), and ## [Unreleased] +### Fixed + +- **PIV serves a Card Capability Container** (`5FC107`) where it previously + answered `6A82` on a card whose host had never written one. It is a mandatory + PIV object (SP 800-73-4 pt1 §3.1.1), and the Windows inbox PIV minidriver + reads it while opening a key container — the shape here follows Table 8's + mandatory elements in table order, with `F5` carrying the PIV data model + number `0x10`. `get_data` reads flash first, so a host `PUT DATA` still + overrides it and an empty one falls back to the default, exactly like the + synthesized CHUID. +- `bcdDevice` moves to **0x09DB**: the applet is shared, so every board's image + gains the object. + ## [0.4.11] - 2026-09-08 The catch-up release, and the one where the instruments were audited harder than diff --git a/assurance/board/PLAT-TIMER-002.toml b/assurance/board/PLAT-TIMER-002.toml index f6c0db9ea..119d545eb 100644 --- a/assurance/board/PLAT-TIMER-002.toml +++ b/assurance/board/PLAT-TIMER-002.toml @@ -40,7 +40,7 @@ # series belong to which, rather than leaving that to a reader holding both. assumption = "PLAT-TIMER-002" -method = """Power a DEFAULT-image board and LEAVE IT ALONE for at least 8589.934592 s -- two comparator periods, 2 h 23 min 9.93 s -- rounding up, so 2 h 24 m is the figure to run. No replug, no reset. THE LENGTH IS DERIVED, and in two steps rather than one, because the first version of this record collapsed them and got the arithmetic wrong: it called two periods "the shortest run that crosses at least one boundary whatever that phase is", and that is false. The period is 2^32 microseconds = 4294.967296 s = 71 min 34.967296 s. (1) A run of length L from an unknown phase p crosses a boundary iff L > 2^32 - p, so the worst phase needs ONE period and not two -- 71 min 35 s already guarantees a crossing whatever the phase at boot was. (2) What the second period buys is a different thing, and it is the reason to run it: the first crossing lands at T - p, which is at most one period in, so two periods always leave a full period AFTER the crossing -- and FAIL below is a stall of up to a whole period, which a run ending at the crossing could not tell from a run that simply stopped. NOTHING MAY TALK TO THE BOARD INSIDE THE WINDOW, and that is load-bearing rather than convenient: every CTAPHID and CCID request arms a fresh short alarm the moment 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 before anything could see it, so a chatty host does not strengthen this run, it empties it. Prove the silence instead of assuming it: on a host, capture the bus for the whole window (usbmon, or Wireshark's USB capture) and keep the capture beside this record; on a charger there is no host to prove anything about, and that is the simpler arm for SILENCE and the weaker one for everything else -- no bus capture, no journal to read, and so no reboot instrument at all -- which is why that arm owes a supply that can be shown not to have dropped, a logging supply or a current trace kept beside this record, and answers INCONCLUSIVE without one. THE OBSERVABLE IS THE LED, and the board produces it alone -- no host, no finger, nothing held open. One render task per backend is spawned on the high-priority executor at firmware/src/main.rs:1022 (ws2812, the default), firmware/src/main.rs:960 (gpio) or firmware/src/main.rs:968 (pimoroni), and each loops on an alarm it re-arms for as long as the board has power: firmware/src/led.rs:618 and firmware/src/led.rs:727 are 5 ms, firmware/src/led.rs:692 is the gpio soft-PWM's 2 ms period. One of those -- or the worker's 16 ms button poll, firmware/src/worker.rs:307 -- is the earliest deadline in the queue at every instant of the run, so the arm that straddles each crossing is one of them and nothing has to be arranged for it to be. What a camera sees is the render: the ambient effect is a ~2 s breathing cycle once a host has configured the device and a twinkle before that, and the gpio and pimoroni backends blink 500 ms on, 500 ms off in both of those states. Record it end to end -- a camera with a running clock in frame, or a photodiode into a logging ADC. SAMPLE WELL ABOVE THE AMBIENT CADENCE, ten frames a second or better, and not the one frame a second the run's length makes tempting: the cadence is 0.5 s on the blinking backends, and a sampler near that rate aliases into a constant, which reads as the FAIL below rather than as an instrument that was too slow. WHAT THIS RECORD DOES NOT YET HAVE, said the way PLAT-FLASH-001 says it. The crossing is not announced by the device, so it is located by arithmetic over the recording's own clock rather than pinned to a device event, and the run therefore proves the ABSENCE of a stall across a window that certainly contains a boundary rather than pinning the survival to the boundary itself. The device's own clock IS readable, and the first version of this record was wrong to say that no instrument in this tree reports the device's uptime: every audit-journal entry is stamped with the ms-since-attach of firmware/src/usb_attach.rs:34-36 -- firmware/src/worker.rs:469 is where the dispatch hands it over -- and tools/rsk/audit.py:170 prints it as the `uptime` column. But reading it costs a command, and a command inside the window is the traffic that masks the defect, so it BRACKETS the run instead of sampling it -- and THE CLOSING STEP HAS TO WRITE, which the first version of this sentence got wrong: enumerate, `rsk audit enable` (PIN and one touch, before the window opens), go quiet, close with `rsk audit disable` (crates/rsk-fido/src/vendor.rs:518 appends the EV_AUDIT_CFG before the flag clears) or with `rsk audit verify` (crates/rsk-fido/src/journal.rs:559 appends an EV_CHECKPOINT; that arm additionally needs a provisioned OTP DEVK, so `disable` is the one every board can run), and only THEN `rsk audit log`, whose newest entry is what dates the run on the device's own counter as well as on the host's. A READ-ONLY CLOSE DATES NOTHING. AUDIT_READ appends no entry at all -- crates/rsk-fido/src/vendor.rs:481 is a bare `journal::vendor_read` -- so after a quiet window the newest entry is still the PRE-WINDOW enable, carrying the uptime it had then. And `EV_BOOT` is appended LAZILY, on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside the window followed by a read-only close writes nothing and the exported window is BYTE-IDENTICAL with and without one. MEASURED against this tree's own journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only close, newest `uptime` 1000 ms, and the rebooted run byte-identical to the quiet one; writing close, newest `uptime` 8590935 ms on the quiet run against a second `EV_BOOT` and 4294967 ms on the rebooted one. An uptime the device volunteers with no command behind it, or a boundary it signals on its own, is the second instrument this row still owes, and it is the one that would turn this from an absence into a location.""" +method = """Power a DEFAULT-image board and LEAVE IT ALONE for at least 8589.934592 s -- two comparator periods, 2 h 23 min 9.93 s -- rounding up, so 2 h 24 m is the figure to run. No replug, no reset. THE LENGTH IS DERIVED, and in two steps rather than one, because the first version of this record collapsed them and got the arithmetic wrong: it called two periods "the shortest run that crosses at least one boundary whatever that phase is", and that is false. The period is 2^32 microseconds = 4294.967296 s = 71 min 34.967296 s. (1) A run of length L from an unknown phase p crosses a boundary iff L > 2^32 - p, so the worst phase needs ONE period and not two -- 71 min 35 s already guarantees a crossing whatever the phase at boot was. (2) What the second period buys is a different thing, and it is the reason to run it: the first crossing lands at T - p, which is at most one period in, so two periods always leave a full period AFTER the crossing -- and FAIL below is a stall of up to a whole period, which a run ending at the crossing could not tell from a run that simply stopped. NOTHING MAY TALK TO THE BOARD INSIDE THE WINDOW, and that is load-bearing rather than convenient: every CTAPHID and CCID request arms a fresh short alarm the moment 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 before anything could see it, so a chatty host does not strengthen this run, it empties it. Prove the silence instead of assuming it: on a host, capture the bus for the whole window (usbmon, or Wireshark's USB capture) and keep the capture beside this record; on a charger there is no host to prove anything about, and that is the simpler arm for SILENCE and the weaker one for everything else -- no bus capture, no journal to read, and so no reboot instrument at all -- which is why that arm owes a supply that can be shown not to have dropped, a logging supply or a current trace kept beside this record, and answers INCONCLUSIVE without one. THE OBSERVABLE IS THE LED, and the board produces it alone -- no host, no finger, nothing held open. One render task per backend is spawned on the high-priority executor at firmware/src/main.rs:1025 (ws2812, the default), firmware/src/main.rs:963 (gpio) or firmware/src/main.rs:971 (pimoroni), and each loops on an alarm it re-arms for as long as the board has power: firmware/src/led.rs:618 and firmware/src/led.rs:727 are 5 ms, firmware/src/led.rs:692 is the gpio soft-PWM's 2 ms period. One of those -- or the worker's 16 ms button poll, firmware/src/worker.rs:307 -- is the earliest deadline in the queue at every instant of the run, so the arm that straddles each crossing is one of them and nothing has to be arranged for it to be. What a camera sees is the render: the ambient effect is a ~2 s breathing cycle once a host has configured the device and a twinkle before that, and the gpio and pimoroni backends blink 500 ms on, 500 ms off in both of those states. Record it end to end -- a camera with a running clock in frame, or a photodiode into a logging ADC. SAMPLE WELL ABOVE THE AMBIENT CADENCE, ten frames a second or better, and not the one frame a second the run's length makes tempting: the cadence is 0.5 s on the blinking backends, and a sampler near that rate aliases into a constant, which reads as the FAIL below rather than as an instrument that was too slow. WHAT THIS RECORD DOES NOT YET HAVE, said the way PLAT-FLASH-001 says it. The crossing is not announced by the device, so it is located by arithmetic over the recording's own clock rather than pinned to a device event, and the run therefore proves the ABSENCE of a stall across a window that certainly contains a boundary rather than pinning the survival to the boundary itself. The device's own clock IS readable, and the first version of this record was wrong to say that no instrument in this tree reports the device's uptime: every audit-journal entry is stamped with the ms-since-attach of firmware/src/usb_attach.rs:34-36 -- firmware/src/worker.rs:469 is where the dispatch hands it over -- and tools/rsk/audit.py:170 prints it as the `uptime` column. But reading it costs a command, and a command inside the window is the traffic that masks the defect, so it BRACKETS the run instead of sampling it -- and THE CLOSING STEP HAS TO WRITE, which the first version of this sentence got wrong: enumerate, `rsk audit enable` (PIN and one touch, before the window opens), go quiet, close with `rsk audit disable` (crates/rsk-fido/src/vendor.rs:518 appends the EV_AUDIT_CFG before the flag clears) or with `rsk audit verify` (crates/rsk-fido/src/journal.rs:559 appends an EV_CHECKPOINT; that arm additionally needs a provisioned OTP DEVK, so `disable` is the one every board can run), and only THEN `rsk audit log`, whose newest entry is what dates the run on the device's own counter as well as on the host's. A READ-ONLY CLOSE DATES NOTHING. AUDIT_READ appends no entry at all -- crates/rsk-fido/src/vendor.rs:481 is a bare `journal::vendor_read` -- so after a quiet window the newest entry is still the PRE-WINDOW enable, carrying the uptime it had then. And `EV_BOOT` is appended LAZILY, on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside the window followed by a read-only close writes nothing and the exported window is BYTE-IDENTICAL with and without one. MEASURED against this tree's own journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only close, newest `uptime` 1000 ms, and the rebooted run byte-identical to the quiet one; writing close, newest `uptime` 8590935 ms on the quiet run against a second `EV_BOOT` and 4294967 ms on the rebooted one. An uptime the device volunteers with no command behind it, or a boundary it signals on its own, is the second instrument this row still owes, and it is the one that would turn this from an absence into a location.""" boot_config = """The DEFAULT image, and this time with no deviation from the shipped configuration at all -- the run needs no finger and no ceremony, so the no-touch build the first version asked for is not merely unnecessary, it is the build with nothing left to observe. Both halves of what is under test are set by this tree's own build: firmware/Cargo.toml enables embassy-rp's `time-driver`, which is what fixes the tick at 1 MHz and so fixes the comparator's period, and firmware/src/main.rs:524 takes `embassy_rp::config::Config::default()`, whose clk_ref is XOSC at 12 MHz. A build that changed either would be a different period and a different run. TWO THINGS THE IMAGE MUST NOT BE. Not `LED_KIND=none`, which compiles no render task at all and so removes the only observable an unattended board has; the default is `ws2812`, and gpio and pimoroni serve here equally. And not a board whose stored LED configuration has been dimmed to zero or put in steady mode, because both stop the render from changing while the alarms underneath it keep running, and this run reads the render. The factory `EF_LED_CONF` is what the expectation below is written against.""" expected = """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.""" outcome = "planned" diff --git a/assurance/board/PLAT-TIMER-003.toml b/assurance/board/PLAT-TIMER-003.toml index 313db82ec..0ba144cd5 100644 --- a/assurance/board/PLAT-TIMER-003.toml +++ b/assurance/board/PLAT-TIMER-003.toml @@ -22,7 +22,7 @@ # INCONCLUSIVE, because a comparator whose counter has stopped can be observed # neither to miss a match nor to make one. assumption = "PLAT-TIMER-003" -method = """Take PLAT-TIMER-002's run -- a DEFAULT-image board powered and LEFT ALONE for at least 8589.934592 s with its LED recorded end to end -- and read the SAME series for a second question: did the render ever stop and stay stopped. TWO CONDITIONS THIS QUESTION ADDS TO THAT RUN, and neither is hygiene. NO DEBUGGER ATTACHED: TIMER0 carries a DBGPAUSE register whose own words are `Set bits high to enable pause when the corresponding debug ports are active`, so a probe that halts a core is a DOCUMENTED way to stop this very counter, and a run taken with one attached observes the probe instead of the silicon. AND A SUPPLY THAT DOES NOT DROP for the whole window: a brown-out reboots the board, and a reboot restarts the counter and repaints the render, which on the recording reads as a run that never froze. THE READING IS ARITHMETIC over the recording's own clock, the same clock that record locates its crossings by -- find the longest interval in which the sampled LED holds one value, and ask whether anything changed after it. Sample as that record says, ten frames a second or better and not the one frame a second the run's length makes tempting, for the same reason there and a sharper one here: a sampler near the ambient cadence aliases into a constant, and here that manufactures the FAIL out of an instrument that was too slow. THE DEVICE'S OWN CLOCK IS THE SECOND WITNESS, and for this row it is worth more than a date stamp. firmware/src/main.rs:800 stamps the origin at boot, immediately before the USB pull-up; firmware/src/usb_attach.rs:34-36 is the milliseconds since it, the clock the FIDO layer measures every window against; tools/rsk/audit.py:170 prints it as the `uptime` column. So a counter that stopped for an interval reports an uptime SHORTER than the wall-clock length of the recording, whether or not it restarted, and a board that rebooted reports one shorter still. Reading it costs a command, and a command inside the window is the traffic PLAT-TIMER-002 refuses, so it BRACKETS the run exactly as it does there, and THE CLOSING STEP IS A COMMAND THAT WRITES: enumerate, `rsk audit enable` (PIN and one touch) before the window opens, go quiet, then `rsk audit disable` -- or `rsk audit verify`, which additionally needs a provisioned OTP DEVK -- and only THEN `rsk audit log`. A READ-ONLY CLOSE CANNOT PRODUCE THIS ROW'S PASS AT ALL, and that is the defect this sentence carried until 2026-09-05. AUDIT_READ appends nothing (crates/rsk-fido/src/vendor.rs:481), so after a quiet window the newest entry is the PRE-WINDOW enable, its `uptime` is materially shorter than the recording ON A PERFECTLY HEALTHY BOARD, and the PASS below was unreachable by construction. The confound the witness exists to exclude was invisible in the same breath: `EV_BOOT` is appended lazily on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside a read-only window writes nothing and the exported window is byte-identical with and without one. MEASURED against this tree's journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only, newest `uptime` 1000 ms and the rebooted run byte-identical; closing with the write, 8590935 ms on the quiet run and, on the rebooted one, a SECOND `EV_BOOT` and 4294967 ms. On the charger arm there is no host to ask and no journal to read, and what stands in for the second witness is a supply that can be shown not to have dropped.""" +method = """Take PLAT-TIMER-002's run -- a DEFAULT-image board powered and LEFT ALONE for at least 8589.934592 s with its LED recorded end to end -- and read the SAME series for a second question: did the render ever stop and stay stopped. TWO CONDITIONS THIS QUESTION ADDS TO THAT RUN, and neither is hygiene. NO DEBUGGER ATTACHED: TIMER0 carries a DBGPAUSE register whose own words are `Set bits high to enable pause when the corresponding debug ports are active`, so a probe that halts a core is a DOCUMENTED way to stop this very counter, and a run taken with one attached observes the probe instead of the silicon. AND A SUPPLY THAT DOES NOT DROP for the whole window: a brown-out reboots the board, and a reboot restarts the counter and repaints the render, which on the recording reads as a run that never froze. THE READING IS ARITHMETIC over the recording's own clock, the same clock that record locates its crossings by -- find the longest interval in which the sampled LED holds one value, and ask whether anything changed after it. Sample as that record says, ten frames a second or better and not the one frame a second the run's length makes tempting, for the same reason there and a sharper one here: a sampler near the ambient cadence aliases into a constant, and here that manufactures the FAIL out of an instrument that was too slow. THE DEVICE'S OWN CLOCK IS THE SECOND WITNESS, and for this row it is worth more than a date stamp. firmware/src/main.rs:803 stamps the origin at boot, immediately before the USB pull-up; firmware/src/usb_attach.rs:34-36 is the milliseconds since it, the clock the FIDO layer measures every window against; tools/rsk/audit.py:170 prints it as the `uptime` column. So a counter that stopped for an interval reports an uptime SHORTER than the wall-clock length of the recording, whether or not it restarted, and a board that rebooted reports one shorter still. Reading it costs a command, and a command inside the window is the traffic PLAT-TIMER-002 refuses, so it BRACKETS the run exactly as it does there, and THE CLOSING STEP IS A COMMAND THAT WRITES: enumerate, `rsk audit enable` (PIN and one touch) before the window opens, go quiet, then `rsk audit disable` -- or `rsk audit verify`, which additionally needs a provisioned OTP DEVK -- and only THEN `rsk audit log`. A READ-ONLY CLOSE CANNOT PRODUCE THIS ROW'S PASS AT ALL, and that is the defect this sentence carried until 2026-09-05. AUDIT_READ appends nothing (crates/rsk-fido/src/vendor.rs:481), so after a quiet window the newest entry is the PRE-WINDOW enable, its `uptime` is materially shorter than the recording ON A PERFECTLY HEALTHY BOARD, and the PASS below was unreachable by construction. The confound the witness exists to exclude was invisible in the same breath: `EV_BOOT` is appended lazily on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside a read-only window writes nothing and the exported window is byte-identical with and without one. MEASURED against this tree's journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only, newest `uptime` 1000 ms and the rebooted run byte-identical; closing with the write, 8590935 ms on the quiet run and, on the rebooted one, a SECOND `EV_BOOT` and 4294967 ms. On the charger arm there is no host to ask and no journal to read, and what stands in for the second witness is a supply that can be shown not to have dropped.""" boot_config = """PLAT-TIMER-002's, unchanged, because it is the same run on the same image: the DEFAULT build, firmware/src/main.rs:524's `embassy_rp::config::Config::default()`, and a stored `EF_LED_CONF` still at the factory look. The same three images are refused for the same reason and it is sharper here -- `LED_KIND=none` compiles no render task, brightness zero paints nothing, steady mode stops the frame changing while the alarms underneath it keep running -- and each of those is an image in which the LED holds one value for the whole run with the counter in perfect health, which is this row's FAIL signature exactly. A run on any of them observes an absent instrument and answers INCONCLUSIVE, never FAIL.""" expected = """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.""" outcome = "planned" diff --git a/assurance/deleters.toml b/assurance/deleters.toml index 7d7aedfac..67d8b5046 100644 --- a/assurance/deleters.toml +++ b/assurance/deleters.toml @@ -522,7 +522,7 @@ why = "the site this audit was about: PIV key fids carry EF_META heads, so the r [[site]] file = "crates/rsk-piv/src/lib.rs" -line = 858 +line = 867 call = "return match fs.delete(fid) {" verb = "delete" answer = "read" @@ -533,7 +533,7 @@ why = "PUT DATA with an empty body IS the object delete, so the removal is the w [[site]] file = "crates/rsk-piv/src/lib.rs" -line = 1172 +line = 1181 call = "let _ = fs.delete(tofid);" verb = "delete" answer = "discarded" @@ -544,7 +544,7 @@ why = "clearing the destination's certificate when the source has none. A public [[site]] file = "crates/rsk-piv/src/lib.rs" -line = 1207 +line = 1216 call = "let dropped = fs.delete_key(key_fid(from));" verb = "delete_key" answer = "read" @@ -555,7 +555,7 @@ why = "MOVE with to = 0xFF, the slot delete. The head earns a retry because one [[site]] file = "crates/rsk-piv/src/lib.rs" -line = 1208 +line = 1217 call = "let _ = fs.delete(pubkey_fid(from));" verb = "delete" answer = "discarded" @@ -566,7 +566,7 @@ why = "the source's cached public point. Heads live on key_fid alone, so this fi [[site]] file = "crates/rsk-piv/src/lib.rs" -line = 1210 +line = 1219 call = "let _ = fs.delete(f);" verb = "delete" answer = "discarded" diff --git a/assurance/platform.toml b/assurance/platform.toml index eb3efd252..e62595ed1 100644 --- a/assurance/platform.toml +++ b/assurance/platform.toml @@ -622,7 +622,7 @@ supports = ["SEC-FIDO-001", "SEC-FIDO-002", "SEC-TRANS-001"] [[assumption]] id = "PLAT-THREAT-002" class = "threat-model" -statement = "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." +statement = "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:1337`), without a DEK behind it." discharge = "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." discharge_owner = "contributor" status = "pending" @@ -1061,7 +1061,7 @@ depends_on = ["PLAT-TIMER-003"] id = "PLAT-TIMER-003" class = "timers" statement = "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." -discharge = "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." +discharge = "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:1025, firmware/src/main.rs:963 or firmware/src/main.rs:971; 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." discharge_owner = "maintainer" status = "pending" failure_direction = "split, and the security half is the one PLAT-TIMER-002 does not have. A stopped counter WEDGES everything that awaits a `Timer` — the LED render, the worker's 16 ms button poll (firmware/src/worker.rs:307), and any open presence wait, whose crates/rsk-device/src/presence.rs:215 busy poll then compares a frozen `now_us` against its timeout for ever — and that is availability, the comparator's direction. But the windows measured on command ARRIVAL do not wedge, they stop counting: the pinUvAuthToken's rolling and absolute caps are `saturating_sub` over a millisecond count that no longer grows, so a grant minted before the stop never retires, while the USB stack, which is interrupt-driven rather than timer-driven, goes on answering. A live grant that outlives its cap is security, and silently. Not an ambiguity but a rule: what AWAITS a timer wedges, what SUBTRACTS two clock readings freezes open" diff --git a/crates/rsk-piv/src/ccc.rs b/crates/rsk-piv/src/ccc.rs new file mode 100644 index 000000000..4ebf73f46 --- /dev/null +++ b/crates/rsk-piv/src/ccc.rs @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// Copyright (C) 2026 RS-Key contributors + +//! Default CCC (Card Capability Container, PIV object `5FC107`) — a **mandatory** +//! PIV object (SP 800-73-4 pt1 §3.1.1) this card previously held only if a host +//! had written one. Serving a default mirrors the CHUID path, so the object a +//! Windows key-container open reads is present on a freshly flashed card. Shape +//! is Table 8 in table order: mandatory elements only, `F0`/`F1`/`F2` +//! zero-length (§3.1.1 allows it and defines no PIV values for them), `F5` +//! carrying the data model number `0x10` (Appendix A), unused optional elements +//! absent. A host `PUT DATA` still overrides it — `get_data` reads flash first. + +/// The nine wire bytes; see the module docs for each element's Table 8 origin. +pub(crate) const CCC: [u8; 9] = [0xF0, 0x00, 0xF1, 0x00, 0xF2, 0x00, 0xF5, 0x01, 0x10]; + +#[cfg(test)] +#[path = "ccc_tests.rs"] +mod tests; diff --git a/crates/rsk-piv/src/ccc_tests.rs b/crates/rsk-piv/src/ccc_tests.rs new file mode 100644 index 000000000..1fc578602 --- /dev/null +++ b/crates/rsk-piv/src/ccc_tests.rs @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: AGPL-3.0-only +// Copyright (C) 2026 RS-Key contributors + +use super::*; + +#[test] +fn wire_bytes_are_the_spec_shape() { + // The exact nine bytes, pinned as a literal so the constant cannot move the + // test with it: F0/F1/F2 zero-length (the spec defines no PIV values), F5 + // the data model number — the one element §3.1.1 requires to carry a value. + assert_eq!(CCC, [0xF0, 0x00, 0xF1, 0x00, 0xF2, 0x00, 0xF5, 0x01, 0x10]); +} + +#[test] +fn is_wellformed_tlv_in_table_order() { + // Table 8 order, mandatory elements only; unused optional elements absent. + let mut i = 0; + for (tag, len) in [(0xF0u8, 0usize), (0xF1, 0), (0xF2, 0), (0xF5, 1)] { + assert_eq!(CCC[i], tag, "tag at {i}"); + assert_eq!(CCC[i + 1] as usize, len, "len at {i}"); + i += 2 + len; + } + assert_eq!(i, CCC.len(), "TLVs must cover the whole object exactly"); +} diff --git a/crates/rsk-piv/src/lib.rs b/crates/rsk-piv/src/lib.rs index 36e960a6b..d1922011f 100644 --- a/crates/rsk-piv/src/lib.rs +++ b/crates/rsk-piv/src/lib.rs @@ -13,6 +13,7 @@ extern crate alloc; mod auth; +mod ccc; mod chuid; pub mod files; pub mod info; @@ -120,6 +121,7 @@ const INS_IMPORT_ASYM: u8 = 0xFE; const INS_SET_MGMKEY: u8 = 0xFF; const CHUID_ID: u32 = 0x5FC102; +const CCC_ID: u32 = 0x5FC107; /// PivmanData (ADMIN DATA) TLV: outer `0x80 { 0x81 = flags, 0x82 = derived-key /// salt, 0x83 = PIN-change timestamp }`; flag bit `0x02` means the management key /// is PIN-protected (a host reads it back from PRINTED). ykman writes the salt @@ -751,6 +753,13 @@ impl PivApplet<'_> { obj[..synth.len()].copy_from_slice(&synth); synth.len() } + // CCC is mandatory (SP 800-73-4 pt1 §3.1.1): a fresh card serves + // the synthesized default too, so a Windows key-container open finds + // the object. A real PUT DATA still wins the read above. + _ if id == CCC_ID => { + obj[..ccc::CCC.len()].copy_from_slice(&ccc::CCC); + ccc::CCC.len() + } _ => return Sw::FILE_NOT_FOUND, }; if push_tlv(res, TAG_DATA_OBJECT, &obj[..n]).is_err() { diff --git a/crates/rsk-piv/src/tests.rs b/crates/rsk-piv/src/tests.rs index 16f8cf3b3..bc02dd7dd 100644 --- a/crates/rsk-piv/src/tests.rs +++ b/crates/rsk-piv/src/tests.rs @@ -1445,15 +1445,16 @@ fn the_pin_read_condition_objects_are_not_world_readable() { CARDHOLDER_IRIS_IMAGES_ID, ]; // The controls include each gated id's immediate neighbours, so an off-by-one - // in `read_needs_pin` cannot pass. CHUID is a weak control on its own — it - // answers OK even when absent (the Windows synthesis) — hence the rest. + // in `read_needs_pin` cannot pass. CHUID and CCC are weak controls on their + // own — both answer OK even when absent (synthesized defaults) — hence the + // rest. let ungated = [ CHUID_ID, 0x5FC101u32, 0x5FC102, 0x5FC104, 0x5FC105, - 0x5FC107, + CCC_ID, 0x5FC10A, 0x5FC10B, 0x5FC10C, @@ -4359,6 +4360,54 @@ fn chuid_synthesized_on_fresh_card() { assert_eq!(&body[29..45], &HASH[..16]); } +#[test] +fn ccc_synthesized_on_fresh_card_and_put_wins() { + // The CCC is mandatory (SP 800-73-4 pt1 §3.1.1). A card that answers 6A82 + // for it made a Windows certificate login fail with "the keyset does not + // exist" when CAPI opened the key container; a fresh card serves the + // synthesized default, and a host PUT still overrides it. + let rng = RefCell::new(TestRng(7)); + let pres = RefCell::new(AlwaysConfirm); + let mut app = PivApplet::new(SERIAL, HASH, None, &rng, &pres); + let mut fs = new_fs(); + select(&mut app, &mut fs); + let (sw, obj) = run( + &mut app, + &mut fs, + INS_GET_DATA, + 0x3F, + 0xFF, + &[0x5C, 0x03, 0x5F, 0xC1, 0x07], + ); + assert_eq!(sw, Sw::OK); + // The wire anchor, as a literal: routing through the arm is not enough to + // pin the bytes (see ccc_tests.rs for the shape's Table 8 derivation). + assert_eq!( + find_tag(&obj, 0x53).unwrap(), + &[0xF0, 0x00, 0xF1, 0x00, 0xF2, 0x00, 0xF5, 0x01, 0x10] + ); + // A host-written CCC persists at the same fid and wins the read (PUT DATA + // needs the management key, as for every object). + auth_mgm(&mut app, &mut fs); + let host = [0xF5u8, 0x01, 0x10, 0xFE, 0x00]; + let mut put = vec![0x5C, 0x03, 0x5F, 0xC1, 0x07, 0x53, host.len() as u8]; + put.extend_from_slice(&host); + assert_eq!( + run(&mut app, &mut fs, INS_PUT_DATA, 0x3F, 0xFF, &put).0, + Sw::OK + ); + let (sw, obj) = run( + &mut app, + &mut fs, + INS_GET_DATA, + 0x3F, + 0xFF, + &[0x5C, 0x03, 0x5F, 0xC1, 0x07], + ); + assert_eq!(sw, Sw::OK); + assert_eq!(find_tag(&obj, 0x53).unwrap(), &host); +} + #[test] fn pin_metadata_shapes() { let rng = RefCell::new(TestRng(7)); diff --git a/docs/guides/piv.md b/docs/guides/piv.md index b97105971..2defd7ef6 100644 --- a/docs/guides/piv.md +++ b/docs/guides/piv.md @@ -12,8 +12,10 @@ identify the card by its applet, not the reader name, so they work on the defaul build. > **Windows note:** the card serves a default CHUID automatically — the Windows -> PIV minidriver needs it to enumerate the certificate containers, so no manual -> `ykman piv objects generate chuid` step is required. +> PIV minidriver needs it to enumerate the certificate containers — and the +> mandatory Card Capability Container (`5FC107`) on the same terms, so neither +> `ykman piv objects generate chuid` nor `ykman piv objects generate ccc` is +> required on firmware 0x09DB or later. Prereqs: on Linux, `pcscd` plus the polkit rule from [linux.md](../linux.md); if you also use GnuPG, the `disable-ccid` line so `scdaemon` and `pcscd` stop diff --git a/docs/platform-assumptions.md b/docs/platform-assumptions.md index 7d787151c..5a52434a2 100644 --- a/docs/platform-assumptions.md +++ b/docs/platform-assumptions.md @@ -99,10 +99,10 @@ Which sites go under which row is not the registry's to choose alone. `docs/unsa | `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-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:1337`), 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-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:1025, firmware/src/main.rs:963 or firmware/src/main.rs:971; 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` | diff --git a/docs/protocol.md b/docs/protocol.md index 0d7e6f137..4fded906c 100644 --- a/docs/protocol.md +++ b/docs/protocol.md @@ -507,6 +507,11 @@ needs only the identifiers above. RS-Key implements: the CHUID (`5FC102`) returns a synthesized default (non-federal FASC-N + a device-stable GUID = `sha256(serial)[..16]`) when the host has not written one, so the Windows minidriver can enumerate the card; a host-written CHUID overrides it. + The Card Capability Container (`5FC107`, mandatory per SP 800-73-4 pt1 §3.1.1) + is served on the same terms: with no host-written object the card answers a + 9-byte synthesized default (`F0 00 F1 00 F2 00 F5 01 10` — zero-length mandatory + elements plus the PIV data model number `0x10`) instead of `6A82`, a host + `PUT DATA` overrides it, and an empty `PUT DATA` falls back to the default again. - **OATH**: Yubico OATH (TOTP/HOTP). - **OTP**: Yubico OTP / HOTP keyboard + CCID. - **OpenPGP card 3.x.** PUT DATA C1/C2/C3 changes a slot's algorithm diff --git a/docs/windows.md b/docs/windows.md index 5839ccd18..adae32ed2 100644 --- a/docs/windows.md +++ b/docs/windows.md @@ -97,11 +97,15 @@ See [ssh.md](guides/ssh.md) for the WebAuthn/OpenSSH details. via the minidriver). Recent firmware aligns the OpenPGP card serial with the device serial the other applets report; older firmware showed a divergent OpenPGP serial. -- **PIV certificates unusable / signing "pending" under CAPI (CryptoAPI):** the - Windows PIV minidriver enumerates the card's containers from its CHUID. Recent - firmware serves a default CHUID automatically, so a freshly flashed card is - usable; on older firmware, provision one with `ykman piv objects generate chuid`. - (The RSA/EC signing itself is unaffected — it matches a real YubiKey byte-for-byte.) +- **PIV certificates unusable / signing "pending" under CAPI (CryptoAPI), or a + certificate login failing with `NTE_BAD_KEYSET` ("the keyset does not exist"):** + the Windows inbox PIV minidriver enumerates the card's containers from its CHUID + and reads the mandatory Card Capability Container (`5FC107`) while opening one. + Firmware 0x09DB and later serves both automatically, so a freshly flashed card is + usable; on older firmware, provision them (`ykman piv objects generate chuid`, + `ykman piv objects generate ccc`). A Yubico-VID build avoids the inbox minidriver + entirely — Yubico's own does not ask for the container object. (The RSA/EC signing + itself is unaffected — it matches a real YubiKey byte-for-byte.) - **PicoForge / a PC/SC tool cannot connect until re-plug:** another program is holding the single reader. Close it (PicoForge, Kleopatra, a stray `gpg`), or unplug and re-plug. `gpgconf --kill scdaemon` releases a `gpg`-held handle. diff --git a/firmware/src/main.rs b/firmware/src/main.rs index 4b4d4e5ca..00b84e25a 100644 --- a/firmware/src/main.rs +++ b/firmware/src/main.rs @@ -714,7 +714,10 @@ async fn main(spawner: Spawner) { config.max_power = 100; config.max_packet_size_0 = 64; // bcdDevice build counter; also surfaced on the trusted-display Firmware screen. - let device_release: u16 = 0x09DA; + // 0x09DB: PIV serves a synthesized Card Capability Container (`5FC107`, + // mandatory per SP 800-73-4 pt1 §3.1.1) where it previously answered 6A82 — + // the object a Windows key-container open reads. + let device_release: u16 = 0x09DB; config.device_release = device_release; let mut builder = Builder::new( diff --git a/formal/README.md b/formal/README.md index 65cc080bc..cbe45103d 100644 --- a/formal/README.md +++ b/formal/README.md @@ -352,7 +352,7 @@ back the same way: |---|---|---| | `crates/rsk-fs/src/lib.rs:62` | `request_rescrub` → `()`: the at-rest lap is never re-armed | `BugRekeyKeepsTheMarker`, RED on `MarkerNeverLies` | | `crates/rsk-oath/src/lib.rs:1226` | `deselect` → `()`: the VALIDATE unlock outlives its selection | `BugSelectKeepsOtherApplet`, RED on `NoStatusOutsideItsSelection` | -| `crates/rsk-piv/src/lib.rs:391` | `deselect` → `()`: the verified PIN outlives its selection | the same | +| `crates/rsk-piv/src/lib.rs:368` | `deselect` → `()`: the verified PIN outlives its selection | the same | That is **model-catches** three times: a defect the suite could not tell from correct code, on a line carrying the property's own tag, which the model reddens. @@ -416,7 +416,7 @@ whole seam module is about was handed to nobody who looked. #### The ninth row, and the column number that decided it -`crates/rsk-piv/src/lib.rs:1323` `&&` → `||` is the sharpest thing this pass has +`crates/rsk-piv/src/lib.rs:1332` `&&` → `||` is the sharpest thing this pass has produced. The PIV PIN gate ends in ```rust @@ -1415,10 +1415,10 @@ share — one flash, one button — appears here as events (`FactoryWipe`, | Invariant | What it asserts | The Rust that owns it | |---|---|---| -| `NoStatusOutsideItsSelection` | An applet holds a security status only while it is the **selected** applet. Structural — it reads straight out of the state | `crates/rsk-sdk/src/applet.rs:374-390` (the one place that decides what a selection does to the applet that was current) · `crates/rsk-piv/src/lib.rs:199-203` · `crates/rsk-openpgp/src/pin.rs:81-94` · `crates/rsk-oath/src/lib.rs:1224-1228` · `crates/rsk-device/src/ccid.rs:354-369` (the ICC power transition) | -| `NoStatusAfterARefusedAuth` | A reference whose authentication was just refused is not authenticated | `crates/rsk-piv/src/lib.rs:183-186` · `crates/rsk-openpgp/src/pin.rs:190-202` · `crates/rsk-oath/src/lib.rs:1160-1161` | +| `NoStatusOutsideItsSelection` | An applet holds a security status only while it is the **selected** applet. Structural — it reads straight out of the state | `crates/rsk-sdk/src/applet.rs:374-390` (the one place that decides what a selection does to the applet that was current) · `crates/rsk-piv/src/lib.rs:201-205` · `crates/rsk-openpgp/src/pin.rs:81-94` · `crates/rsk-oath/src/lib.rs:1224-1228` · `crates/rsk-device/src/ccid.rs:354-369` (the ICC power transition) | +| `NoStatusAfterARefusedAuth` | A reference whose authentication was just refused is not authenticated | `crates/rsk-piv/src/lib.rs:185-188` · `crates/rsk-openpgp/src/pin.rs:190-202` · `crates/rsk-oath/src/lib.rs:1160-1161` | | `NoKeyOpOnTheAdminStatus` | No key operation runs on a status its own specification does not name | `crates/rsk-openpgp/src/pso.rs:80-92` · `crates/rsk-openpgp/src/internalaut.rs:45-48` · `crates/rsk-piv/src/auth.rs:57-65`, `:113-117` | -| `ReselectPreservesAccessStatus` | A re-SELECT of the same AID changes no access status. **A conformance claim, labelled as one** | `crates/rsk-piv/src/lib.rs:365-368` · `crates/rsk-openpgp/src/lib.rs:354-357` | +| `ReselectPreservesAccessStatus` | A re-SELECT of the same AID changes no access status. **A conformance claim, labelled as one** | `crates/rsk-piv/src/lib.rs:367-370` · `crates/rsk-openpgp/src/lib.rs:354-357` | | `AccessCodeRemovalNeedsTheCode` | Removing the OATH access code needs the validated status the code bought. **A step rule — its violation produces exactly the exempt code-less state, so no state predicate can see it** | `crates/rsk-oath/src/lib.rs:330-332` (the shared gate) · `:337-349` (the removal path) | The fourth one points the other way from the first three and that is why it is @@ -1437,8 +1437,8 @@ direction it actually goes. | Command | What a refusal costs | The authority | The mutant | |---|---|---|---| -| PIV `VERIFY` | `has_pin` **and** `pin_fresh` (`crates/rsk-piv/src/lib.rs:183-186` is the only writer of either) | the applet's own session discipline | `NoStatusAfterARefusedAuth` | -| PIV `CHANGE REFERENCE DATA` / `RESET RETRY COUNTER` | **nothing** — it takes no `&mut Session` at all (`crates/rsk-piv/src/lib.rs:543-577`) | SP 800-73-4 pt 2 §3.2.2/§3.2.3, plus a measured YubiKey 5.7.4 | `BugPivChangeResetsStatus`, RED in 46 | +| PIV `VERIFY` | `has_pin` **and** `pin_fresh` (`crates/rsk-piv/src/lib.rs:185-188` is the only writer of either) | the applet's own session discipline | `NoStatusAfterARefusedAuth` | +| PIV `CHANGE REFERENCE DATA` / `RESET RETRY COUNTER` | **nothing** — it takes no `&mut Session` at all (`crates/rsk-piv/src/lib.rs:545-579`) | SP 800-73-4 pt 2 §3.2.2/§3.2.3, plus a measured YubiKey 5.7.4 | `BugPivChangeResetsStatus`, RED in 46 | | OpenPGP `VERIFY` / `CHANGE` | exactly the **addressed** reference, keyed on the FID compared rather than on P2 (`crates/rsk-openpgp/src/pin.rs:190-202`, `:267-269`) | OpenPGP 3.4.1, and the `RESET RETRY COUNTER` case that compares `EF_RC` while passing `p2 = 0x81` | `NoStatusAfterARefusedAuth` | | OATH OTP-PIN `CHANGE` | **both** flags (`crates/rsk-oath/src/lib.rs:1160-1161`) | `aa47867` — before it the whole retry budget could be burned through the door that did not close | `BugFailedChangeKeepsStatus` | | OATH access-code `VALIDATE` | **nothing** — the standing unlock survives (`crates/rsk-oath/src/lib.rs:540-542`) | a MAC challenge-response has no retry counter for a refusal to protect; a YubiKey 5.7.4 measured keeping it from a genuinely locked applet | `BugRefusedValidateDropsUnlock`, RED in 46 | @@ -1673,9 +1673,9 @@ seam modules keep, so a switch is one real thing a reviewer could break: | Mutation switch | Removes | Target invariant | Caught in | |---|---|---|---| -| `BugUseWhenBlocked` | the `left == 0 => PIN_BLOCKED` floor (`crates/rsk-piv/src/lib.rs:1292-1294` / `crates/rsk-openpgp/src/pin.rs:232-234`), which guards a direct verify AND a recovery reference | `NoAuthWhenBlocked` | 30 states | -| `BugWrongDoesNotSpend` | the decrement that IS the gate (`crates/rsk-piv/src/lib.rs:1312` / `crates/rsk-openpgp/src/pin.rs:139`) | `WrongAttemptIsCharged` | 2 states | -| `BugRecoveryWithoutSecret` | the recovery secret verified before the refill (`crates/rsk-piv/src/lib.rs:1447` / `crates/rsk-openpgp/src/pin.rs:898`) | `BudgetRisesOnlyWithItsSecret` | 9 states | +| `BugUseWhenBlocked` | the `left == 0 => PIN_BLOCKED` floor (`crates/rsk-piv/src/lib.rs:520-522` / `crates/rsk-openpgp/src/pin.rs:232-234`), which guards a direct verify AND a recovery reference | `NoAuthWhenBlocked` | 30 states | +| `BugWrongDoesNotSpend` | the decrement that IS the gate (`crates/rsk-piv/src/lib.rs:1321` / `crates/rsk-openpgp/src/pin.rs:139`) | `WrongAttemptIsCharged` | 2 states | +| `BugRecoveryWithoutSecret` | the recovery secret verified before the refill (`crates/rsk-piv/src/lib.rs:1456` / `crates/rsk-openpgp/src/pin.rs:898`) | `BudgetRisesOnlyWithItsSecret` | 9 states | `Lattice.cfg` is **GREEN, exhaustive** over 243 distinct states at depth 11, with no dead action; every `LatSolo_*.cfg` is RED on its own target. The all-blocked diff --git a/formal/RSKeyAppletSeams.tla b/formal/RSKeyAppletSeams.tla index b4403fb86..59711b35a 100644 --- a/formal/RSKeyAppletSeams.tla +++ b/formal/RSKeyAppletSeams.tla @@ -138,7 +138,7 @@ VARIABLES sel, \* Dispatcher::current (crates/rsk-sdk/src/applet.rs:145) held, \* [Refs -> BOOLEAN]: the in-RAM security statuses \* PIV's `pin_fresh` -- the UNSPENT half of `has_pin`, which a PIN-policy - \* ALWAYS key operation consumes (crates/rsk-piv/src/lib.rs:165-179). The + \* ALWAYS key operation consumes (crates/rsk-piv/src/lib.rs:167-181). The \* only status here that is a two-part thing. fresh, \* Whether OATH has an access code provisioned. It decides what a SELECT @@ -198,7 +198,7 @@ Init == /\ viol = {} \* Every status an applet owns, gone. This is `Session::reset` -\* (crates/rsk-piv/src/lib.rs:199-203), `pin::Session::reset` +\* (crates/rsk-piv/src/lib.rs:201-205), `pin::Session::reset` \* (crates/rsk-openpgp/src/pin.rs:81-94) and OATH's `deselect` \* (crates/rsk-oath/src/lib.rs:1224-1228) -- three functions, one meaning. ClearedFor(h, a) == @@ -269,9 +269,9 @@ SelectOther(a) == (* disagree about what a refusal costs -- see the invariant's comment. *) (***************************************************************************) -\* PIV VERIFY (crates/rsk-piv/src/lib.rs:521-535): success sets has_pin AND +\* PIV VERIFY (crates/rsk-piv/src/lib.rs:523-537): success sets has_pin AND \* pin_fresh, refusal clears both, through `Session::set_pin` -\* (crates/rsk-piv/src/lib.rs:183-186) which is the only writer of either. +\* (crates/rsk-piv/src/lib.rs:185-188) which is the only writer of either. PivVerify(ok) == /\ sel = Piv /\ held' = [held EXCEPT !["pivPin"] = ok] @@ -282,7 +282,7 @@ PivVerify(ok) == /\ UNCHANGED << sel, oneShotSig, psig, oathCodeSet, viol >> \* PIV CHANGE REFERENCE DATA / RESET RETRY COUNTER take no `&mut Session` at all -\* (crates/rsk-piv/src/lib.rs:543-577), so a refused change costs the standing +\* (crates/rsk-piv/src/lib.rs:545-579), so a refused change costs the standing \* status NOTHING. Deliberate, and settled by measurement rather than taste: \* SP 800-73-4 pt2 3.2.2/3.2.3 say the security status is unchanged and a real \* YubiKey keeps it. @@ -650,7 +650,7 @@ NoKeyOpOnTheAdminStatus == \* THE OTHER HALF OF THE REFUSAL RULE, and it points the opposite way: two \* refusals must cost NOTHING, and each is settled by its own authority rather \* than by a cross-applet principle. PIV's CHANGE REFERENCE DATA takes no -\* `&mut Session` at all (crates/rsk-piv/src/lib.rs:543-577) -- SP 800-73-4 pt2 +\* `&mut Session` at all (crates/rsk-piv/src/lib.rs:545-579) -- SP 800-73-4 pt2 \* 3.2.2/3.2.3, plus a measured YubiKey 5.7.4. OATH's access-code VALIDATE keeps \* the standing unlock (crates/rsk-oath/src/lib.rs:540-542), because a MAC \* challenge-response has no retry counter for a refusal to protect. diff --git a/formal/RSKeyBootHardening.tla b/formal/RSKeyBootHardening.tla index 9c6b5bc10..3922e2b54 100644 --- a/formal/RSKeyBootHardening.tla +++ b/formal/RSKeyBootHardening.tla @@ -21,7 +21,7 @@ (* FIVE lazy re-keys skipping that, and its sweep landed the CALL at *) (* crates/rsk-fido/src/clientpin.rs:811-813, *) (* crates/rsk-fido/src/clientpin.rs:1210-1213, *) -(* crates/rsk-piv/src/lib.rs:1336, crates/rsk-oath/src/lib.rs:1206, *) +(* crates/rsk-piv/src/lib.rs:621, crates/rsk-oath/src/lib.rs:1206, *) (* crates/rsk-openpgp/src/pin.rs:330 -- three of those five used to name *) (* the comment or the write ABOVE the call, which is what a mechanical *) (* re-number leaves behind. Run-35's five is a HISTORICAL set, not *) diff --git a/formal/RSKeyRetryLattice.tla b/formal/RSKeyRetryLattice.tla index 016e1d574..4e24752d0 100644 --- a/formal/RSKeyRetryLattice.tla +++ b/formal/RSKeyRetryLattice.tla @@ -40,18 +40,18 @@ EXTENDS Naturals CONSTANTS Max, \* the retry ceiling; models MAX_PIN_RETRIES / the per-reference default \* The `left == 0 => PIN_BLOCKED` floor, checked BEFORE the comparison at - \* crates/rsk-piv/src/lib.rs:1292-1294 (check_ref) and + \* crates/rsk-piv/src/lib.rs:520-522 (check_ref) and \* crates/rsk-openpgp/src/pin.rs:232-234 (check_pin). One switch: the same \* floor guards a direct verify AND a recovery reference (the PUK/RC that \* check_ref/check_pin is called on), so removing it opens both. BugUseWhenBlocked, - \* The decrement that IS the anti-bruteforce gate: crates/rsk-piv/src/lib.rs:1312 + \* The decrement that IS the anti-bruteforce gate: crates/rsk-piv/src/lib.rs:1321 \* (`set_retries_left(fs, retry, left - 1)`, spent BEFORE the compare) and \* crates/rsk-openpgp/src/pin.rs:139 (`pw[idx] -= 1`). Removing it lets a wrong \* attempt cost nothing -- unlimited guesses at full speed. BugWrongDoesNotSpend, \* The recovery reference verified BEFORE the target is refilled: - \* crates/rsk-piv/src/lib.rs:1447 (`check_ref(EF_PUK, ..)` opens + \* crates/rsk-piv/src/lib.rs:1456 (`check_ref(EF_PUK, ..)` opens \* unblock_pin_with_puk) and crates/rsk-openpgp/src/pin.rs:898 (`check_pin(EF_RC, \* ..)` opens reset_retry's P1=0 branch). Removing it refills the target on a \* WRONG recovery secret. @@ -67,7 +67,7 @@ Refs == {"pivPin", "pivPuk", "pw1", "pw3", "rc"} \* The references a host VERIFY targets directly. `pivPuk` and `rc` are absent: \* neither is verified on its own, only PRESENTED as the recovery secret inside a -\* RESET RETRY (crates/rsk-piv/src/lib.rs:580-587, crates/rsk-openpgp/src/pin.rs:875-925), +\* RESET RETRY (crates/rsk-piv/src/lib.rs:582-589, crates/rsk-openpgp/src/pin.rs:875-925), \* where a wrong one still spends its counter. VerifyTargets == {"pivPin", "pw1", "pw3"} @@ -103,7 +103,7 @@ Init == /\ viol = {} (***************************************************************************) -(* VERIFY. crates/rsk-piv/src/lib.rs:1287-1354 (check_ref) and *) +(* VERIFY. crates/rsk-piv/src/lib.rs:1296-1363 (check_ref) and *) (* crates/rsk-openpgp/src/pin.rs:209-300 (check_pin): refuse at zero, spend *) (* on a wrong value, refill on a correct one. *) (***************************************************************************) diff --git a/formal/citations.lock b/formal/citations.lock index 116e53291..8153545ba 100644 --- a/formal/citations.lock +++ b/formal/citations.lock @@ -29,9 +29,9 @@ assurance/board/PLAT-TIMER-002.toml firmware/src/led.rs 618-618 Timer::after_mil assurance/board/PLAT-TIMER-002.toml firmware/src/led.rs 692-692 const PERIOD_US: u64 = 2000; const PERIOD_US: u64 = 2000; assurance/board/PLAT-TIMER-002.toml firmware/src/led.rs 727-727 Timer::after_millis(5).await; Timer::after_millis(5).await; assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 524-524 let mut config = embassy_rp::config::Config::default(); let mut config = embassy_rp::config::Config::default(); -assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 960-960 hp.spawn(led::gpio_task(led).unwrap()); hp.spawn(led::gpio_task(led).unwrap()); -assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 968-968 hp.spawn(led::pimoroni_task(rg, b).unwrap()); hp.spawn(led::pimoroni_task(rg, b).unwrap()); -assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 1022-1022 hp.spawn(led::ws2812_task(ws2812).unwrap()); hp.spawn(led::ws2812_task(ws2812).unwrap()); +assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 963-963 hp.spawn(led::gpio_task(led).unwrap()); hp.spawn(led::gpio_task(led).unwrap()); +assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 971-971 hp.spawn(led::pimoroni_task(rg, b).unwrap()); hp.spawn(led::pimoroni_task(rg, b).unwrap()); +assurance/board/PLAT-TIMER-002.toml firmware/src/main.rs 1025-1025 hp.spawn(led::ws2812_task(ws2812).unwrap()); hp.spawn(led::ws2812_task(ws2812).unwrap()); assurance/board/PLAT-TIMER-002.toml firmware/src/presence.rs 237-240 #[cfg(feature = "no-touch")] } assurance/board/PLAT-TIMER-002.toml firmware/src/usb_attach.rs 34-36 /// Milliseconds since the attach — the clock the FIDO layer gets as `Ctx::now_ms`, pub fn elapsed_ms() -> u64 { assurance/board/PLAT-TIMER-002.toml firmware/src/worker.rs 307-307 const BTN_POLL_MS: u64 = 16; const BTN_POLL_MS: u64 = 16; @@ -41,7 +41,7 @@ assurance/board/PLAT-TIMER-002.toml tools/rsk/audit.py 170-170 print(f"{'seq':>6 assurance/board/PLAT-TIMER-003.toml crates/rsk-fido/src/journal.rs 215-217 if !ctx.state.audit_boot_logged { let _ = raw_append(&ctx.dev, ctx.fs, ctx.now_ms, EV_BOOT, 0, &[]); assurance/board/PLAT-TIMER-003.toml crates/rsk-fido/src/vendor.rs 481-481 journal::vendor_read(ctx, out) journal::vendor_read(ctx, out) assurance/board/PLAT-TIMER-003.toml firmware/src/main.rs 524-524 let mut config = embassy_rp::config::Config::default(); let mut config = embassy_rp::config::Config::default(); -assurance/board/PLAT-TIMER-003.toml firmware/src/main.rs 800-800 usb_attach::mark(); usb_attach::mark(); +assurance/board/PLAT-TIMER-003.toml firmware/src/main.rs 803-803 usb_attach::mark(); usb_attach::mark(); assurance/board/PLAT-TIMER-003.toml firmware/src/pin_lock.rs 54-54 rp_pac::WATCHDOG.scratch2().write_value(encode(lock)); rp_pac::WATCHDOG.scratch2().write_value(encode(lock)); assurance/board/PLAT-TIMER-003.toml firmware/src/usb_attach.rs 34-36 /// Milliseconds since the attach — the clock the FIDO layer gets as `Ctx::now_ms`, pub fn elapsed_ms() -> u64 { assurance/board/PLAT-TIMER-003.toml scripts/platform_gate.py 1337-1337 OUTCOME_STATUS = {"pass": "discharged", "fail": "refuted"} OUTCOME_STATUS = {"pass": "discharged", "fail": "refuted"} @@ -491,7 +491,7 @@ assurance/platform.toml crates/rsk-openpgp/src/pin.rs 277-277 if let Err(sw) = m assurance/platform.toml crates/rsk-openpgp/src/pin.rs 340-340 if n < 1 || blob[0] != DEK_FORMAT_V3 { if n < 1 || blob[0] != DEK_FORMAT_V3 { assurance/platform.toml crates/rsk-openpgp/src/pin.rs 775-775 rec[1] = PIN_FORMAT_V1; rec[1] = PIN_FORMAT_V1; assurance/platform.toml crates/rsk-otp/src/seal.rs 55-55 pub fn seal_put( pub fn seal_put( -assurance/platform.toml crates/rsk-piv/src/lib.rs 1328-1328 // kbase-migration fallback: the correct PIN against a verifier stored // kbase-migration fallback: the correct PIN against a verifier stored +assurance/platform.toml crates/rsk-piv/src/lib.rs 1337-1337 // kbase-migration fallback: the correct PIN against a verifier stored // kbase-migration fallback: the correct PIN against a verifier stored assurance/platform.toml crates/rsk-store/src/lib.rs 88-88 matches!(fid, 0xC000 | 0xC001 | 0x0093 | 0xCC01) matches!(fid, 0xC000 | 0xC001 | 0x0093 | 0xCC01) assurance/platform.toml crates/rsk-store/src/lib.rs 145-152 /// Removes from BOTH partitions, not just the one [`is_counter_fid`] routes to. /// the second call finds nothing and costs one ring walk. assurance/platform.toml crates/rsk-store/src/lib.rs 179-181 let main_done = for_each_in(&mut self.main, &mut self.buf, f); main_done && counter_done @@ -525,9 +525,9 @@ assurance/platform.toml firmware/src/main.rs 601-601 let mut trng_cfg = TrngConf assurance/platform.toml firmware/src/main.rs 602-608 // The default sample_count (25) is too low for some RP2350 ROSC units: the // unchanged — the NIST health checks stay enabled, the source is unchanged. assurance/platform.toml firmware/src/main.rs 609-609 trng_cfg.sample_count = 1000; trng_cfg.sample_count = 1000; assurance/platform.toml firmware/src/main.rs 610-610 let trng = Trng::new(p.TRNG, Irqs, trng_cfg); let trng = Trng::new(p.TRNG, Irqs, trng_cfg); -assurance/platform.toml firmware/src/main.rs 960-960 hp.spawn(led::gpio_task(led).unwrap()); hp.spawn(led::gpio_task(led).unwrap()); -assurance/platform.toml firmware/src/main.rs 968-968 hp.spawn(led::pimoroni_task(rg, b).unwrap()); hp.spawn(led::pimoroni_task(rg, b).unwrap()); -assurance/platform.toml firmware/src/main.rs 1022-1022 hp.spawn(led::ws2812_task(ws2812).unwrap()); hp.spawn(led::ws2812_task(ws2812).unwrap()); +assurance/platform.toml firmware/src/main.rs 963-963 hp.spawn(led::gpio_task(led).unwrap()); hp.spawn(led::gpio_task(led).unwrap()); +assurance/platform.toml firmware/src/main.rs 971-971 hp.spawn(led::pimoroni_task(rg, b).unwrap()); hp.spawn(led::pimoroni_task(rg, b).unwrap()); +assurance/platform.toml firmware/src/main.rs 1025-1025 hp.spawn(led::ws2812_task(ws2812).unwrap()); hp.spawn(led::ws2812_task(ws2812).unwrap()); assurance/platform.toml firmware/src/presence.rs 99-101 /// User presence via BOOTSEL (default) or a dedicated GPIO button. pub struct ButtonPresence { assurance/platform.toml firmware/src/presence.rs 137-137 const _: () = assert!(embassy_time::TICK_HZ == 1_000_000); const _: () = assert!(embassy_time::TICK_HZ == 1_000_000); assurance/platform.toml firmware/src/presence.rs 163-166 #[cfg(not(feature = "display"))] pub type Presence = crate::display::TouchPresence; @@ -785,15 +785,15 @@ formal/README.md crates/rsk-piv/src/auth.rs 57-65 /// skips the PIN; listing kno formal/README.md crates/rsk-piv/src/auth.rs 63-63 PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh, PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh, formal/README.md crates/rsk-piv/src/auth.rs 113-117 /// nothing clears the PIN's own status — 9B included, hence `is_key`. self.sess.pin_fresh = false; formal/README.md crates/rsk-piv/src/files.rs 513-513 if deleted > RESET_MAX_DELETES { if deleted > RESET_MAX_DELETES { -formal/README.md crates/rsk-piv/src/lib.rs 183-186 fn set_pin(&mut self, verified: bool) { } -formal/README.md crates/rsk-piv/src/lib.rs 199-203 self.clear_challenge(); pub struct PivApplet<'a> { -formal/README.md crates/rsk-piv/src/lib.rs 365-368 if !reselect { // The default PIN/PUK/retry/mgmt/attestation files are provisioned once -formal/README.md crates/rsk-piv/src/lib.rs 391-391 self.sess.reset(); self.sess.reset(); -formal/README.md crates/rsk-piv/src/lib.rs 543-577 // the retry counter … shall be decremented by one." A YubiKey 5.7.4 does /// `6A88` for anything but `P1 = 00, P2 = 80`, as on `change_pin` — and here -formal/README.md crates/rsk-piv/src/lib.rs 1292-1294 Err(sw) => return sw, if left == 0 { -formal/README.md crates/rsk-piv/src/lib.rs 1312-1312 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { -formal/README.md crates/rsk-piv/src/lib.rs 1323-1323 && ct_eq( && ct_eq( -formal/README.md crates/rsk-piv/src/lib.rs 1447-1447 puk: &[u8], puk: &[u8], +formal/README.md crates/rsk-piv/src/lib.rs 185-188 fn set_pin(&mut self, verified: bool) { } +formal/README.md crates/rsk-piv/src/lib.rs 201-205 self.clear_challenge(); pub struct PivApplet<'a> { +formal/README.md crates/rsk-piv/src/lib.rs 367-370 if !reselect { // The default PIN/PUK/retry/mgmt/attestation files are provisioned once +formal/README.md crates/rsk-piv/src/lib.rs 368-368 self.sess.reset(); self.sess.reset(); +formal/README.md crates/rsk-piv/src/lib.rs 520-522 Err(sw) => return sw, if left == 0 { +formal/README.md crates/rsk-piv/src/lib.rs 545-579 // the retry counter … shall be decremented by one." A YubiKey 5.7.4 does /// `6A88` for anything but `P1 = 00, P2 = 80`, as on `change_pin` — and here +formal/README.md crates/rsk-piv/src/lib.rs 1321-1321 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { +formal/README.md crates/rsk-piv/src/lib.rs 1332-1332 && ct_eq( && ct_eq( +formal/README.md crates/rsk-piv/src/lib.rs 1456-1456 puk: &[u8], puk: &[u8], formal/README.md crates/rsk-rescue/src/lib.rs 141-143 /// Refines `RSKeyAdminSurface!PrivilegedOpNeedsPresence` — SEC-ADM-002. self.presence.borrow_mut().request(confirm) == Presence::Confirmed formal/README.md crates/rsk-sdk/src/applet.rs 208-210 fn selectable(&self, i: usize) -> bool { } formal/README.md crates/rsk-sdk/src/applet.rs 374-390 // answered to the AID SP 800-85A-4 C.1.1.2 names as invalid. A YubiKey { @@ -873,11 +873,11 @@ formal/RSKeyAppletSeams.tla crates/rsk-openpgp/src/pin.rs 267-269 // comparison, formal/RSKeyAppletSeams.tla crates/rsk-openpgp/src/putdata.rs 59-65 pub fn write_authorized(sess: &Session, fid: u16) -> bool { } formal/RSKeyAppletSeams.tla crates/rsk-piv/src/auth.rs 57-65 /// skips the PIN; listing known gated values made unknown bytes ungated. } formal/RSKeyAppletSeams.tla crates/rsk-piv/src/auth.rs 113-117 /// nothing clears the PIN's own status — 9B included, hence `is_key`. self.sess.pin_fresh = false; -formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 165-179 /// A private-key operation at any PIN-gated slot spends this one alone impl Session { -formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 183-186 fn set_pin(&mut self, verified: bool) { } -formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 199-203 self.clear_challenge(); pub struct PivApplet<'a> { -formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 521-535 return Sw::PIN_BLOCKED; // the oracle's order too. -formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 543-577 // the retry counter … shall be decremented by one." A YubiKey 5.7.4 does /// `6A88` for anything but `P1 = 00, P2 = 80`, as on `change_pin` — and here +formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 167-181 /// A private-key operation at any PIN-gated slot spends this one alone impl Session { +formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 185-188 fn set_pin(&mut self, verified: bool) { } +formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 201-205 self.clear_challenge(); pub struct PivApplet<'a> { +formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 523-537 return Sw::PIN_BLOCKED; // the oracle's order too. +formal/RSKeyAppletSeams.tla crates/rsk-piv/src/lib.rs 545-579 // the retry counter … shall be decremented by one." A YubiKey 5.7.4 does /// `6A88` for anything but `P1 = 00, P2 = 80`, as on `change_pin` — and here formal/RSKeyAppletSeams.tla crates/rsk-sdk/src/applet.rs 145-145 apdu.ins == 0xA4 && apdu.p1 == 0x04 && (apdu.p2 == 0x00 || apdu.p2 == 0x04) apdu.ins == 0xA4 && apdu.p1 == 0x04 && (apdu.p2 == 0x00 || apdu.p2 == 0x04) formal/RSKeyAppletSeams.tla crates/rsk-sdk/src/applet.rs 222-230 /// { formal/RSKeyAppletSeams.tla crates/rsk-sdk/src/applet.rs 374-390 // answered to the AID SP 800-85A-4 C.1.1.2 names as invalid. A YubiKey { @@ -892,7 +892,7 @@ formal/RSKeyBootHardening.tla crates/rsk-fs/src/lib.rs 80-98 /// Run the one-sho formal/RSKeyBootHardening.tla crates/rsk-fs/src/lib.rs 99-99 if fs.compact().is_ok() { if fs.compact().is_ok() { formal/RSKeyBootHardening.tla crates/rsk-oath/src/lib.rs 1206-1206 if rsk_fs::request_rescrub(fs).is_ok() { if rsk_fs::request_rescrub(fs).is_ok() { formal/RSKeyBootHardening.tla crates/rsk-openpgp/src/pin.rs 330-330 rsk_fs::request_rescrub(fs).map_err(|_| Sw::MEMORY_FAILURE)?; rsk_fs::request_rescrub(fs).map_err(|_| Sw::MEMORY_FAILURE)?; -formal/RSKeyBootHardening.tla crates/rsk-piv/src/lib.rs 1336-1336 if rsk_fs::request_rescrub(fs).is_err() { if rsk_fs::request_rescrub(fs).is_err() { +formal/RSKeyBootHardening.tla crates/rsk-piv/src/lib.rs 621-621 if rsk_fs::request_rescrub(fs).is_err() { if rsk_fs::request_rescrub(fs).is_err() { formal/RSKeyBootHardening.tla firmware/src/pin_lock.rs 18-21 //! a real power cycle clears it. The *whole* lock moves: carrying the engaged flag //! formal/RSKeyBootHardening.tla firmware/src/pin_lock.rs 36-37 const TAG: u32 = 0x5253_4B00; const TAG_MASK: u32 = 0xFFFF_FF00; formal/RSKeyBootHardening.tla firmware/src/pin_lock.rs 52-54 /// Refines `RSKeyBootHardening!TheWholeLockRides` — SEC-BOOT-002. rp_pac::WATCHDOG.scratch2().write_value(encode(lock)); @@ -903,11 +903,11 @@ formal/RSKeyRetryLattice.tla crates/rsk-openpgp/src/pin.rs 669-669 let mut fid = formal/RSKeyRetryLattice.tla crates/rsk-openpgp/src/pin.rs 875-925 /// resetting code (P1=0x00) or via a verified admin PIN (P1=0x02). Both re-seal return match result { formal/RSKeyRetryLattice.tla crates/rsk-openpgp/src/pin.rs 898-898 if data.len() <= rc_len { if data.len() <= rc_len { formal/RSKeyRetryLattice.tla crates/rsk-openpgp/src/pin.rs 930-930 if p1 != 0x02 { if p1 != 0x02 { -formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 580-587 fn reset_retry(&mut self, dev: &Device, fs: &mut Fs, apdu: &Apdu) -> Sw { unblock_pin_with_puk(dev, fs, puk, new) -formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1287-1354 /// Refines `RSKeyRetryLattice!NoAuthWhenBlocked` — SEC-LAT-001. Sw::retries(left) -formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1292-1294 Err(sw) => return sw, if left == 0 { -formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1312-1312 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { -formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1447-1447 puk: &[u8], puk: &[u8], +formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 520-522 Err(sw) => return sw, if left == 0 { +formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 582-589 fn reset_retry(&mut self, dev: &Device, fs: &mut Fs, apdu: &Apdu) -> Sw { unblock_pin_with_puk(dev, fs, puk, new) +formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1296-1363 /// Refines `RSKeyRetryLattice!NoAuthWhenBlocked` — SEC-LAT-001. Sw::retries(left) +formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1321-1321 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { +formal/RSKeyRetryLattice.tla crates/rsk-piv/src/lib.rs 1456-1456 puk: &[u8], puk: &[u8], formal/RSKeySecurityState.tla crates/rsk-device/src/ctap.rs 202-205 backup_sealed_record: fs.has_data(EF_BACKUP_SEALED), credential_slots_raw: credentials.iter().filter(|present| **present).count() as u16, formal/RSKeySecurityState.tla crates/rsk-device/src/ctap.rs 354-361 // Persist the clientPIN soft lock across a warm reboot. It is RAM-only, and a .store_pin_lock(self.fido_state.borrow().pin_lock()); formal/RSKeySecurityState.tla crates/rsk-device/src/presence.rs 25-26 /// No host request in flight: an on-panel (local) flow owns the button. pub const SCOPE_NONE: u8 = 0; @@ -1149,15 +1149,15 @@ formal/comutants.toml crates/rsk-otp/src/tests.rs 2217-2217 assert_ne!( assert_n formal/comutants.toml crates/rsk-piv/src/auth.rs 63-63 PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh, PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh, formal/comutants.toml crates/rsk-piv/src/auth.rs 115-119 fn spend_pin(&mut self) { } formal/comutants.toml crates/rsk-piv/src/keygen.rs 600-600 if !sess.has_mgm { if !sess.has_mgm { -formal/comutants.toml crates/rsk-piv/src/lib.rs 183-186 fn set_pin(&mut self, verified: bool) { } -formal/comutants.toml crates/rsk-piv/src/lib.rs 288-288 if p1 != 0x00 || !self.sess.has_mgm || !is_key(p2) { if p1 != 0x00 || !self.sess.has_mgm || !is_key(p2) { -formal/comutants.toml crates/rsk-piv/src/lib.rs 390-392 fn deselect(&mut self, _fs: &mut Fs) { } -formal/comutants.toml crates/rsk-piv/src/lib.rs 594-594 if !self.sess.has_mgm || !self.sess.has_pin { if !self.sess.has_mgm || !self.sess.has_pin { -formal/comutants.toml crates/rsk-piv/src/lib.rs 676-676 if !self.sess.has_mgm { if !self.sess.has_mgm { -formal/comutants.toml crates/rsk-piv/src/lib.rs 804-804 if !self.sess.has_mgm { if !self.sess.has_mgm { -formal/comutants.toml crates/rsk-piv/src/lib.rs 1053-1053 if !self.sess.has_mgm { if !self.sess.has_mgm { -formal/comutants.toml crates/rsk-piv/src/lib.rs 1113-1113 if !self.sess.has_mgm { if !self.sess.has_mgm { -formal/comutants.toml crates/rsk-piv/src/lib.rs 1312-1312 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { +formal/comutants.toml crates/rsk-piv/src/lib.rs 185-188 fn set_pin(&mut self, verified: bool) { } +formal/comutants.toml crates/rsk-piv/src/lib.rs 290-290 if p1 != 0x00 || !self.sess.has_mgm || !is_key(p2) { if p1 != 0x00 || !self.sess.has_mgm || !is_key(p2) { +formal/comutants.toml crates/rsk-piv/src/lib.rs 392-394 fn deselect(&mut self, _fs: &mut Fs) { } +formal/comutants.toml crates/rsk-piv/src/lib.rs 596-596 if !self.sess.has_mgm || !self.sess.has_pin { if !self.sess.has_mgm || !self.sess.has_pin { +formal/comutants.toml crates/rsk-piv/src/lib.rs 678-678 if !self.sess.has_mgm { if !self.sess.has_mgm { +formal/comutants.toml crates/rsk-piv/src/lib.rs 813-813 if !self.sess.has_mgm { if !self.sess.has_mgm { +formal/comutants.toml crates/rsk-piv/src/lib.rs 1062-1062 if !self.sess.has_mgm { if !self.sess.has_mgm { +formal/comutants.toml crates/rsk-piv/src/lib.rs 1122-1122 if !self.sess.has_mgm { if !self.sess.has_mgm { +formal/comutants.toml crates/rsk-piv/src/lib.rs 1321-1321 if set_retries_left(fs, retry, left - 1).is_err() { if set_retries_left(fs, retry, left - 1).is_err() { formal/comutants.toml crates/rsk-sdk/src/applet.rs 227-227 pub fn reset_card(&mut self, applets: &mut [&mut dyn Applet], ctx: &mut C) { pub fn reset_card(&mut self, applets: &mut [&mut dyn Applet], ctx: &mut C) { formal/comutants.toml firmware/src/pin_lock.rs 18-21 //! a real power cycle clears it. The *whole* lock moves: carrying the engaged flag //! formal/comutants.toml firmware/src/worker.rs 397-398 if rsk_mgmt::take_device_reset() && self.ccid.factory_wipe() { self.reboot(1).await; @@ -1179,8 +1179,8 @@ scripts/test_run_tlc.py scripts/verdict_gate.py 619-634 if row["invariant"] is n scripts/test_security_trace.py tools/emu/src/device.rs 754-755 crate::security_trace::POWER_CYCLE, 0, scripts/test_token_refinement_gate.py crates/rsk-device/src/ctap.rs 122-122 *st = rsk_fido::FidoState::new(); *st = rsk_fido::FidoState::new(); scripts/test_token_refinement_gate.py crates/rsk-fido/src/credential.rs 919-919 let fid = EF_RP + i; let fid = EF_RP + i; -scripts/test_token_refinement_gate.py firmware/src/main.rs 1167-1167 let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); +scripts/test_token_refinement_gate.py firmware/src/main.rs 1170-1170 let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); scripts/token_refinement_gate.py crates/rsk-device/src/ctap.rs 122-122 *st = rsk_fido::FidoState::new(); *st = rsk_fido::FidoState::new(); -scripts/token_refinement_gate.py firmware/src/main.rs 1167-1167 let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); +scripts/token_refinement_gate.py firmware/src/main.rs 1170-1170 let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); let fido_state_ref = FIDO_STATE.init(RefCell::new(rsk_fido::FidoState::new())); scripts/trace_map.py crates/rsk-sdk/src/applet.rs 387-387 let reselect = self.current == Some(i); let reselect = self.current == Some(i); tools/emu/src/hid.rs crates/rsk-usb/src/ctaphid.rs 621-634 async fn on_frame(&mut self, f: &[u8; HID_RPT_SIZE]) { } diff --git a/formal/comutants.toml b/formal/comutants.toml index d45541cd3..c59353ca1 100644 --- a/formal/comutants.toml +++ b/formal/comutants.toml @@ -1000,7 +1000,7 @@ replace = """ """ slice = ["cargo", "test", "-p", "rsk-openpgp"] expect = "killed" -note = "spend_pin_retry stops charging the attempt: unlimited PW1/PW3/RC guesses at full speed. Deliberately the OpenPGP half of this switch, so the lattice's three entries cover both applets rather than PIV three times; PIV's twin is the `set_retries_left(fs, retry, left - 1)` at crates/rsk-piv/src/lib.rs:1312." +note = "spend_pin_retry stops charging the attempt: unlimited PW1/PW3/RC guesses at full speed. Deliberately the OpenPGP half of this switch, so the lattice's three entries cover both applets rather than PIV three times; PIV's twin is the `set_retries_left(fs, retry, left - 1)` at crates/rsk-piv/src/lib.rs:1321." [comutant.BugRecoveryWithoutSecret] status = "patch" @@ -1250,7 +1250,7 @@ note = "637ed98 taken back out on the PIV half: every SELECT resets, including t status = "unreachable" evidence = """the applets' deselect is redundant with their own fresh SELECT, so removing it from the ICC power transition changes nothing observable. Three -applets carry an access status and implement deselect — crates/rsk-piv/src/lib.rs:390-392 +applets carry an access status and implement deselect — crates/rsk-piv/src/lib.rs:392-394 (sess.reset), crates/rsk-openpgp/src/lib.rs:337-339 (reset_session), crates/rsk-oath/src/lib.rs:1222-1229 (validated + otp_pin_verified) — and all three ALSO re-lock in select: piv and openpgp on `if !reselect`, oath by recomputing `validated = !code_set` and clearing @@ -1362,7 +1362,7 @@ note = "both layers, as the model's switch has them: the ALWAYS arm stops readin [comutant.BugPinFreshOutlivesPin] status = "unreachable" -evidence = "the clamp is unobservable in today's Rust. `pin_fresh` has exactly one reader — crates/rsk-piv/src/auth.rs:63, `PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh` — and it is CONJOINED with the status it refines, so a freshness that outlives `has_pin` authorises nothing: the guard is already false on the other half. `Session::set_pin` (crates/rsk-piv/src/lib.rs:183-186) is the only writer that sets it TRUE, and `GenAuth::spend_pin` (crates/rsk-piv/src/auth.rs:115-119) only ever sets it false. The first patch here scored a false kill by taking `self.pin_fresh = verified` out of `set_pin`, which is the INVERSE defect — it makes freshness unreachable rather than immortal, fail-closed rather than fail-open, and all 11 failures were 9000-expected-got-6982. The faithful mutant (`if verified { self.pin_fresh = true; }` — grant kept, clamp dropped) measures GREEN over 130 tests. The model keeps `pfresh` as a second requirement-side copy precisely to expose a split the Rust does not have." +evidence = "the clamp is unobservable in today's Rust. `pin_fresh` has exactly one reader — crates/rsk-piv/src/auth.rs:63, `PINPOLICY_ALWAYS => sess.has_pin && sess.pin_fresh` — and it is CONJOINED with the status it refines, so a freshness that outlives `has_pin` authorises nothing: the guard is already false on the other half. `Session::set_pin` (crates/rsk-piv/src/lib.rs:185-188) is the only writer that sets it TRUE, and `GenAuth::spend_pin` (crates/rsk-piv/src/auth.rs:115-119) only ever sets it false. The first patch here scored a false kill by taking `self.pin_fresh = verified` out of `set_pin`, which is the INVERSE defect — it makes freshness unreachable rather than immortal, fail-closed rather than fail-open, and all 11 failures were 9000-expected-got-6982. The faithful mutant (`if verified { self.pin_fresh = true; }` — grant kept, clamp dropped) measures GREEN over 130 tests. The model keeps `pfresh` as a second requirement-side copy precisely to expose a split the Rust does not have." [comutant.BugSigPinNotSpent] status = "patch" @@ -1400,7 +1400,7 @@ replace = """ """ slice = ["cargo", "test", "-p", "rsk-openpgp"] expect = "killed" -note = "the converse of BugAdminOpensKeyOps: a USER status opens PUT DATA's administrative surface. PIV states the same rule at seven separate 9B management-key gates (crates/rsk-piv/src/lib.rs:288, 594, 676, 804, 1053, 1113 and crates/rsk-piv/src/keygen.rs:600), none of them patched here." +note = "the converse of BugAdminOpensKeyOps: a USER status opens PUT DATA's administrative surface. PIV states the same rule at seven separate 9B management-key gates (crates/rsk-piv/src/lib.rs:290, 596, 678, 813, 1062, 1122 and crates/rsk-piv/src/keygen.rs:600), none of them patched here." [comutant.BugRefusedValidateGrants] status = "patch" diff --git a/scripts/test_token_refinement_gate.py b/scripts/test_token_refinement_gate.py index d2f8f8ff3..fcdcaa61c 100644 --- a/scripts/test_token_refinement_gate.py +++ b/scripts/test_token_refinement_gate.py @@ -438,7 +438,7 @@ def test_an_unowned_concrete_site_fails(tree: Tree, body: str, finding: str): "fn stray(gna: &RefCell) {\n" " let mut st = gna.borrow_mut();\n *st = Default::default();\n}\n", # CONTROL for the swap clause: BUILDING a fresh state replaces nothing. - # `firmware/src/main.rs:1167` is exactly this, and a rule reading + # `firmware/src/main.rs:1170` is exactly this, and a rule reading # `FidoState::new` anywhere would own the boot that makes the one cell. "fn stray() { let cell = RefCell::new(FidoState::new()); hand(cell); }\n", ], diff --git a/scripts/token_refinement_gate.py b/scripts/token_refinement_gate.py index cd17004a5..8116ddaf5 100644 --- a/scripts/token_refinement_gate.py +++ b/scripts/token_refinement_gate.py @@ -588,7 +588,7 @@ def discovered_volatile( typed = re.compile(WHOLE_TYPED.format(state=state)) if state else None # `mem::replace(st, FidoState::new())` moves the same bits with no `=` in # sight. Scoped to the swap primitives naming the type, NOT to the type - # anywhere: `RefCell::new(FidoState::new())` at `firmware/src/main.rs:1167` + # anywhere: `RefCell::new(FidoState::new())` at `firmware/src/main.rs:1170` # BUILDS the one session cell at boot and replaces nothing, and a rule reading # `FidoState::new` alone owns it. Measured: this alternative adds 0 sites. swapped = re.compile(SWAP.format(state=state)) if state else None diff --git a/tests/interop/divergences.py b/tests/interop/divergences.py index 762203c8c..08047c6b1 100644 --- a/tests/interop/divergences.py +++ b/tests/interop/divergences.py @@ -128,6 +128,14 @@ def classify(self, real, rsk): ("*.timestamp", Ignore("key generation timestamp")), ("*.guid", Ignore("random GUID")), ("piv.chuid", Ignore("random CHUID/CCC GUID")), + ( + "piv.ccc", + ExpectDiff( + None, + r"f000f100f200f50110", + "RS-Key serves a synthesized CCC; the reference card may serve none or empty", + ), + ), ("oath.deviceId", Ignore("random OATH device id / SELECT salt")), ("*.salt", Ignore("random salt")), ("otp.slot*.publicId", Ignore("Yubico-OTP public id / device serial")),