fix(kms-auth)!: make policy revocation cover every selectable epoch

.github/workflows/halmos.yml

@@ -0,0 +1,60 @@
+# SPDX-FileCopyrightText: © 2025 Phala Network <dstack@phala.network>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+name: KMS Auth-ETH Halmos
+
+on:
+  push:
+    paths:
+      - 'dstack/kms/auth-eth/**'
+      - '.github/workflows/halmos.yml'
+  pull_request:
+    paths:
+      - 'dstack/kms/auth-eth/**'
+      - '.github/workflows/halmos.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  halmos:
+    name: ${{ matrix.contract }}
+    runs-on: ubuntu-latest
+    timeout-minutes: 40
+    strategy:
+      fail-fast: false
+      matrix:
+        contract:
+          - DstackAppSymbolicTest
+          - DstackAppEpochSymbolicTest
+          - DstackKmsSymbolicTest
+          - DstackKmsEpochSymbolicTest
+    defaults:
+      run:
+        working-directory: dstack/kms/auth-eth
+    env:
+      # Halmos does not support the vm.deployCode that dynamic test linking emits.
+      FOUNDRY_DYNAMIC_TEST_LINKING: 'false'
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Checkout contract dependencies
+        working-directory: .
+        run: |
+          git submodule update --init --recursive --depth 1 -- \
+            dstack/kms/auth-eth/lib/forge-std \
+            dstack/kms/auth-eth/lib/openzeppelin-contracts-upgradeable \
+            dstack/kms/auth-eth/lib/openzeppelin-foundry-upgrades
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: v1.8.4
+
+      - name: Install Halmos
+        run: pipx install halmos==0.3.3
+
+      - name: Run Halmos
+        run: halmos --contract ${{ matrix.contract }}

docs/app-key-epochs.md

@@ -53,28 +53,44 @@ epochs. For an image handover, explicitly approve the new image in the old row s
 it can migrate old keys, approve it in the new row, and remove the old image from
 the old row after the handover. The old image never needs access to the new row.
 
