From 2d035cccd7b53fd5f1e671f951b370a2baf0538b Mon Sep 17 00:00:00 2001 From: Cuihtlauac ALVARADO Date: Thu, 11 Jun 2026 17:19:42 +0200 Subject: [PATCH] docs(backlog): bundle far-future-timestamp fix with re-climbing the ladder to Rung 4 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The far-future request-timestamp replay residual surfaced during PR #35 (by the Extended Rung 4 ReplayWindow model's NoFutureReplay witness). Rewrite the top backlog item so it is explicit that the work is two-part: (1) the code fix in check_freshness / parse_age, and (2) re-discharging every rung that covers the touched code — Rung 1 regression test, Rung 2 freshness property, Rung 3 Kani monotonicity, Rung 4 flipping NoFutureReplay to a held invariant — so assurance returns to the Rung 4 level rather than leaving the proofs trailing the code. Co-Authored-By: Claude Opus 4.8 (1M context) --- backlog.md | 48 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 14 deletions(-) diff --git a/backlog.md b/backlog.md index 636dec4..aa91401 100644 --- a/backlog.md +++ b/backlog.md @@ -6,20 +6,40 @@ the assurance ladder defined in [docs/formalisation-roadmap.md](docs/formalisation-roadmap.md); each names its rung. -## Cap far-future request timestamps (replay-protection gap) - -Surfaced by the Extended Rung 4 `ReplayWindow` TLA+ model. `parse_age` -(`server.rs:146`) clamps a future-dated timestamp to age 0 with **no upper -bound**, so a request dated beyond `REPLAY_RETENTION` into the future passes the -freshness gate indefinitely while its id ages out of `SeenIds` — making it -replayable every retention window *regardless of how large retention is*. The -60s↔120s window relationship does not help here. Low severity (needs the request -onto the channel — SSH pinning guards that — and privileged commands still gate -the first run on a keypress), but for auto-approved unprivileged commands it is a -real repeatable replay. Fix: in `check_freshness` / `parse_age`, reject -timestamps more than a small clock-skew allowance into the future instead of -clamping to age 0; extend the Rung 2 freshness property and the `ReplayWindow` -model's `NoFutureReplay` invariant to cover it. +## Cap far-future request timestamps, then re-climb the ladder to Rung 4 + +The replay-protection residual surfaced **during PR #35** by the Extended Rung 4 +`ReplayWindow` TLA+ model (its `NoFutureReplay` invariant exhibits a concrete +trace). `parse_age` (`server.rs:146`) clamps a future-dated timestamp to age 0 +with **no upper bound**, so a request dated beyond `REPLAY_RETENTION` into the +future passes the freshness gate indefinitely while its id ages out of +`SeenIds` — making it replayable every retention window *regardless of how large +retention is*. The 60s↔120s window relationship does not help here. Low severity +(needs the request onto the channel — SSH pinning guards that — and privileged +commands still gate the first run on a keypress), but for auto-approved +unprivileged commands it is a real repeatable replay. + +**The fix.** In `check_freshness` / `parse_age`, reject timestamps more than a +small clock-skew allowance into the future instead of clamping to age 0. + +**Re-climb the ladder to the same level (Rung 4).** The fix touches code that +several already-discharged rungs cover, so re-establish each so assurance +returns to where PR #35 left it — do *not* leave the proofs trailing the code: + +- **Rung 1 (CI):** the existing gate should stay green; add a regression test + for the rejected far-future timestamp. +- **Rung 2 (property):** extend the freshness property in `src/prop.rs` so it + asserts a sufficiently-future timestamp is *rejected*, not silently fresh. +- **Rung 3 (Kani):** re-drive the `ymd_hms_to_epoch` monotonicity/totality + proofs against the new gate (the bounded-future rejection must stay + panic-free over the full domain). +- **Rung 4 (TLA+):** flip the `ReplayWindow` model's `NoFutureReplay` from a + surfaced-gap witness to a *held* invariant, and re-check the sibling models + are unaffected. + +Done = the code rejects far-future timestamps **and** every rung above is +re-discharged against the fixed code (negative controls re-run where they +exist). ## Rung 5 — Deductive verification of the trusted core