From 60fa1722fc7f16af4ca7bf3205215bb1cbee089b Mon Sep 17 00:00:00 2001 From: Kevin Wang Date: Sun, 8 Nov 2026 19:07:45 -0800 Subject: [PATCH 1/5] test(auth-eth): add Halmos symbolic tests for DstackApp app epochs Prove app-epoch monotonicity, the epoch bound on policy writes, rejection of inactive epochs and foreign operations, legacy isAppAllowed equivalence at the current epoch, and epoch isolation of authorization decisions. Mutation testing confirms each property catches a targeted bug. Document the FOUNDRY_DYNAMIC_TEST_LINKING=false workaround needed to run Halmos 0.3.3 with Forge 1.8. Signed-off-by: Kevin Wang --- dstack/kms/auth-eth/README.md | 5 + .../kms/auth-eth/docs/formal-verification.md | 24 ++ .../test/DstackAppEpoch.symbolic.t.sol | 238 ++++++++++++++++++ 3 files changed, 267 insertions(+) create mode 100644 dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol diff --git a/dstack/kms/auth-eth/README.md b/dstack/kms/auth-eth/README.md index 029213912..04d4feaa9 100644 --- a/dstack/kms/auth-eth/README.md +++ b/dstack/kms/auth-eth/README.md @@ -149,9 +149,14 @@ than a gate. pipx install slither-analyzer halmos slither . halmos --contract DstackAppSymbolicTest +halmos --contract DstackAppEpochSymbolicTest halmos --contract DstackKmsSymbolicTest ``` +Forge 1.8 enables `dynamic_test_linking` by default, which compiles `new` in +tests to `vm.deployCode`, a cheat code Halmos 0.3.3 does not support. Disable +it for Halmos runs with `FOUNDRY_DYNAMIC_TEST_LINKING=false`. + Configuration lives in `slither.config.json` and `foundry.toml`. See `docs/formal-verification.md` for the verification roadmap, what each symbolic property proves, and the deeper-verification plan for a future diff --git a/dstack/kms/auth-eth/docs/formal-verification.md b/dstack/kms/auth-eth/docs/formal-verification.md index e9987e409..d8fa9f33c 100644 --- a/dstack/kms/auth-eth/docs/formal-verification.md +++ b/dstack/kms/auth-eth/docs/formal-verification.md @@ -120,6 +120,30 @@ says `pre: msg.sender == owner()`, we trust the OZ modifier. init, both `initialize` overloads revert for any inputs. Verifies INV-3. +`test/DstackAppEpoch.symbolic.t.sol` (app epochs; setUp advances to epoch 2 +and admits one app per epoch, then one symbolic owner write where noted): +- [x] `check_AppEpoch_StepMonotonic` — no call to any enumerated mutating + function, by any caller, decreases `currentAppEpoch`; it moves only by + one, through the owner's `advanceAppEpoch(current)`. +- [x] `check_PolicyWrite_RejectsInactiveEpoch` — every `*AtEpoch` setter + reverts for an epoch above the current one, for any caller. +- [x] `check_AuthorizeApp_RejectsInactiveEpochAndForeignOperation` — an + epoch above the current one or a non-app operation is never authorized. +- [x] `check_IsAppAllowed_EqualsCurrentEpochDecision` — the legacy + `isAppAllowed` returns exactly the `authorizeApp` result at the current + epoch, never an older policy. +- [x] `check_PolicyWrite_PreservesOtherEpochDecisions` — a policy write at + one epoch, through the explicit or the current-epoch setters, never + changes an authorization decision at another epoch, including epoch + 0's legacy fields. + +Mutation-tested: dropping a setter's epoch bound, aliasing epoch 1 onto the +legacy fields, deciding `isAppAllowed` at epoch 0, a permissionless +`advanceAppEpoch` and dropping its stale-transaction guard each produce a +counterexample. Dropping the inactive-epoch check in `_authorizeApp` does +not: policy for an inactive epoch cannot be written, so that check is +defense in depth. + Single-call (`test/DstackKms.symbolic.t.sol`): - [x] `check_RegisterApp_AnyCallerCanRegisterNonZeroAddress` + `_RejectsZeroAddress` — codifies the permissionless-by-design behavior; see "Findings" diff --git a/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol new file mode 100644 index 000000000..aff8af4d3 --- /dev/null +++ b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol @@ -0,0 +1,238 @@ +/* + * SPDX-FileCopyrightText: © 2026 Phala Network + * + * SPDX-License-Identifier: Apache-2.0 + */ + +pragma solidity ^0.8.24; + +import "forge-std/Test.sol"; +import "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol"; +import "../contracts/AuthorizationOperation.sol"; +import "../contracts/DstackApp.sol"; + +/// @notice Halmos symbolic tests for DstackApp app epochs. +/// +/// Halmos has no symbolic storage, so tests that quantify over policy states +/// first apply one symbolic owner write on top of setUp's concrete state. +/// DstackApp reads only the compose hash, device ID and TCB status of an +/// AppInfo, so those are the symbolic inputs; the remaining fields stay zero. +/// +/// Run with `halmos --contract DstackAppEpochSymbolicTest`. +contract DstackAppEpochSymbolicTest is Test { + DstackApp internal app; + address internal constant OWNER = address(0xA11CE); + uint256 internal constant POLICY_SETTERS = 10; + + function setUp() public { + DstackApp impl = new DstackApp(); + bytes memory initData = abi.encodeWithSignature( + "initialize(address,bool,bool,bytes32,bytes32)", OWNER, false, false, bytes32(0), bytes32(0) + ); + app = DstackApp(address(new ERC1967Proxy(address(impl), initData))); + // Epoch 0 keeps the legacy storage fields; epochs 1 and 2 use the + // per-epoch maps. Each epoch admits some app so that decisions can be + // allowed as well as denied. + vm.startPrank(OWNER); + app.addComposeHash(bytes32(uint256(0xc0))); + app.addDevice(bytes32(uint256(0xd0))); + app.advanceAppEpoch(0); + app.addComposeHash(bytes32(uint256(0xc1))); + app.setAllowAnyDevice(true); + app.advanceAppEpoch(1); + app.addComposeHash(bytes32(uint256(0xc2))); + app.addDevice(bytes32(uint256(0xd2))); + vm.stopPrank(); + } + + /// Calldata of one policy setter and the epoch it writes. + function _policyCall( + uint256 which, + uint256 epoch, + bytes32 word, + bool flag + ) + internal + view + returns (bytes memory data, uint256 target) + { + uint256 current = app.currentAppEpoch(); + target = which < 5 ? epoch : current; + if (which == 0) data = abi.encodeCall(DstackApp.addComposeHashAtEpoch, (epoch, word)); + else if (which == 1) data = abi.encodeCall(DstackApp.removeComposeHashAtEpoch, (epoch, word)); + else if (which == 2) data = abi.encodeCall(DstackApp.addDeviceAtEpoch, (epoch, word)); + else if (which == 3) data = abi.encodeCall(DstackApp.removeDeviceAtEpoch, (epoch, word)); + else if (which == 4) data = abi.encodeCall(DstackApp.setAllowAnyDeviceAtEpoch, (epoch, flag)); + else if (which == 5) data = abi.encodeCall(DstackApp.addComposeHash, (word)); + else if (which == 6) data = abi.encodeCall(DstackApp.removeComposeHash, (word)); + else if (which == 7) data = abi.encodeCall(DstackApp.addDevice, (word)); + else if (which == 8) data = abi.encodeCall(DstackApp.removeDevice, (word)); + else data = abi.encodeCall(DstackApp.setAllowAnyDevice, (flag)); + } + + function _ownerPolicyWrite(uint256 which, uint256 epoch, bytes32 word, bool flag) internal { + if (which >= POLICY_SETTERS) return; + (bytes memory data,) = _policyCall(which, epoch, word, flag); + vm.prank(OWNER); + (bool ok,) = address(app).call(data); + ok; // a reverted write leaves the setUp state, which is also a valid pre-state + } + + function _info( + bytes32 composeHash, + bytes32 deviceId, + bool upToDate + ) + internal + pure + returns (IAppAuth.AppInfo memory info) + { + info.composeHash = composeHash; + info.deviceId = deviceId; + info.tcbStatus = upToDate ? "UpToDate" : "OutOfDate"; + } + + function _decision(IAppAuth.AppInfo memory info, uint256 epoch) internal view returns (bool, bytes32) { + (bool allowed, string memory reason) = app.authorizeApp(info, epoch, AuthorizationOperation.APP_GET_KEY); + return (allowed, keccak256(bytes(reason))); + } + + // --------------------------------------------------------------- + // The app epoch never decreases, and only the owner's + // advanceAppEpoch(current) moves it, by exactly one. + // --------------------------------------------------------------- + + function check_AppEpoch_StepMonotonic( + address caller, + uint256 which, + uint256 epoch, + bytes32 word, + bool flag, + address addr + ) + external + { + uint256 before = app.currentAppEpoch(); + + bytes memory data; + if (which < POLICY_SETTERS) (data,) = _policyCall(which, epoch, word, flag); + else if (which == 10) data = abi.encodeCall(DstackApp.advanceAppEpoch, (epoch)); + else if (which == 11) data = abi.encodeCall(DstackApp.setRequireTcbUpToDate, (flag)); + else if (which == 12) data = abi.encodeCall(DstackApp.disableUpgrades, ()); + else if (which == 13) data = abi.encodeCall(UUPSUpgradeable.upgradeToAndCall, (addr, "")); + else if (which == 14) data = abi.encodeCall(Ownable2StepUpgradeable.transferOwnership, (addr)); + else if (which == 15) data = abi.encodeCall(Ownable2StepUpgradeable.acceptOwnership, ()); + else if (which == 16) data = abi.encodeCall(OwnableUpgradeable.renounceOwnership, ()); + else return; + + vm.prank(caller); + (bool ok,) = address(app).call(data); + ok; + + uint256 afterEpoch = app.currentAppEpoch(); + if (afterEpoch != before) { + assert(afterEpoch == before + 1); + assert(caller == OWNER && which == 10 && epoch == before); + } + } + + // --------------------------------------------------------------- + // No caller can write policy for an epoch that is not active yet. + // --------------------------------------------------------------- + + function check_PolicyWrite_RejectsInactiveEpoch( + address caller, + uint256 which, + uint256 epoch, + bytes32 word, + bool flag + ) + external + { + vm.assume(which < 5 && epoch > app.currentAppEpoch()); + (bytes memory data,) = _policyCall(which, epoch, word, flag); + vm.prank(caller); + (bool ok,) = address(app).call(data); + assert(!ok); + } + + // --------------------------------------------------------------- + // An epoch that is not active is never authorized, and only app + // operations are authorized. + // --------------------------------------------------------------- + + function check_AuthorizeApp_RejectsInactiveEpochAndForeignOperation( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bool flag, + bytes32 composeHash, + bytes32 deviceId, + bool upToDate, + uint256 epoch, + bytes32 operation + ) + external + { + _ownerPolicyWrite(which, writeEpoch, word, flag); + IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); + vm.assume(epoch > app.currentAppEpoch() || !AuthorizationOperation.isApp(operation)); + (bool allowed,) = app.authorizeApp(info, epoch, operation); + assert(!allowed); + } + + // --------------------------------------------------------------- + // The legacy IAppAuth entry point decides exactly as the + // epoch-aware one at the current epoch, never an older policy. + // --------------------------------------------------------------- + + function check_IsAppAllowed_EqualsCurrentEpochDecision( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bool flag, + bytes32 composeHash, + bytes32 deviceId, + bool upToDate + ) + external + { + _ownerPolicyWrite(which, writeEpoch, word, flag); + IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); + (bool allowed, string memory reason) = app.isAppAllowed(info); + (bool expected, bytes32 expectedReason) = _decision(info, app.currentAppEpoch()); + assert(allowed == expected && keccak256(bytes(reason)) == expectedReason); + } + + // --------------------------------------------------------------- + // Epoch isolation: a policy write at one epoch never changes an + // authorization decision at another epoch, including epoch 0's + // legacy fields. Covers both the explicit and current-epoch setters. + // --------------------------------------------------------------- + + function check_PolicyWrite_PreservesOtherEpochDecisions( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bool flag, + bytes32 composeHash, + bytes32 deviceId, + bool upToDate, + uint256 epoch + ) + external + { + vm.assume(which < POLICY_SETTERS); + (bytes memory data, uint256 target) = _policyCall(which, writeEpoch, word, flag); + vm.assume(target != epoch); + + IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); + (bool allowedBefore, bytes32 reasonBefore) = _decision(info, epoch); + vm.prank(OWNER); + (bool ok,) = address(app).call(data); + ok; + (bool allowedAfter, bytes32 reasonAfter) = _decision(info, epoch); + + assert(allowedBefore == allowedAfter && reasonBefore == reasonAfter); + } +} From 791cc228140d859d2bf295e814d5de74a6234b21 Mon Sep 17 00:00:00 2001 From: Kevin Wang Date: Sun, 8 Nov 2026 20:25:06 -0800 Subject: [PATCH 2/5] test(auth-eth): prove DstackApp authorization matches epoch policy Add positive properties: authorizeApp allows exactly when the epoch policy admits the app, and each per-epoch setter takes effect. Signed-off-by: Kevin Wang --- .../kms/auth-eth/docs/formal-verification.md | 11 ++++- .../test/DstackAppEpoch.symbolic.t.sol | 42 +++++++++++++++++++ 2 files changed, 51 insertions(+), 2 deletions(-) diff --git a/dstack/kms/auth-eth/docs/formal-verification.md b/dstack/kms/auth-eth/docs/formal-verification.md index d8fa9f33c..c371572f8 100644 --- a/dstack/kms/auth-eth/docs/formal-verification.md +++ b/dstack/kms/auth-eth/docs/formal-verification.md @@ -136,8 +136,15 @@ and admits one app per epoch, then one symbolic owner write where noted): one epoch, through the explicit or the current-epoch setters, never changes an authorization decision at another epoch, including epoch 0's legacy fields. - -Mutation-tested: dropping a setter's epoch bound, aliasing epoch 1 onto the +- [x] `check_AuthorizeApp_MatchesPolicy` — for both app operations, + `authorizeApp` allows exactly when the epoch is active, the TCB + requirement holds, and that epoch admits the compose hash and device. +- [x] `check_PolicyWrite_TakesEffect` — each `*AtEpoch` setter on an active + epoch either sets the value it was given or reverts on a zero ID. + +Mutation-tested: requiring both the any-device flag and a listed device, +ignoring the value of a per-epoch `allowAnyDevice` write, dropping a setter's +epoch bound, aliasing epoch 1 onto the legacy fields, deciding `isAppAllowed` at epoch 0, a permissionless `advanceAppEpoch` and dropping its stale-transaction guard each produce a counterexample. Dropping the inactive-epoch check in `_authorizeApp` does diff --git a/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol index aff8af4d3..c43c989e4 100644 --- a/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol +++ b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol @@ -235,4 +235,46 @@ contract DstackAppEpochSymbolicTest is Test { assert(allowedBefore == allowedAfter && reasonBefore == reasonAfter); } + + function check_AuthorizeApp_MatchesPolicy( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bool flag, + bool tcbFlag, + bytes32 composeHash, + bytes32 deviceId, + bool upToDate, + uint256 epoch, + bool getCert + ) + external + { + vm.prank(OWNER); + app.setRequireTcbUpToDate(tcbFlag); + _ownerPolicyWrite(which, writeEpoch, word, flag); + IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); + bytes32 op = getCert ? AuthorizationOperation.APP_GET_CERT : AuthorizationOperation.APP_GET_KEY; + (bool allowed,) = app.authorizeApp(info, epoch, op); + bool expected = epoch <= app.currentAppEpoch() && (!tcbFlag || upToDate) + && app.allowedComposeHashesAtEpoch(epoch, composeHash) + && (app.allowAnyDeviceAtEpoch(epoch) || app.allowedDeviceIdsAtEpoch(epoch, deviceId)); + assert(allowed == expected); + } + + function check_PolicyWrite_TakesEffect(uint256 which, uint256 epoch, bytes32 word, bool flag) external { + vm.assume(which < 5 && epoch <= app.currentAppEpoch()); + (bytes memory data,) = _policyCall(which, epoch, word, flag); + vm.prank(OWNER); + (bool ok,) = address(app).call(data); + if (!ok) { + assert(word == bytes32(0) && (which == 0 || which == 2)); + return; + } + if (which == 0) assert(app.allowedComposeHashesAtEpoch(epoch, word)); + if (which == 1) assert(!app.allowedComposeHashesAtEpoch(epoch, word)); + if (which == 2) assert(app.allowedDeviceIdsAtEpoch(epoch, word)); + if (which == 3) assert(!app.allowedDeviceIdsAtEpoch(epoch, word)); + if (which == 4) assert(app.allowAnyDeviceAtEpoch(epoch) == flag); + } } From 5523b07da163b6e9f7ca25a7dbe9a59536cf189f Mon Sep 17 00:00:00 2001 From: Kevin Wang Date: Sun, 8 Nov 2026 21:26:13 -0800 Subject: [PATCH 3/5] test(auth-eth): add Halmos symbolic tests for DstackKms root epochs Prove the root registry step invariant (append-only entries, chain hash recursion, hash-bound activation and pop, kmsInfo following the current epoch), canonical key encodings, authorization epoch bounds and root epoch reporting, bootstrap-only authorization before registration, KMS and app authorization matching epoch policy, epoch isolation of KMS policy writes, and legacy entry points following the current epochs. Mutation testing confirms each property catches a targeted bug. Signed-off-by: Kevin Wang --- dstack/kms/auth-eth/README.md | 1 + .../kms/auth-eth/docs/formal-verification.md | 45 ++ .../test/DstackKmsEpoch.symbolic.t.sol | 465 ++++++++++++++++++ 3 files changed, 511 insertions(+) create mode 100644 dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol diff --git a/dstack/kms/auth-eth/README.md b/dstack/kms/auth-eth/README.md index 04d4feaa9..0fa860491 100644 --- a/dstack/kms/auth-eth/README.md +++ b/dstack/kms/auth-eth/README.md @@ -151,6 +151,7 @@ slither . halmos --contract DstackAppSymbolicTest halmos --contract DstackAppEpochSymbolicTest halmos --contract DstackKmsSymbolicTest +halmos --contract DstackKmsEpochSymbolicTest ``` Forge 1.8 enables `dynamic_test_linking` by default, which compiles `new` in diff --git a/dstack/kms/auth-eth/docs/formal-verification.md b/dstack/kms/auth-eth/docs/formal-verification.md index c371572f8..98d87e870 100644 --- a/dstack/kms/auth-eth/docs/formal-verification.md +++ b/dstack/kms/auth-eth/docs/formal-verification.md @@ -151,6 +151,51 @@ counterexample. Dropping the inactive-epoch check in `_authorizeApp` does not: policy for an inactive epoch cannot be written, so that check is defense in depth. +`test/DstackKmsEpoch.symbolic.t.sol` (root epochs; setUp registers epochs +0-2, activates 1 so that 2 is pending, admits one KMS identity and OS image +per epoch, and deploys an app at app epoch 1): +- [x] `check_RootRegistry_StepInvariant` — after any single call to any + enumerated mutating function, by any caller with symbolic args: the + current epoch stays registered and moves only by one, through the + owner's activation naming its chain hash; the registry changes by at + most one entry at its end, and only the owner's pop of a pending + epoch naming its chain hash removes one; existing entries keep their + keys and hashes; every chain hash commits to its keys and the previous + hash; `kmsInfo` holds the current keys without legacy evidence. +- [x] `check_RegisterRootEpoch_AcceptsOnlyCanonicalEncodings` — registration + succeeds exactly for a 91-byte uncompressed P-256 SPKI and a 33-byte + compressed secp256k1 key. +- [x] `check_Authorize_EnforcesEpochBounds` — a wrong-kind operation, an app + root epoch above the current one, a KMS root epoch above the latest + registered one, or an app epoch above the app's current one is never + authorized; every result reports the current root epoch and hash. +- [x] `check_Authorize_OnlyBootstrapBeforeRegistration` — with no root epoch + registered, only `kms_bootstrap` can be authorized. +- [x] `check_AuthorizeKms_MatchesEpochPolicy` — after any one owner write, + KMS authorization allows exactly when the selected root epoch is + registered, the TCB is up to date, and that epoch's row admits the OS + image, aggregated MR and device. +- [x] `check_AuthorizeApp_MatchesKmsAndAppPolicy` — app authorization allows + exactly when both epochs are active, the selected root epoch admits + the OS image, and the app's own `authorizeApp` admits it. +- [x] `check_KmsPolicyWrite_PreservesOtherEpochDecisions` — a KMS policy + write at one root epoch, through the explicit or the latest-epoch + setters, never changes a KMS decision at another epoch. +- [x] `check_LegacyEntryPoints_FollowCurrentEpochs` — `isKmsAllowed` + decides as `kms_serve` at the current root epoch, and `isAppAllowed` + denies an app that has left app epoch 0. + +Mutation-tested: a chain hash that ignores the previous epoch, activation +that leaves `kmsInfo` stale, a pop that ignores the chain hash, app requests +selecting a pending root epoch, KMS requests limited to the current epoch, +`isKmsAllowed` checking the latest epoch, accepting an `0x04` k256 tag, an +OS image row aliasing epoch 1 onto the legacy row, an app check skipping the +OS image, and non-bootstrap operations before registration each produce a +counterexample. + +The bounds test found that wrong-kind rejections reported root epoch +`(0, 0x0)`, contrary to the KMS README; fixed in #1538. + Single-call (`test/DstackKms.symbolic.t.sol`): - [x] `check_RegisterApp_AnyCallerCanRegisterNonZeroAddress` + `_RejectsZeroAddress` — codifies the permissionless-by-design behavior; see "Findings" diff --git a/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol new file mode 100644 index 000000000..3df82de83 --- /dev/null +++ b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol @@ -0,0 +1,465 @@ +/* + * SPDX-FileCopyrightText: © 2026 Phala Network + * + * SPDX-License-Identifier: Apache-2.0 + */ + +pragma solidity ^0.8.24; + +import "forge-std/Test.sol"; +import "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol"; +import "../contracts/AuthorizationOperation.sol"; +import "../contracts/DstackApp.sol"; +import "../contracts/DstackKms.sol"; + +/// @notice Halmos symbolic tests for DstackKms root epochs and epoch-scoped +/// authorization. +/// +/// setUp registers root epochs 0, 1 and 2, activates 1 (so 2 is pending), +/// admits one KMS identity and OS image per epoch, and deploys an app at app +/// epoch 1. Halmos has no symbolic storage, so the properties are proved from +/// this state, after one symbolic call where noted. +/// +/// Run with `halmos --contract DstackKmsEpochSymbolicTest`. +contract DstackKmsEpochSymbolicTest is Test { + DstackKms internal kms; + DstackApp internal app; + address internal constant OWNER = address(0xA11CE); + bytes27 internal constant P256_SPKI_PREFIX = 0x3059301306072a8648ce3d020106082a8648ce3d03010703420004; + uint256 internal constant KMS_POLICY_SETTERS = 12; + + /// The AppInfo fields DstackKms and DstackApp read; the app ID is the + /// deployed app and the remaining fields stay zero. + struct Identity { + bytes32 osImageHash; + bytes32 mrAggregated; + bytes32 deviceId; + bytes32 composeHash; + bool upToDate; + } + + function setUp() public { + DstackKms impl = new DstackKms(); + bytes memory initData = abi.encodeCall(DstackKms.initialize, (OWNER, address(new DstackApp()))); + kms = DstackKms(address(new ERC1967Proxy(address(impl), initData))); + + vm.startPrank(OWNER); + for (uint256 epoch = 0; epoch < 3; epoch++) { + kms.registerRootEpoch(_ca(bytes32(epoch + 1), bytes32(0)), _k256(true, bytes32(epoch + 1)), "evidence"); + kms.addOsImageHashAtEpoch(epoch, _id(0x05, epoch)); + kms.addKmsAggregatedMrAtEpoch(epoch, _id(0x0a, epoch)); + kms.addKmsDeviceAtEpoch(epoch, _id(0x0d, epoch)); + } + (, bytes32 hash1) = _entry(1); + kms.activateRootEpoch(1, hash1); + + app = DstackApp(kms.deployAndRegisterApp(OWNER, false, false, true, bytes32(0), _id(0xc0, 0))); + app.advanceAppEpoch(0); + app.addComposeHash(_id(0xc0, 1)); + app.setAllowAnyDevice(true); + vm.stopPrank(); + } + + function _id(uint256 kind, uint256 epoch) internal pure returns (bytes32) { + return bytes32((kind << 8) | epoch); + } + + function _ca(bytes32 x, bytes32 y) internal pure returns (bytes memory) { + return abi.encodePacked(P256_SPKI_PREFIX, x, y); + } + + function _k256(bool even, bytes32 x) internal pure returns (bytes memory) { + return abi.encodePacked(even ? bytes1(0x02) : bytes1(0x03), x); + } + + function _current() internal view returns (uint256 epoch) { + (epoch,) = kms.currentRootEpoch(); + } + + /// Hash of an epoch's keys, and its chain hash. + function _entry(uint256 epoch) internal view returns (bytes32 keys, bytes32 chainHash) { + (bytes memory ca, bytes memory k256,, bytes32 hash) = kms.rootEpoch(epoch); + return (keccak256(abi.encode(ca, k256)), hash); + } + + function _info(Identity memory id) internal view returns (IAppAuth.AppInfo memory info) { + info.appId = address(app); + info.osImageHash = id.osImageHash; + info.mrAggregated = id.mrAggregated; + info.deviceId = id.deviceId; + info.composeHash = id.composeHash; + info.tcbStatus = id.upToDate ? "UpToDate" : "OutOfDate"; + } + + function _request( + IAppAuth.AppInfo memory info, + bytes32 operation, + bool rootSet, + uint256 root, + bool appSet, + uint256 appEpoch + ) + internal + pure + returns (DstackKms.AuthorizationRequest memory) + { + return DstackKms.AuthorizationRequest( + info, operation, DstackKms.OptionalUint256(appSet, appEpoch), DstackKms.OptionalUint256(rootSet, root) + ); + } + + /// Calldata of one KMS policy setter and the root epoch it writes. + function _kmsPolicyCall( + uint256 which, + uint256 epoch, + bytes32 word + ) + internal + view + returns (bytes memory data, uint256 target) + { + // Setters without an epoch write the latest registered epoch, pending included. + target = which < 6 ? epoch : kms.rootEpochCount() - 1; + if (which == 0) data = abi.encodeCall(DstackKms.addKmsAggregatedMrAtEpoch, (epoch, word)); + else if (which == 1) data = abi.encodeCall(DstackKms.removeKmsAggregatedMrAtEpoch, (epoch, word)); + else if (which == 2) data = abi.encodeCall(DstackKms.addKmsDeviceAtEpoch, (epoch, word)); + else if (which == 3) data = abi.encodeCall(DstackKms.removeKmsDeviceAtEpoch, (epoch, word)); + else if (which == 4) data = abi.encodeCall(DstackKms.addOsImageHashAtEpoch, (epoch, word)); + else if (which == 5) data = abi.encodeCall(DstackKms.removeOsImageHashAtEpoch, (epoch, word)); + else if (which == 6) data = abi.encodeCall(DstackKms.addKmsAggregatedMr, (word)); + else if (which == 7) data = abi.encodeCall(DstackKms.removeKmsAggregatedMr, (word)); + else if (which == 8) data = abi.encodeCall(DstackKms.addKmsDevice, (word)); + else if (which == 9) data = abi.encodeCall(DstackKms.removeKmsDevice, (word)); + else if (which == 10) data = abi.encodeCall(DstackKms.addOsImageHash, (word)); + else data = abi.encodeCall(DstackKms.removeOsImageHash, (word)); + } + + // --------------------------------------------------------------- + // Root registry step invariant. After any single call to any + // enumerated mutating function, by any caller with symbolic args: + // - the current epoch stays registered and only the owner's + // activation of the next epoch, naming its chain hash, moves it, + // by one; + // - the registry changes by at most one entry at its end, and only + // the owner's pop of a pending epoch, naming its chain hash, + // removes one; + // - existing entries keep their keys and chain hashes; + // - every chain hash commits to its keys and the previous hash; + // - kmsInfo holds the current epoch's keys and no legacy evidence. + // --------------------------------------------------------------- + + /// Calldata of any enumerated mutating function. + function _anyCall( + uint256 which, + uint256 epoch, + bytes32 word, + bytes32 hash, + bool flag, + address addr + ) + internal + view + returns (bytes memory data) + { + if (which < KMS_POLICY_SETTERS) { + (data,) = _kmsPolicyCall(which, epoch, word); + } else if (which == 12) { + data = abi.encodeCall(DstackKms.registerRootEpoch, (_ca(word, hash), _k256(flag, word), "url")); + } else if (which == 13) { + data = abi.encodeCall(DstackKms.activateRootEpoch, (epoch, hash)); + } else if (which == 14) { + data = abi.encodeCall(DstackKms.popRootEpoch, (epoch, hash)); + } else if (which == 15) { + data = abi.encodeCall(DstackKms.setRootEpochEvidenceUrl, (epoch, "url")); + } else if (which == 16) { + data = abi.encodeCall(DstackKms.setGatewayAppId, ("gateway")); + } else if (which == 17) { + data = abi.encodeCall(DstackKms.setAppImplementation, (addr)); + } else if (which == 18) { + data = abi.encodeCall(DstackKms.registerApp, (addr)); + } else if (which == 19) { + data = abi.encodeWithSignature( + "deployAndRegisterApp(address,bool,bool,bool,bytes32,bytes32)", addr, flag, flag, flag, word, hash + ); + } else if (which == 20) { + data = abi.encodeCall(UUPSUpgradeable.upgradeToAndCall, (addr, "")); + } else if (which == 21) { + data = abi.encodeCall(Ownable2StepUpgradeable.transferOwnership, (addr)); + } else if (which == 22) { + data = abi.encodeCall(OwnableUpgradeable.renounceOwnership, ()); + } + } + + function _snapshot() internal view returns (bytes32[] memory entries, bytes32[] memory hashes) { + uint256 count = kms.rootEpochCount(); + entries = new bytes32[](count); + hashes = new bytes32[](count); + for (uint256 i = 0; i < count; i++) { + (entries[i], hashes[i]) = _entry(i); + } + } + + /// Every chain hash commits to its keys and the previous hash, entries + /// that existed before keep their keys and hashes, and kmsInfo holds + /// the current keys without legacy evidence. + function _assertRegistryConsistent(bytes32[] memory entries, bytes32[] memory hashes) internal view { + bytes32 previous; + for (uint256 i = 0; i < kms.rootEpochCount(); i++) { + (bytes memory ca, bytes memory k256,, bytes32 chainHash) = kms.rootEpoch(i); + assert(chainHash == keccak256(abi.encodePacked(previous, keccak256(ca), keccak256(k256)))); + if (i < entries.length) assert(keccak256(abi.encode(ca, k256)) == entries[i] && chainHash == hashes[i]); + previous = chainHash; + } + (bytes memory infoK256, bytes memory infoCa, bytes memory quote, bytes memory eventlog) = kms.kmsInfo(); + (bytes memory currentCa, bytes memory currentK256,,) = kms.rootEpoch(_current()); + assert(keccak256(infoCa) == keccak256(currentCa) && keccak256(infoK256) == keccak256(currentK256)); + assert(quote.length == 0 && eventlog.length == 0); + } + + /// @custom:halmos --loop 4 + function check_RootRegistry_StepInvariant( + address caller, + uint256 which, + uint256 epoch, + bytes32 word, + bytes32 hash, + bool flag, + address addr + ) + external + { + vm.assume(which <= 22); + // Registry functions index the root epoch array, which Halmos cannot + // do symbolically. Only epochs 0-2 exist, so every larger index + // behaves as 3; branching makes each case concrete. + if (which >= 13 && which <= 15) epoch = epoch == 0 ? 0 : epoch == 1 ? 1 : epoch == 2 ? 2 : 3; + uint256 currentBefore = _current(); + (bytes32[] memory entries, bytes32[] memory hashes) = _snapshot(); + + vm.prank(caller); + (bool ok,) = address(kms).call(_anyCall(which, epoch, word, hash, flag, addr)); + ok; + + uint256 count = kms.rootEpochCount(); + uint256 current = _current(); + assert(current < count); + if (current != currentBefore) { + assert(current == currentBefore + 1); + assert(caller == OWNER && which == 13 && epoch == current && hash == hashes[current]); + } + assert(count + 1 >= entries.length && count <= entries.length + 1); + if (count < entries.length) { + assert(caller == OWNER && which == 14 && epoch == count && epoch > currentBefore && hash == hashes[count]); + } + if (count > entries.length) assert(caller == OWNER && which == 12); + _assertRegistryConsistent(entries, hashes); + } + + /// Drop the last byte, keep the bytes, or append a zero byte. + function _resize(bytes memory data, int8 change) internal pure returns (bytes memory) { + if (change < 0) { + assembly { + mstore(data, sub(mload(data), 1)) + } + return data; + } + return change == 0 ? data : abi.encodePacked(data, bytes1(0)); + } + + // --------------------------------------------------------------- + // registerRootEpoch accepts exactly the encodings the KMS + // produces: a 91-byte uncompressed P-256 SubjectPublicKeyInfo and + // a 33-byte compressed secp256k1 key. + // --------------------------------------------------------------- + + function check_RegisterRootEpoch_AcceptsOnlyCanonicalEncodings( + bytes27 prefix, + bytes32 x, + bytes1 tag, + int8 caLength, + int8 k256Length + ) + external + { + bytes memory ca = _resize(abi.encodePacked(prefix, x, x), caLength); + bytes memory k256 = _resize(abi.encodePacked(tag, x), k256Length); + + vm.prank(OWNER); + (bool ok,) = address(kms).call(abi.encodeCall(DstackKms.registerRootEpoch, (ca, k256, "url"))); + + bool canonical = ca.length == 91 && prefix == P256_SPKI_PREFIX && k256.length == 33 + && (tag == bytes1(0x02) || tag == bytes1(0x03)); + assert(ok == canonical); + } + + // --------------------------------------------------------------- + // Authorization bounds: an operation of the wrong kind, an app + // root epoch above the current one, a KMS root epoch above the + // latest registered one, or an app epoch above the app's current + // one is never authorized. Every result reports the current root + // epoch and its chain hash. + // --------------------------------------------------------------- + + function check_Authorize_EnforcesEpochBounds( + bool isKms, + bytes32 operation, + bool rootSet, + uint256 root, + bool appSet, + uint256 appEpoch, + Identity calldata id + ) + external + view + { + DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, rootSet, root, appSet, appEpoch); + DstackKms.AuthorizationResult memory result = isKms ? kms.authorizeKms(request) : kms.authorizeApp(request); + + (uint256 current, bytes32 currentHash) = kms.currentRootEpoch(); + assert(result.currentRootEpoch == current && result.currentRootEpochHash == currentHash); + + bool kindMatches = isKms ? AuthorizationOperation.isKms(operation) : AuthorizationOperation.isApp(operation); + uint256 rootBound = isKms ? kms.rootEpochCount() - 1 : current; + uint256 appBound = isKms ? 0 : app.currentAppEpoch(); + if (!kindMatches || (rootSet && root > rootBound) || (appSet && appEpoch > appBound)) { + assert(!result.isAllowed); + } + } + + // --------------------------------------------------------------- + // Before any root epoch is registered, only KMS bootstrap can be + // authorized. + // --------------------------------------------------------------- + + function check_Authorize_OnlyBootstrapBeforeRegistration( + bool isKms, + bytes32 operation, + Identity calldata id + ) + external + { + DstackKms impl = new DstackKms(); + bytes memory initData = abi.encodeCall(DstackKms.initialize, (OWNER, address(new DstackApp()))); + DstackKms fresh = DstackKms(address(new ERC1967Proxy(address(impl), initData))); + vm.startPrank(OWNER); + fresh.addOsImageHash(id.osImageHash); + fresh.addKmsAggregatedMr(id.mrAggregated); + fresh.addKmsDevice(id.deviceId); + vm.stopPrank(); + + DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, false, 0, false, 0); + DstackKms.AuthorizationResult memory result = isKms ? fresh.authorizeKms(request) : fresh.authorizeApp(request); + if (result.isAllowed) assert(isKms && operation == AuthorizationOperation.KMS_BOOTSTRAP); + } + + // --------------------------------------------------------------- + // KMS authorization matches the policy of the selected root epoch + // (requested, or current when unset), after any one owner write. + // --------------------------------------------------------------- + + function check_AuthorizeKms_MatchesEpochPolicy( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bytes32 operation, + bool rootSet, + uint256 root, + Identity calldata id + ) + external + { + if (which < KMS_POLICY_SETTERS) { + (bytes memory data,) = _kmsPolicyCall(which, writeEpoch, word); + vm.prank(OWNER); + (bool ok,) = address(kms).call(data); + ok; + } + + DstackKms.AuthorizationResult memory result = + kms.authorizeKms(_request(_info(id), operation, rootSet, root, false, 0)); + + uint256 epoch = rootSet ? root : _current(); + bool expected = AuthorizationOperation.isKms(operation) && epoch < kms.rootEpochCount() && id.upToDate + && kms.allowedOsImagesAtEpoch(epoch, id.osImageHash) + && kms.kmsAllowedAggregatedMrsAtEpoch(epoch, id.mrAggregated) + && kms.kmsAllowedDeviceIdsAtEpoch(epoch, id.deviceId); + assert(result.isAllowed == expected); + } + + // --------------------------------------------------------------- + // App authorization admits exactly a registered app whose OS image + // the selected root epoch allows and whose own policy admits it at + // the selected app epoch. + // --------------------------------------------------------------- + + function check_AuthorizeApp_MatchesKmsAndAppPolicy( + bool getCert, + bool rootSet, + uint256 root, + bool appSet, + uint256 appEpoch, + Identity calldata id + ) + external + view + { + bytes32 operation = getCert ? AuthorizationOperation.APP_GET_CERT : AuthorizationOperation.APP_GET_KEY; + IAppAuth.AppInfo memory info = _info(id); + DstackKms.AuthorizationResult memory result = + kms.authorizeApp(_request(info, operation, rootSet, root, appSet, appEpoch)); + + uint256 rootEpoch = rootSet ? root : _current(); + uint256 selectedAppEpoch = appSet ? appEpoch : app.currentAppEpoch(); + bool expected = rootEpoch <= _current() && selectedAppEpoch <= app.currentAppEpoch() + && kms.allowedOsImagesAtEpoch(rootEpoch, id.osImageHash); + if (expected) (expected,) = app.authorizeApp(info, selectedAppEpoch, operation); + assert(result.isAllowed == expected); + } + + // --------------------------------------------------------------- + // Epoch isolation: a KMS policy write at one root epoch never + // changes a KMS authorization decision at another. + // --------------------------------------------------------------- + + function check_KmsPolicyWrite_PreservesOtherEpochDecisions( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bytes32 operation, + uint256 root, + Identity calldata id + ) + external + { + vm.assume(which < KMS_POLICY_SETTERS); + (bytes memory data, uint256 target) = _kmsPolicyCall(which, writeEpoch, word); + vm.assume(target != root); + + DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, true, root, false, 0); + DstackKms.AuthorizationResult memory before = kms.authorizeKms(request); + vm.prank(OWNER); + (bool ok,) = address(kms).call(data); + ok; + DstackKms.AuthorizationResult memory afterWrite = kms.authorizeKms(request); + + assert(before.isAllowed == afterWrite.isAllowed); + assert(keccak256(bytes(before.rejectionReason)) == keccak256(bytes(afterWrite.rejectionReason))); + } + + // --------------------------------------------------------------- + // Legacy entry points: isKmsAllowed decides as KMS_SERVE at the + // current root epoch, and isAppAllowed never authorizes an app + // whose policy has left app epoch 0. + // --------------------------------------------------------------- + + function check_LegacyEntryPoints_FollowCurrentEpochs(Identity calldata id) external view { + IAppAuth.AppInfo memory info = _info(id); + (bool kmsAllowed,) = kms.isKmsAllowed(info); + DstackKms.AuthorizationResult memory serve = + kms.authorizeKms(_request(info, AuthorizationOperation.KMS_SERVE, false, 0, false, 0)); + assert(kmsAllowed == serve.isAllowed); + + (bool appAllowed,) = kms.isAppAllowed(info); + assert(!appAllowed); + } +} From b4cbe2b9143ea54526b10e780ae0f2a2b73cd019 Mon Sep 17 00:00:00 2001 From: Kevin Wang Date: Mon, 9 Nov 2026 07:13:55 -0800 Subject: [PATCH 4/5] test(auth-eth): sync the epoch symbolic tests with the reviewed contracts Follow the interface of #1542: AuthorizationRequest and AuthorizationResult live in IAppEpochAuth.sol, `isAllowed` is `authorized`, and DstackApp's authorizeApp takes the request. Update the properties that the review intentionally changed: - *AtEpoch setters may prepare the next app epoch, and revert past it; - the legacy isAppAllowed refuses at a nonzero app epoch, and at epoch 0 decides at epoch 0 even with the next row prepared; - epoch-less KMS setters write every row from the current epoch to the latest one; - the legacy isKmsAllowed decides at root epoch 0. Each changed property was mutation-tested against the matching bug. Signed-off-by: Kevin Wang --- .../kms/auth-eth/docs/formal-verification.md | 32 ++++---- .../test/DstackAppEpoch.symbolic.t.sol | 57 ++++++++++++-- .../test/DstackKmsEpoch.symbolic.t.sol | 76 +++++++++++-------- 3 files changed, 114 insertions(+), 51 deletions(-) diff --git a/dstack/kms/auth-eth/docs/formal-verification.md b/dstack/kms/auth-eth/docs/formal-verification.md index 98d87e870..9d59e6101 100644 --- a/dstack/kms/auth-eth/docs/formal-verification.md +++ b/dstack/kms/auth-eth/docs/formal-verification.md @@ -125,13 +125,17 @@ and admits one app per epoch, then one symbolic owner write where noted): - [x] `check_AppEpoch_StepMonotonic` — no call to any enumerated mutating function, by any caller, decreases `currentAppEpoch`; it moves only by one, through the owner's `advanceAppEpoch(current)`. -- [x] `check_PolicyWrite_RejectsInactiveEpoch` — every `*AtEpoch` setter - reverts for an epoch above the current one, for any caller. +- [x] `check_PolicyWrite_RejectsEpochPastNext` — every `*AtEpoch` setter + reverts for an epoch above the next one, for any caller; the owner may + prepare the next epoch's row before advancing. - [x] `check_AuthorizeApp_RejectsInactiveEpochAndForeignOperation` — an epoch above the current one or a non-app operation is never authorized. -- [x] `check_IsAppAllowed_EqualsCurrentEpochDecision` — the legacy - `isAppAllowed` returns exactly the `authorizeApp` result at the current - epoch, never an older policy. +- [x] `check_IsAppAllowed_RefusesAtNonzeroEpoch` — once the app epoch has + advanced, the legacy `isAppAllowed` refuses, since its callers derive + epoch-0 keys. +- [x] `check_IsAppAllowed_EqualsEpochZeroDecisionBeforeAdvance` — at app + epoch 0, with the next row prepared and any one owner write, the legacy + `isAppAllowed` returns exactly the `authorizeApp` result at epoch 0. - [x] `check_PolicyWrite_PreservesOtherEpochDecisions` — a policy write at one epoch, through the explicit or the current-epoch setters, never changes an authorization decision at another epoch, including epoch @@ -144,8 +148,9 @@ and admits one app per epoch, then one symbolic owner write where noted): Mutation-tested: requiring both the any-device flag and a listed device, ignoring the value of a per-epoch `allowAnyDevice` write, dropping a setter's -epoch bound, aliasing epoch 1 onto the -legacy fields, deciding `isAppAllowed` at epoch 0, a permissionless +epoch bound or widening it past the next epoch, aliasing epoch 1 onto the +legacy fields, letting `isAppAllowed` decide at a nonzero epoch or read the +prepared next row, a permissionless `advanceAppEpoch` and dropping its stale-transaction guard each produce a counterexample. Dropping the inactive-epoch check in `_authorizeApp` does not: policy for an inactive epoch cannot be written, so that check is @@ -179,16 +184,17 @@ per epoch, and deploys an app at app epoch 1): exactly when both epochs are active, the selected root epoch admits the OS image, and the app's own `authorizeApp` admits it. - [x] `check_KmsPolicyWrite_PreservesOtherEpochDecisions` — a KMS policy - write at one root epoch, through the explicit or the latest-epoch - setters, never changes a KMS decision at another epoch. -- [x] `check_LegacyEntryPoints_FollowCurrentEpochs` — `isKmsAllowed` - decides as `kms_serve` at the current root epoch, and `isAppAllowed` - denies an app that has left app epoch 0. + write at one root epoch, or through the epoch-less setters at every + epoch from the current one to the latest, never changes a KMS decision + at an epoch it did not write. +- [x] `check_LegacyEntryPoints_ReadEpochZero` — `isKmsAllowed` decides as + `kms_serve` at root epoch 0, and `isAppAllowed` denies an app that has + left app epoch 0. Mutation-tested: a chain hash that ignores the previous epoch, activation that leaves `kmsInfo` stale, a pop that ignores the chain hash, app requests selecting a pending root epoch, KMS requests limited to the current epoch, -`isKmsAllowed` checking the latest epoch, accepting an `0x04` k256 tag, an +`isKmsAllowed` checking the current epoch, accepting an `0x04` k256 tag, an OS image row aliasing epoch 1 onto the legacy row, an app check skipping the OS image, and non-bootstrap operations before registration each produce a counterexample. diff --git a/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol index c43c989e4..97e8acf01 100644 --- a/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol +++ b/dstack/kms/auth-eth/test/DstackAppEpoch.symbolic.t.sol @@ -11,6 +11,21 @@ import "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol"; import "../contracts/AuthorizationOperation.sol"; import "../contracts/DstackApp.sol"; +function _appAuth( + DstackApp target, + IAppAuth.AppInfo memory info, + uint256 epoch, + bytes32 operation +) + view + returns (bool, string memory) +{ + AuthorizationResult memory result = target.authorizeApp( + AuthorizationRequest(info, operation, OptionalUint256(true, epoch), OptionalUint256(false, 0)) + ); + return (result.authorized, result.rejectionReason); +} + /// @notice Halmos symbolic tests for DstackApp app epochs. /// /// Halmos has no symbolic storage, so tests that quantify over policy states @@ -93,7 +108,7 @@ contract DstackAppEpochSymbolicTest is Test { } function _decision(IAppAuth.AppInfo memory info, uint256 epoch) internal view returns (bool, bytes32) { - (bool allowed, string memory reason) = app.authorizeApp(info, epoch, AuthorizationOperation.APP_GET_KEY); + (bool allowed, string memory reason) = _appAuth(app, info, epoch, AuthorizationOperation.APP_GET_KEY); return (allowed, keccak256(bytes(reason))); } @@ -140,7 +155,7 @@ contract DstackAppEpochSymbolicTest is Test { // No caller can write policy for an epoch that is not active yet. // --------------------------------------------------------------- - function check_PolicyWrite_RejectsInactiveEpoch( + function check_PolicyWrite_RejectsEpochPastNext( address caller, uint256 which, uint256 epoch, @@ -149,7 +164,7 @@ contract DstackAppEpochSymbolicTest is Test { ) external { - vm.assume(which < 5 && epoch > app.currentAppEpoch()); + vm.assume(which < 5 && epoch > app.currentAppEpoch() + 1); (bytes memory data,) = _policyCall(which, epoch, word, flag); vm.prank(caller); (bool ok,) = address(app).call(data); @@ -177,7 +192,7 @@ contract DstackAppEpochSymbolicTest is Test { _ownerPolicyWrite(which, writeEpoch, word, flag); IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); vm.assume(epoch > app.currentAppEpoch() || !AuthorizationOperation.isApp(operation)); - (bool allowed,) = app.authorizeApp(info, epoch, operation); + (bool allowed,) = _appAuth(app, info, epoch, operation); assert(!allowed); } @@ -186,7 +201,7 @@ contract DstackAppEpochSymbolicTest is Test { // epoch-aware one at the current epoch, never an older policy. // --------------------------------------------------------------- - function check_IsAppAllowed_EqualsCurrentEpochDecision( + function check_IsAppAllowed_RefusesAtNonzeroEpoch( uint256 which, uint256 writeEpoch, bytes32 word, @@ -197,10 +212,38 @@ contract DstackAppEpochSymbolicTest is Test { ) external { + _ownerPolicyWrite(which, writeEpoch, word, flag); + (bool allowed, string memory reason) = app.isAppAllowed(_info(composeHash, deviceId, upToDate)); + assert(!allowed); + assert(keccak256(bytes(reason)) == keccak256("App epoch requires epoch-aware authorization")); + } + + function check_IsAppAllowed_EqualsEpochZeroDecisionBeforeAdvance( + uint256 which, + uint256 writeEpoch, + bytes32 word, + bool flag, + bytes32 composeHash, + bytes32 deviceId, + bool upToDate + ) + external + { + bytes memory initData = abi.encodeWithSignature( + "initialize(address,bool,bool,bytes32,bytes32)", OWNER, false, false, bytes32(0), bytes32(0) + ); + app = DstackApp(address(new ERC1967Proxy(address(new DstackApp()), initData))); + vm.startPrank(OWNER); + app.addComposeHash(bytes32(uint256(0xc0))); + app.addDevice(bytes32(uint256(0xd0))); + // A prepared next row must not leak into the legacy decision. + app.addComposeHashAtEpoch(1, bytes32(uint256(0xc1))); + app.setAllowAnyDeviceAtEpoch(1, true); + vm.stopPrank(); _ownerPolicyWrite(which, writeEpoch, word, flag); IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); (bool allowed, string memory reason) = app.isAppAllowed(info); - (bool expected, bytes32 expectedReason) = _decision(info, app.currentAppEpoch()); + (bool expected, bytes32 expectedReason) = _decision(info, 0); assert(allowed == expected && keccak256(bytes(reason)) == expectedReason); } @@ -255,7 +298,7 @@ contract DstackAppEpochSymbolicTest is Test { _ownerPolicyWrite(which, writeEpoch, word, flag); IAppAuth.AppInfo memory info = _info(composeHash, deviceId, upToDate); bytes32 op = getCert ? AuthorizationOperation.APP_GET_CERT : AuthorizationOperation.APP_GET_KEY; - (bool allowed,) = app.authorizeApp(info, epoch, op); + (bool allowed,) = _appAuth(app, info, epoch, op); bool expected = epoch <= app.currentAppEpoch() && (!tcbFlag || upToDate) && app.allowedComposeHashesAtEpoch(epoch, composeHash) && (app.allowAnyDeviceAtEpoch(epoch) || app.allowedDeviceIdsAtEpoch(epoch, deviceId)); diff --git a/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol index 3df82de83..52ebca400 100644 --- a/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol +++ b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol @@ -12,6 +12,21 @@ import "../contracts/AuthorizationOperation.sol"; import "../contracts/DstackApp.sol"; import "../contracts/DstackKms.sol"; +function _appAuth( + DstackApp target, + IAppAuth.AppInfo memory info, + uint256 epoch, + bytes32 operation +) + view + returns (bool, string memory) +{ + AuthorizationResult memory result = target.authorizeApp( + AuthorizationRequest(info, operation, OptionalUint256(true, epoch), OptionalUint256(false, 0)) + ); + return (result.authorized, result.rejectionReason); +} + /// @notice Halmos symbolic tests for DstackKms root epochs and epoch-scoped /// authorization. /// @@ -101,11 +116,9 @@ contract DstackKmsEpochSymbolicTest is Test { ) internal pure - returns (DstackKms.AuthorizationRequest memory) + returns (AuthorizationRequest memory) { - return DstackKms.AuthorizationRequest( - info, operation, DstackKms.OptionalUint256(appSet, appEpoch), DstackKms.OptionalUint256(rootSet, root) - ); + return AuthorizationRequest(info, operation, OptionalUint256(appSet, appEpoch), OptionalUint256(rootSet, root)); } /// Calldata of one KMS policy setter and the root epoch it writes. @@ -118,8 +131,10 @@ contract DstackKmsEpochSymbolicTest is Test { view returns (bytes memory data, uint256 target) { - // Setters without an epoch write the latest registered epoch, pending included. - target = which < 6 ? epoch : kms.rootEpochCount() - 1; + // Setters without an epoch write every row from the current epoch to the + // latest registered one; `target` is the lowest row written. + (target,) = kms.currentRootEpoch(); + if (which < 6) target = epoch; if (which == 0) data = abi.encodeCall(DstackKms.addKmsAggregatedMrAtEpoch, (epoch, word)); else if (which == 1) data = abi.encodeCall(DstackKms.removeKmsAggregatedMrAtEpoch, (epoch, word)); else if (which == 2) data = abi.encodeCall(DstackKms.addKmsDeviceAtEpoch, (epoch, word)); @@ -312,8 +327,8 @@ contract DstackKmsEpochSymbolicTest is Test { external view { - DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, rootSet, root, appSet, appEpoch); - DstackKms.AuthorizationResult memory result = isKms ? kms.authorizeKms(request) : kms.authorizeApp(request); + AuthorizationRequest memory request = _request(_info(id), operation, rootSet, root, appSet, appEpoch); + AuthorizationResult memory result = isKms ? kms.authorizeKms(request) : kms.authorizeApp(request); (uint256 current, bytes32 currentHash) = kms.currentRootEpoch(); assert(result.currentRootEpoch == current && result.currentRootEpochHash == currentHash); @@ -322,7 +337,7 @@ contract DstackKmsEpochSymbolicTest is Test { uint256 rootBound = isKms ? kms.rootEpochCount() - 1 : current; uint256 appBound = isKms ? 0 : app.currentAppEpoch(); if (!kindMatches || (rootSet && root > rootBound) || (appSet && appEpoch > appBound)) { - assert(!result.isAllowed); + assert(!result.authorized); } } @@ -347,9 +362,9 @@ contract DstackKmsEpochSymbolicTest is Test { fresh.addKmsDevice(id.deviceId); vm.stopPrank(); - DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, false, 0, false, 0); - DstackKms.AuthorizationResult memory result = isKms ? fresh.authorizeKms(request) : fresh.authorizeApp(request); - if (result.isAllowed) assert(isKms && operation == AuthorizationOperation.KMS_BOOTSTRAP); + AuthorizationRequest memory request = _request(_info(id), operation, false, 0, false, 0); + AuthorizationResult memory result = isKms ? fresh.authorizeKms(request) : fresh.authorizeApp(request); + if (result.authorized) assert(isKms && operation == AuthorizationOperation.KMS_BOOTSTRAP); } // --------------------------------------------------------------- @@ -375,15 +390,14 @@ contract DstackKmsEpochSymbolicTest is Test { ok; } - DstackKms.AuthorizationResult memory result = - kms.authorizeKms(_request(_info(id), operation, rootSet, root, false, 0)); + AuthorizationResult memory result = kms.authorizeKms(_request(_info(id), operation, rootSet, root, false, 0)); uint256 epoch = rootSet ? root : _current(); bool expected = AuthorizationOperation.isKms(operation) && epoch < kms.rootEpochCount() && id.upToDate && kms.allowedOsImagesAtEpoch(epoch, id.osImageHash) && kms.kmsAllowedAggregatedMrsAtEpoch(epoch, id.mrAggregated) && kms.kmsAllowedDeviceIdsAtEpoch(epoch, id.deviceId); - assert(result.isAllowed == expected); + assert(result.authorized == expected); } // --------------------------------------------------------------- @@ -405,15 +419,14 @@ contract DstackKmsEpochSymbolicTest is Test { { bytes32 operation = getCert ? AuthorizationOperation.APP_GET_CERT : AuthorizationOperation.APP_GET_KEY; IAppAuth.AppInfo memory info = _info(id); - DstackKms.AuthorizationResult memory result = - kms.authorizeApp(_request(info, operation, rootSet, root, appSet, appEpoch)); + AuthorizationResult memory result = kms.authorizeApp(_request(info, operation, rootSet, root, appSet, appEpoch)); uint256 rootEpoch = rootSet ? root : _current(); uint256 selectedAppEpoch = appSet ? appEpoch : app.currentAppEpoch(); bool expected = rootEpoch <= _current() && selectedAppEpoch <= app.currentAppEpoch() && kms.allowedOsImagesAtEpoch(rootEpoch, id.osImageHash); - if (expected) (expected,) = app.authorizeApp(info, selectedAppEpoch, operation); - assert(result.isAllowed == expected); + if (expected) (expected,) = _appAuth(app, info, selectedAppEpoch, operation); + assert(result.authorized == expected); } // --------------------------------------------------------------- @@ -433,31 +446,32 @@ contract DstackKmsEpochSymbolicTest is Test { { vm.assume(which < KMS_POLICY_SETTERS); (bytes memory data, uint256 target) = _kmsPolicyCall(which, writeEpoch, word); - vm.assume(target != root); + // Epoch-less setters write every row from `target` on. + vm.assume(which < 6 ? target != root : root < target); - DstackKms.AuthorizationRequest memory request = _request(_info(id), operation, true, root, false, 0); - DstackKms.AuthorizationResult memory before = kms.authorizeKms(request); + AuthorizationRequest memory request = _request(_info(id), operation, true, root, false, 0); + AuthorizationResult memory before = kms.authorizeKms(request); vm.prank(OWNER); (bool ok,) = address(kms).call(data); ok; - DstackKms.AuthorizationResult memory afterWrite = kms.authorizeKms(request); + AuthorizationResult memory afterWrite = kms.authorizeKms(request); - assert(before.isAllowed == afterWrite.isAllowed); + assert(before.authorized == afterWrite.authorized); assert(keccak256(bytes(before.rejectionReason)) == keccak256(bytes(afterWrite.rejectionReason))); } // --------------------------------------------------------------- - // Legacy entry points: isKmsAllowed decides as KMS_SERVE at the - // current root epoch, and isAppAllowed never authorizes an app - // whose policy has left app epoch 0. + // Legacy entry points: isKmsAllowed decides as KMS_SERVE at root + // epoch 0, and isAppAllowed never authorizes an app whose policy has + // left app epoch 0. // --------------------------------------------------------------- - function check_LegacyEntryPoints_FollowCurrentEpochs(Identity calldata id) external view { + function check_LegacyEntryPoints_ReadEpochZero(Identity calldata id) external view { IAppAuth.AppInfo memory info = _info(id); (bool kmsAllowed,) = kms.isKmsAllowed(info); - DstackKms.AuthorizationResult memory serve = - kms.authorizeKms(_request(info, AuthorizationOperation.KMS_SERVE, false, 0, false, 0)); - assert(kmsAllowed == serve.isAllowed); + AuthorizationResult memory serve = + kms.authorizeKms(_request(info, AuthorizationOperation.KMS_SERVE, true, 0, false, 0)); + assert(kmsAllowed == serve.authorized); (bool appAllowed,) = kms.isAppAllowed(info); assert(!appAllowed); From 297a1e2e6edf2cd325cbf407792fb95e81619cc5 Mon Sep 17 00:00:00 2001 From: Kevin Wang Date: Mon, 9 Nov 2026 07:31:29 -0800 Subject: [PATCH 5/5] test(auth-eth): check that legacy entry points refuse once rotated Since #1545, isKmsAllowed and isAppAllowed refuse while a later root epoch is current. Replace the epoch-0 equivalence check, which setUp's rotated state no longer reaches, with two checks: both entry points refuse after a rotation, and before any rotation isKmsAllowed decides as kms_serve at epoch 0 even with the next epoch registered and prepared. Removing either rotation guard or reading the pending row each produce a counterexample. Signed-off-by: Kevin Wang --- .../kms/auth-eth/docs/formal-verification.md | 10 +++--- .../test/DstackKmsEpoch.symbolic.t.sol | 32 +++++++++++++++---- 2 files changed, 31 insertions(+), 11 deletions(-) diff --git a/dstack/kms/auth-eth/docs/formal-verification.md b/dstack/kms/auth-eth/docs/formal-verification.md index 9d59e6101..8a5bed9a0 100644 --- a/dstack/kms/auth-eth/docs/formal-verification.md +++ b/dstack/kms/auth-eth/docs/formal-verification.md @@ -187,14 +187,16 @@ per epoch, and deploys an app at app epoch 1): write at one root epoch, or through the epoch-less setters at every epoch from the current one to the latest, never changes a KMS decision at an epoch it did not write. -- [x] `check_LegacyEntryPoints_ReadEpochZero` — `isKmsAllowed` decides as - `kms_serve` at root epoch 0, and `isAppAllowed` denies an app that has - left app epoch 0. +- [x] `check_LegacyEntryPoints_RefuseOnceRotated` — once a later root epoch + is current, `isKmsAllowed` and `isAppAllowed` refuse. +- [x] `check_LegacyKmsCheck_ReadsEpochZeroBeforeRotation` — before any + rotation, with the next epoch registered and prepared, `isKmsAllowed` + decides as `kms_serve` at root epoch 0. Mutation-tested: a chain hash that ignores the previous epoch, activation that leaves `kmsInfo` stale, a pop that ignores the chain hash, app requests selecting a pending root epoch, KMS requests limited to the current epoch, -`isKmsAllowed` checking the current epoch, accepting an `0x04` k256 tag, an +`isKmsAllowed` reading the pending epoch or still deciding after a rotation, accepting an `0x04` k256 tag, an OS image row aliasing epoch 1 onto the legacy row, an app check skipping the OS image, and non-bootstrap operations before registration each produce a counterexample. diff --git a/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol index 52ebca400..1ffe7ff84 100644 --- a/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol +++ b/dstack/kms/auth-eth/test/DstackKmsEpoch.symbolic.t.sol @@ -461,19 +461,37 @@ contract DstackKmsEpochSymbolicTest is Test { } // --------------------------------------------------------------- - // Legacy entry points: isKmsAllowed decides as KMS_SERVE at root - // epoch 0, and isAppAllowed never authorizes an app whose policy has - // left app epoch 0. + // Legacy entry points serve KMS binaries that only hold root epoch 0: + // before any rotation isKmsAllowed decides as KMS_SERVE at epoch 0, + // and once a later epoch is current both refuse. isAppAllowed never + // authorizes an app whose policy has left app epoch 0. // --------------------------------------------------------------- - function check_LegacyEntryPoints_ReadEpochZero(Identity calldata id) external view { + function check_LegacyEntryPoints_RefuseOnceRotated(Identity calldata id) external view { + IAppAuth.AppInfo memory info = _info(id); + bytes32 rotated = keccak256("Root epoch requires epoch-aware authorization"); + (bool kmsAllowed, string memory kmsReason) = kms.isKmsAllowed(info); + assert(!kmsAllowed && keccak256(bytes(kmsReason)) == rotated); + (bool appAllowed, string memory appReason) = kms.isAppAllowed(info); + assert(!appAllowed && keccak256(bytes(appReason)) == rotated); + } + + function check_LegacyKmsCheck_ReadsEpochZeroBeforeRotation(Identity calldata id) external { + bytes memory initData = abi.encodeCall(DstackKms.initialize, (OWNER, address(new DstackApp()))); + kms = DstackKms(address(new ERC1967Proxy(address(new DstackKms()), initData))); + vm.startPrank(OWNER); + for (uint256 epoch = 0; epoch < 2; epoch++) { + kms.registerRootEpoch(_ca(bytes32(epoch + 1), bytes32(0)), _k256(true, bytes32(epoch + 1)), "evidence"); + kms.addOsImageHashAtEpoch(epoch, _id(0x05, epoch)); + kms.addKmsAggregatedMrAtEpoch(epoch, _id(0x0a, epoch)); + kms.addKmsDeviceAtEpoch(epoch, _id(0x0d, epoch)); + } + vm.stopPrank(); + // Epoch 1 is registered and prepared but pending. IAppAuth.AppInfo memory info = _info(id); (bool kmsAllowed,) = kms.isKmsAllowed(info); AuthorizationResult memory serve = kms.authorizeKms(_request(info, AuthorizationOperation.KMS_SERVE, true, 0, false, 0)); assert(kmsAllowed == serve.authorized); - - (bool appAllowed,) = kms.isAppAllowed(info); - assert(!appAllowed); } }