-Existing `DstackKms` add/remove methods (OS images, KMS aggregated MRs, KMS
-devices) operate on every root row from the current epoch through the latest
-**registered** one, so a removal during a rotation revokes the material in both
-the serving and the pending row, and an addition allows it in both. Before any
-root epoch is registered, they operate on epoch zero. `DstackApp` add/remove
-methods, and `setAllowAnyDevice`, likewise operate on the current app epoch and
-the next one. The `*AtEpoch(epoch, material)` methods select a particular
-registered root epoch, or a historical, current or next app epoch; removal
-affects only that row. `setAllowAnyDeviceAtEpoch(epoch, allowed)` is also
-row-specific. Single-material add/remove scripts in `Manage.s.sol` accept optional
-`ROOT_EPOCH` or `APP_EPOCH` variables, respectively, as does `SetAllowAnyDevice`.
+A request may select any epoch up to the current one and is decided on that
+epoch's row, so a value is revoked only once every row allowing it is cleared.
+Neither contract has epoch-less material setters: `*AtEpoch(epoch, material)`
+changes one row and `*AtEpochs(fromEpoch, toEpoch, material)` every row in the
+range, so one transaction revokes a value from all rows, with
+`remove*AtEpochs(0, latest, …)` in `DstackKms` and
+`remove*AtEpochs(0, currentAppEpoch, …)` in `DstackApp`. `DstackKms` writes
+registered root epochs (before any is registered, only epoch zero); `DstackApp`
+writes app epochs up to the next one, as do `setAllowAnyDeviceAtEpoch(s)`.
+`DstackApp` reports these setters as the ERC-165 interface
+`IAppEpochManagement` and no longer reports `IAppAuthBasicManagement`
+(`0x8fd37527`), whose epoch-less setters it removed. The scripts in
+`Manage.s.sol` take `ROOT_EPOCH` or `APP_EPOCH` for one row, or
+`FROM_ROOT_EPOCH`/`TO_ROOT_EPOCH` and `FROM_APP_EPOCH`/`TO_APP_EPOCH` for a range,
+and fail without them.
+
+App policies deployed before app epochs (v0.5.x, v0.6.0) keep working with an
+upgraded `DstackKms` and KMS: they report no `IAppEpochAuth`, so `authorizeApp`
+asks their `isAppAllowed` and only for app epoch zero, and `currentAppEpoch`
+reports zero for them. Their owners keep the epoch-less setters until they
+upgrade, which `Manage.s.sol` detects and uses with no epoch or `APP_EPOCH=0`.
+Upgrading keeps their allowlists as app epoch zero. See
+[onchain-governance.md](./onchain-governance.md#apps-deployed-before-app-epochs).
+
+Disk and environment migration after a root rotation fetches the keys of the
+recorded epoch, so a new image migrating old data must be allowed in that old
+row too. Without it the guest stops with an error naming the root and app epoch
+it could not get keys for.
 
 The `*AtEpoch` getters read the selected row, including legacy epoch zero.
 `EpochPolicyChanged` events include the row and the resulting permission. Legacy
 bool getters and events describe **epoch zero only**; changing a nonzero row does
 not change its legacy bool or emit a misleading legacy material event.
-Root policy rows from epoch 1 belong to the epoch's keys: the contract stores
-them under its chain hash, so a row can be written only once the epoch is
-registered (register, prepare the row, then activate). A popped epoch's rows do
-not carry over: other keys registered under the same number start with empty
-rows, which must be prepared again before activation. Epoch 0 keeps the legacy
-mappings.
+Root policy rows from epoch 1 belong to the epoch's registration, so a row can
+be written only once the epoch is registered (register, prepare the row, then
+activate). A popped epoch's rows do not carry over: the next registration of the
+number starts with empty rows, even with the same keys, which must be prepared
+again before activation. Epoch 0 keeps the legacy mappings.
 
 ### KMS keyring handover
 
@@ -91,8 +107,8 @@ This permits staged key distribution without changing which epoch the KMS serves
 ### Upgrading existing proxies
 
 The original bool mappings and `allowAnyDevice` retain their storage locations and
-are used directly as row zero. New nested mappings consume three storage-gap slots
-in each contract; no entries are copied and no reinitializer is required. Existing
+are used directly as row zero. New storage consumes storage-gap slots in each
+contract (four in `DstackKms`, three in `DstackApp`); no entries are copied and no reinitializer is required. Existing
 owners, pending owners, policy flags, root registries and app epoch counters are
 preserved. Even if the pre-upgrade counter is nonzero, old global approvals grant
 only row zero after upgrading: explicitly populate the intended nonzero rows.

docs/formal/key-rotation/EpochPolicy.cfg

@@ -0,0 +1,20 @@
+\* SPDX-FileCopyrightText: © 2026 Phala Network <dstack@phala.network>
+\* SPDX-License-Identifier: Apache-2.0
+
+SPECIFICATION Spec
+CONSTANTS
+    Values = {v1, v2}
+    Keys = {1, 2}
+    MaxEpoch = 2
+    MaxRegistrations = 5
+    KeyByChainHash = FALSE
+    Composes = {c1}
+    MaxAppEpoch = 2
+    LegacyIgnoresAppEpoch = FALSE
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    TypeOK
+    RevocationIsTotal
+    AppKeyMatchesSelectedRow
+PROPERTIES
+    RegistrationStartsEmpty

docs/formal/key-rotation/EpochPolicy.tla

@@ -0,0 +1,166 @@
+\* SPDX-FileCopyrightText: © 2026 Phala Network <dstack@phala.network>
+\* SPDX-License-Identifier: Apache-2.0
+
+----------------------------- MODULE EpochPolicy -----------------------------
+(***************************************************************************)
+(* Epoch-scoped policy of DstackKms and DstackApp, and key release decided *)
+(* on the selected rows.                                                   *)
+(*                                                                         *)
+(* Root side (DstackKms): one row of allowed values (OS images; KMS MRs   *)
+(* and devices alike) per root epoch, written by *AtEpoch(s) over a range *)
+(* of registered rows. A pending epoch can be popped and registered again, *)
+(* with the same or other keys. Rows are keyed by registration            *)
+(* (RootEpoch.registration); KeyByChainHash = TRUE models the earlier     *)
+(* contract, which keyed them by chain hash.                               *)
+(*                                                                         *)
+(* App side (DstackApp): one row of allowed compose hashes per app epoch,  *)
+(* written over a range up to the next epoch. An app policy predating app  *)
+(* epochs (v0.5.x, v0.6.0) has only its flat mapping, which is row 0, and  *)
+(* epoch-less setters writing it; DstackKms authorizes it through          *)
+(* isAppAllowed for app epoch 0 only. Its owner may upgrade it at any      *)
+(* time, keeping the mapping as row 0. LegacyIgnoresAppEpoch = TRUE drops  *)
+(* the app epoch 0 check of that fallback.                                 *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANTS Values, Keys, MaxEpoch, MaxRegistrations, KeyByChainHash,
+          Composes, MaxAppEpoch, LegacyIgnoresAppEpoch
+
+VARIABLES
+    keys,        \* keys of the registered root epochs, epoch e at index e + 1
+    regs,        \* registration of each registered root epoch
+    nextReg,     \* registrations so far
+    cur,         \* current root epoch
+    rows,        \* <<row key, value>> pairs allowed
+    revoked,     \* values removed from every registered row, not added since
+    legacy,      \* the app policy predates app epochs
+    appCur,      \* current app epoch
+    appRows,     \* <<app epoch, compose hash>> pairs allowed
+    appRevoked,  \* compose hashes removed from every app row, not added since
+    leaked,      \* a key released for a revoked value or compose hash
+    mismatched   \* an app key released for an app epoch whose row disallows it
+
+vars == <<keys, regs, nextReg, cur, rows, revoked, legacy, appCur, appRows,
+          appRevoked, leaked, mismatched>>
+rootVars == <<keys, regs, nextReg, cur, rows, revoked>>
+appVars == <<legacy, appCur, appRows, appRevoked>>
+ghostVars == <<leaked, mismatched>>
+
+Latest == Len(keys) - 1
+RowKey(ks, rs, e) == IF KeyByChainHash THEN SubSeq(ks, 1, e + 1) ELSE <<rs[e + 1]>>
+Row(e) == {v \in Values: <<RowKey(keys, regs, e), v>> \in rows}
+AppRow(a) == {c \in Composes: <<a, c>> \in appRows}
+
+Init ==
+    /\ \E k \in Keys: keys = <<k>>
+    /\ regs = <<0>> /\ nextReg = 1 /\ cur = 0
+    /\ rows = {} /\ revoked = {}
+    /\ legacy \in BOOLEAN /\ appCur = 0 /\ appRows = {} /\ appRevoked = {}
+    /\ leaked = {} /\ mismatched = FALSE
+
+\* ---- DstackKms ----
+Register(k) ==
+    /\ Latest < MaxEpoch /\ nextReg < MaxRegistrations
+    /\ keys' = Append(keys, k)
+    /\ regs' = Append(regs, nextReg)
+    /\ nextReg' = nextReg + 1
+    /\ UNCHANGED <<cur, rows, revoked, appVars, ghostVars>>
+
+Activate ==
+    /\ cur < Latest
+    /\ cur' = cur + 1
+    /\ UNCHANGED <<keys, regs, nextReg, rows, revoked, appVars, ghostVars>>
+
+Pop ==
+    /\ Latest > cur
+    /\ keys' = SubSeq(keys, 1, Latest)
+    /\ regs' = SubSeq(regs, 1, Latest)
+    /\ UNCHANGED <<nextReg, cur, rows, revoked, appVars, ghostVars>>
+
+\* add*AtEpochs / remove*AtEpochs(from, to, v); *AtEpoch is from = to.
+Write(from, to, v, allowed) ==
+    /\ from <= to /\ to <= Latest
+    /\ LET written == {<<RowKey(keys, regs, e), v>>: e \in from..to}
+       IN rows' = IF allowed THEN rows \cup written ELSE rows \ written
+    /\ revoked' = IF allowed THEN revoked \ {v}
+                  ELSE IF from = 0 /\ to = Latest THEN revoked \cup {v}
+                  ELSE revoked
+    /\ UNCHANGED <<keys, regs, nextReg, cur, appVars, ghostVars>>
+
+\* ---- DstackApp ----
+AppWrite(from, to, c, allowed) ==
+    /\ ~legacy /\ from <= to /\ to <= appCur + 1
+    /\ LET written == {<<a, c>>: a \in from..to}
+       IN appRows' = IF allowed THEN appRows \cup written ELSE appRows \ written
+    /\ appRevoked' = IF allowed THEN appRevoked \ {c}
+                     ELSE IF from = 0 /\ to = appCur + 1 THEN appRevoked \cup {c}
+                     ELSE appRevoked
+    /\ UNCHANGED <<rootVars, legacy, appCur, ghostVars>>
+
+\* The epoch-less setters of a legacy policy write its only row.
+LegacyWrite(c, allowed) ==
+    /\ legacy
+    /\ appRows' = IF allowed THEN appRows \cup {<<0, c>>} ELSE appRows \ {<<0, c>>}
+    /\ appRevoked' = IF allowed THEN appRevoked \ {c} ELSE appRevoked \cup {c}
+    /\ UNCHANGED <<rootVars, legacy, appCur, ghostVars>>
+
+Upgrade ==
+    /\ legacy /\ legacy' = FALSE
+    /\ UNCHANGED <<rootVars, appCur, appRows, appRevoked, ghostVars>>
+
+Advance ==
+    /\ ~legacy /\ appCur < MaxAppEpoch
+    /\ appCur' = appCur + 1
+    /\ UNCHANGED <<rootVars, legacy, appRows, appRevoked, ghostVars>>
+
+\* ---- Key release ----
+\* kms_serve releases keys of the current epoch at most; the key handover
+\* may carry a registered pending one.
+KmsRelease(op, e, v) ==
+    /\ e <= (IF op = "kms_export_keys" THEN Latest ELSE cur)
+    /\ v \in Row(e)
+    /\ leaked' = IF v \in revoked THEN leaked \cup {<<"root", e, v>>} ELSE leaked
+    /\ UNCHANGED <<rootVars, appVars, mismatched>>
+
+\* app_get_key for root epoch e <= current and app epoch a. A legacy policy
+\* is asked through isAppAllowed, which reads its only row.
+AppRelease(e, a, v, c) ==
+    /\ e <= cur /\ v \in Row(e)
+    /\ IF legacy
+         THEN (a = 0 \/ LegacyIgnoresAppEpoch) /\ c \in AppRow(0)
+         ELSE a <= appCur /\ c \in AppRow(a)
+    /\ leaked' = leaked \cup (IF v \in revoked THEN {<<"root", e, v>>} ELSE {})
+                        \cup (IF c \in appRevoked THEN {<<"app", a, c>>} ELSE {})
+    /\ mismatched' = (mismatched \/ c \notin AppRow(a))
+    /\ UNCHANGED <<rootVars, appVars>>
+
+Next ==
+    \/ Activate \/ Pop \/ Upgrade \/ Advance
+    \/ \E k \in Keys: Register(k)
+    \/ \E from, to \in 0..MaxEpoch, v \in Values, allowed \in BOOLEAN: Write(from, to, v, allowed)
+    \/ \E from, to \in 0..MaxAppEpoch + 1, c \in Composes, allowed \in BOOLEAN: AppWrite(from, to, c, allowed)
+    \/ \E c \in Composes, allowed \in BOOLEAN: LegacyWrite(c, allowed)
+    \/ \E op \in {"kms_serve", "kms_export_keys"}, e \in 0..MaxEpoch, v \in Values: KmsRelease(op, e, v)
+    \/ \E e \in 0..MaxEpoch, a \in 0..MaxAppEpoch, v \in Values, c \in Composes: AppRelease(e, a, v, c)
+
+Spec == Init /\ [][Next]_vars
+
+-----------------------------------------------------------------------------
+TypeOK == cur <= Latest /\ Latest <= MaxEpoch /\ Len(regs) = Len(keys) /\ appCur <= MaxAppEpoch
+          /\ (legacy => appCur = 0)
+
+\* A value or compose hash removed from every row gets no key of any root or
+\* app epoch, for any operation, until it is added again; including through a
+\* root epoch popped and registered again, and across the upgrade of a legacy
+\* app policy.
+RevocationIsTotal == leaked = {}
+
+\* An app key of app epoch a is released only when row a allows the compose
+\* hash; for a legacy policy, only app epoch 0, its flat mapping.
+AppKeyMatchesSelectedRow == ~mismatched
+
+\* A root epoch registration starts with an empty row, whatever its keys.
+RegistrationStartsEmpty ==
+    [][Len(keys') > Len(keys) =>
+        \A v \in Values: <<RowKey(keys', regs', Latest + 1), v>> \notin rows']_vars
+=============================================================================

docs/formal/key-rotation/EpochPolicyChainHash.cfg

@@ -0,0 +1,16 @@
+\* SPDX-FileCopyrightText: © 2026 Phala Network <dstack@phala.network>
+\* SPDX-License-Identifier: Apache-2.0
+
+SPECIFICATION Spec
+CONSTANTS
+    Values = {v1, v2}
+    Keys = {1, 2}
+    MaxEpoch = 2
+    MaxRegistrations = 5
+    KeyByChainHash = TRUE
+    Composes = {c1}
+    MaxAppEpoch = 2
+    LegacyIgnoresAppEpoch = FALSE
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    RevocationIsTotal

docs/formal/key-rotation/EpochPolicyLegacyAppEpoch.cfg

@@ -0,0 +1,16 @@
+\* SPDX-FileCopyrightText: © 2026 Phala Network <dstack@phala.network>
+\* SPDX-License-Identifier: Apache-2.0
+
+SPECIFICATION Spec
+CONSTANTS
+    Values = {v1, v2}
+    Keys = {1, 2}
+    MaxEpoch = 2
+    MaxRegistrations = 5
+    KeyByChainHash = FALSE
+    Composes = {c1}
+    MaxAppEpoch = 2
+    LegacyIgnoresAppEpoch = TRUE
+CHECK_DEADLOCK FALSE
+INVARIANTS
+    AppKeyMatchesSelectedRow

docs/formal/key-rotation/README.md

@@ -13,6 +13,7 @@ as implemented, checked exhaustively with TLC within the stated bounds.
 | `KmsRotation.tla` | Root epoch registry, KMS keyrings, onboarding, key release | `DstackKms.sol`, `kms/src/main_service.rs`, `kms/src/onboard_service.rs` |
 | `DiskMigration.tla` | Data disk setup and LUKS key migration, with crashes and rotations | `dstack-util/src/system_setup.rs`, `system_setup/luks.rs` |
 | `EnvUpdate.tla` | Env re-encryption at boot and the VMM update window | `dstack-util/src/system_setup.rs`, `vmm/src/app.rs` |
+| `EpochPolicy.tla` | Root and app epoch policy rows, range setters, pop and re-registration, legacy app policies, key release on the selected rows | `DstackKms.sol`, `DstackApp.sol` |
 
 ## Running
 
@@ -26,6 +27,9 @@ java -cp tla2tools.jar tlc2.TLC -config DiskMigration.cfg DiskMigration.tla
 | `DiskMigration.cfg` | epochs 0-3 | all invariants hold (828 states) |
 | `EnvUpdate.cfg` | epochs 0-2, 2 owner updates, lossy host API, fail-closed guest | `OwnerUpdateKept` and `NoAppEnv` hold (267 states) |
 | `EnvUpdateLossy.cfg` | same, guest only logs an unanswered update | `NoAppEnv` violated |
+| `EpochPolicy.cfg` | root epochs 0-2, 5 registrations, 2 choices of keys, 2 values; app epochs 0-2, 1 compose hash | `RevocationIsTotal`, `AppKeyMatchesSelectedRow` and `RegistrationStartsEmpty` hold (6,104,564 states) |
+| `EpochPolicyChainHash.cfg` | same, rows keyed by chain hash | `RevocationIsTotal` violated |
+| `EpochPolicyLegacyAppEpoch.cfg` | same, legacy app fallback ignores the requested app epoch | `AppKeyMatchesSelectedRow` violated |
 
 Checked with TLC 2026.11.06 on OpenJDK 21. `EnvUpdate.cfg` models the guest of
 #1546; `EnvUpdateLossy.cfg` the guest before it.
@@ -40,11 +44,24 @@ produces a counterexample:
 - `KmsRotation`: skipping the latest registered epoch's chain hash check on
   handover, which lets an ordinary join pass on a losing pending root.
 - `EnvUpdate`: starting applications after an unanswered update.
+- `EpochPolicy`: the two configs above; and treating a removal from the
+  current epoch through the latest as a revocation, as the epoch-less setters
+  before #1561 did, which lets a historical row still release the key.
 
 ## Abstractions
 
 - A key epoch in `DiskMigration` and `EnvUpdate` stands for the (root, app)
-  epoch pair; the KMS serves every epoch up to the current one.
+  epoch pair; the KMS serves every epoch up to the current one. Authorization
+  is assumed to allow the instance at each of them; `EpochPolicy` models the
+  rows that decide it, and a migrating instance must be allowed in the old
+  rows too.
+- In `KmsRotation`, keys are released for epochs up to the current one and
+  handed over up to the latest registered one, the operation bounds of
+  `kms_serve`/`app_get_key` and `kms_export_keys`/`kms_import_keys`.
+- `EpochPolicy` merges the root materials (OS image, KMS MR and device) into
+  one row per epoch, and the app materials into compose hashes; a release
+  needs one allowed value in each selected row. It has one app and no KMS
+  nodes; `KmsRotation` covers the keyrings.
 - A boot fetches its keys once; the KMS may rotate at any point of
   `DiskMigration`, and between boots in `EnvUpdate`.
 - Each cryptsetup command on the device is atomic: it writes a new keyslot