feat: Rung 4 + Extended Rung 4 — TLA+/ProVerif formal models

.github/workflows/proverif.yml

@@ -0,0 +1,51 @@
+name: ProVerif
+
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read
+
+# Cancel superseded runs on the same ref.
+concurrency:
+  group: proverif-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  proverif:
+    name: proverif (Rung 4 SSH channel, informational)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      # ProVerif brings its own toolchain (installed via opam / OCaml),
+      # independent of rust-toolchain.toml, so this does not affect the gating
+      # Rust jobs. m4 expands the single .m4.pv template into the two
+      # configurations.
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: '5'
+      # Refresh the apt index before opam pulls ProVerif's system deps (it
+      # depends on the GTK GUI libs). Without this the runner's mirror
+      # intermittently 404s on a superseded liblzma-dev version pin, which
+      # fails this otherwise non-gating job at install time (seen flapping on
+      # this branch -- same commit passing on one trigger, failing on another).
+      - name: Refresh apt package index
+        run: sudo apt-get update
+      - name: Install ProVerif
+        run: opam install -y proverif
+      # Informational only, like the kani / geiger jobs. Both configurations are
+      # run so the log shows both outcomes. The FIRST-CONTACT run is *expected*
+      # to report query (c) (payload secrecy) false with a key-substitution
+      # attack derivation -- that surfaced gap is the artifact's purpose
+      # (attack-tree leaf 4.2), so the job must not gate on ProVerif's exit code
+      # (continue-on-error + the `|| true` below).
+      - name: Check the SSH-channel model (pinned + first-contact)
+        continue-on-error: true
+        run: |
+          echo '================ PINNED (known_hosts populated) ================'
+          m4 -DPINNED proofs/proverif/ssh-channel.m4.pv > pinned.pv
+          opam exec -- proverif pinned.pv || true
+          echo '================ FIRST CONTACT (no pinning; MITM expected) ====='
+          m4 proofs/proverif/ssh-channel.m4.pv > unpinned.pv
+          opam exec -- proverif unpinned.pv || true

.github/workflows/tlc.yml

@@ -0,0 +1,59 @@
+name: TLC
+
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read
+
+# Cancel superseded runs on the same ref.
+concurrency:
+  group: tlc-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  tlc:
+    name: tlc (Rung 4 TLA+ models, informational)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '21'
+      # TLA+ tools manage their own toolchain (a single jar), independent of
+      # rust-toolchain.toml, so this does not affect the gating Rust jobs. The
+      # committed .tla already contains the pcal.trans translation, so no
+      # PlusCal re-translation step is needed.
+      - name: Fetch TLA+ tools
+        run: |
+          curl -sSL -o tla2tools.jar \
+            https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+      # Informational only, like the kani / geiger jobs: surfaces the Rung 4
+      # model-check in the job log without gating merge while the property set
+      # is still growing. Promote to a required check once stable.
+      - name: Model-check the approval state machine
+        continue-on-error: true
+        run: |
+          java -cp tla2tools.jar tlc2.TLC -nowarning \
+            -config proofs/tla/ApprovalStateMachine.cfg \
+            -workers auto \
+            proofs/tla/ApprovalStateMachine.tla
+      # The Extended Rung 4 freshness <-> replay-retention window-sizing model.
+      - name: Model-check the replay-window sizing
+        continue-on-error: true
+        run: |
+          java -cp tla2tools.jar tlc2.TLC -nowarning \
+            -config proofs/tla/ReplayWindow.cfg \
+            -workers auto \
+            proofs/tla/ReplayWindow.tla
+      # The Extended Rung 4 concurrent-handler interleaving model (shared `seen`
+      # set + TTY lock); checks the atomic try_insert closes the dedup TOCTOU.
+      - name: Model-check the concurrent handlers
+        continue-on-error: true
+        run: |
+          java -cp tla2tools.jar tlc2.TLC -nowarning \
+            -config proofs/tla/ConcurrentHandlers.cfg \
+            -workers auto \
+            proofs/tla/ConcurrentHandlers.tla

README.md

@@ -84,6 +84,7 @@ Each `execute` shows the exact command in the TUI; press `y` to approve,
 - [docs/usage.md](docs/usage.md) — CLI flags, non-privileged mode, SSH tunnels, agent forwarding
 - [docs/protocol.md](docs/protocol.md) — JSON-line wire protocol over the Unix socket
 - [docs/security.md](docs/security.md) — security model; [docs/security-audit.md](docs/security-audit.md) — point-in-time audit; [docs/threat-model.md](docs/threat-model.md) — STRIDE + attack tree; [docs/formalisation-roadmap.md](docs/formalisation-roadmap.md) — graduated-assurance plan; [docs/assurance-case.md](docs/assurance-case.md) — GSN argument
+- [proofs/](proofs/) — machine-checked models: [TLA+/PlusCal approval state machine](proofs/tla/) (TLC, Rung 4) and [ProVerif SSH-channel model](proofs/proverif/) (Rung 4); Kani bounded proofs live in [src/proofs.rs](src/proofs.rs) (Rung 3)
 - [docs/pkexec.md](docs/pkexec.md) — `--pkexec` mode and polkit auth caching (not recommended)
 - [docs/architecture.md](docs/architecture.md) — source layout and implementation status
 - [docs/comparison.md](docs/comparison.md) — how sudo-proxy relates to other tools

backlog.md

@@ -6,14 +6,20 @@ the assurance ladder defined in
 [docs/formalisation-roadmap.md](docs/formalisation-roadmap.md); each names its
 rung.
 
-## Rung 4 — Protocol-level models
-
-TLA+/PlusCal or Alloy model of the approval + `confirm_unprivileged` policy state
-machine: replay impossible, no exec without approval, policy flag transitions
-only on an interactive keypress (pins down the F2 / attack-tree leaf 1.4/4.4
-residual). Tamarin/ProVerif model of the SSH path to make the channel
-assumptions explicit and surface the first-contact MITM gap (attack-tree leaf
-4.2 / assumption A4).
+## 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.
 
 ## Rung 5 — Deductive verification of the trusted core