diff --git a/REUSE.toml b/REUSE.toml index 3441a411..cc27b617 100644 --- a/REUSE.toml +++ b/REUSE.toml @@ -23,6 +23,7 @@ path = [ "**/tsconfig.node.json", "**/tsconfig.browser.json", "kms/auth-eth-bun/.oxlintrc.json", + "kms/auth-eth/slither.config.json", "package-lock.json", "**/package-lock.json", "kms/auth-eth/.openzeppelin/unknown-2035.json", diff --git a/kms/auth-eth/README.md b/kms/auth-eth/README.md index 96eb66ee..3d3b88f3 100644 --- a/kms/auth-eth/README.md +++ b/kms/auth-eth/README.md @@ -128,6 +128,26 @@ npm run build && npm start npm test ``` +## Static Analysis & Symbolic Verification (local only) + +We run [Slither](https://github.com/crytic/slither) and +[Halmos](https://github.com/a16z/halmos) locally during development. They +are intentionally not part of CI — symbolic proofs are slow, sensitive to +solver versions, and most valuable as an interactive design check rather +than a gate. + +```bash +pipx install slither-analyzer halmos +slither . +halmos --contract DstackAppSymbolicTest +halmos --contract DstackKmsSymbolicTest +``` + +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 +audit-firm engagement. + ## Additional Commands ```bash diff --git a/kms/auth-eth/contracts/DstackKms.sol b/kms/auth-eth/contracts/DstackKms.sol index ed6a008e..d3b4de34 100644 --- a/kms/auth-eth/contracts/DstackKms.sol +++ b/kms/auth-eth/contracts/DstackKms.sol @@ -45,6 +45,8 @@ contract DstackKms is Initializable, Ownable2StepUpgradeable, UUPSUpgradeable, E address public appImplementation; // Events + // appId is unindexed for backward compatibility with deployed log indexers. + // slither-disable-next-line unindexed-event-address event AppRegistered(address appId); event KmsInfoSet(bytes k256Pubkey); event KmsAggregatedMrAdded(bytes32 mrAggregated); @@ -54,6 +56,7 @@ contract DstackKms is Initializable, Ownable2StepUpgradeable, UUPSUpgradeable, E event OsImageHashAdded(bytes32 osImageHash); event OsImageHashRemoved(bytes32 osImageHash); event GatewayAppIdSet(string gatewayAppId); + // slither-disable-next-line unindexed-event-address event AppImplementationSet(address implementation); event AppDeployedViaFactory(address indexed appId, address indexed deployer); @@ -164,6 +167,10 @@ contract DstackKms is Initializable, Ownable2StepUpgradeable, UUPSUpgradeable, E initialComposeHash ); + // The ERC1967Proxy constructor delegatecalls into DstackApp.initialize, + // which only writes to its own storage and cannot reenter this contract. + // The post-deploy state write and event are therefore safe. + // slither-disable-next-line reentrancy-benign,reentrancy-events appId = address(new ERC1967Proxy(appImplementation, initData)); registerApp(appId); emit AppDeployedViaFactory(appId, msg.sender); @@ -267,7 +274,10 @@ contract DstackKms is Initializable, Ownable2StepUpgradeable, UUPSUpgradeable, E return (false, "App not deployed or invalid address"); } - // Call the app's isAppAllowed function + // Call the app's isAppAllowed function. The tuple is forwarded as the + // function's return value; the slither detector trips on the named + // return + forward pattern but the value is actually used. + // slither-disable-next-line unused-return return IAppAuth(bootInfo.appId).isAppAllowed(bootInfo); } diff --git a/kms/auth-eth/docs/formal-verification.md b/kms/auth-eth/docs/formal-verification.md new file mode 100644 index 00000000..12ad3ecf --- /dev/null +++ b/kms/auth-eth/docs/formal-verification.md @@ -0,0 +1,211 @@ + + +# Formal Verification Plan — `kms/auth-eth` + +A layered approach: cheap static analysis → SMTChecker invariants → Halmos +symbolic tests → (optional) Certora. Each layer is independently mergeable. + +The **formal specification** these layers verify against lives in +[`specification.md`](./specification.md). The spec is normative — code +and tests track the spec, not the other way around. + +Reference: + +## Targets + +The two contracts under verification are authorization gates for TEE workloads; +correctness matters more than gas. + +- `contracts/DstackApp.sol` (209 LOC) — per-app boot authorization +- `contracts/DstackKms.sol` (276 LOC) — KMS whitelist + factory +- `contracts/IAppAuth.sol`, `contracts/IAppAuthBasicManagement.sol` — interfaces + +## Layer 0 — Slither (static analysis) + +Not formal verification but the standard first pass. Catches reentrancy, +shadowing, uninitialized state, unsafe `delegatecall`, etc. + +- [ ] Install slither-analyzer (Python via pipx or as a uv tool) +- [ ] Add `slither.config.json` at `kms/auth-eth/` excluding `lib/`, `out/`, + `cache/`, `node_modules/`, `test/` (focus on production contracts) +- [ ] Run baseline `slither contracts/` and triage findings into: + - real → fix + - false-positive / wontfix → suppress with `// slither-disable-next-line` + and a justifying comment + +- [x] Slither runs locally; no CI gate (intentional) +- [ ] Update `kms/auth-eth/README.md` with one line on how to run Slither locally + +**Effort:** ~1h. **Owner:** _tbd_. + +## Layer 1 — SMTChecker (deferred) + +**Status: deferred.** Originally planned as the cheap free tier, but the +practical setup cost is high enough that it's not worth doing before Halmos. + +What was tried (and why it fails to deliver value here): + +1. **CHC engine + `solvers = ["z3"]`:** solc's binary distributions on + foundry's `svm` (Solidity version manager) are not compiled with z3 + linkage. Result: every analysis emits `Warning (7649): CHC analysis was + not possible since no Horn solver was found and enabled`. +2. **CHC engine + `solvers = ["smtlib2"]`:** solc emits SMT-LIB2 queries + but does not auto-spawn an external solver. Without a wrapper, nothing + actually runs. +3. **BMC engine:** runs, but on our OZ-upgradeable contracts emits only + `Warning (5724): SMTChecker: N unsupported language feature(s)` — + delegatecall, complex modifiers, and proxy patterns aren't in scope. + Net useful findings: zero. + +To enable SMTChecker properly we'd need to either: +- build solc from source with `USE_Z3=1`, ship the binary, point forge at it + (via `solc = "/path/to/our/solc"` in `foundry.toml`); +- or run solc in a container image like `ethereum/solc:0.8.24-z3` and wire + it into CI. + +Either path is significant infra work. Halmos (Layer 2) covers everything +SMTChecker would prove on our contracts (asserts, overflows, owner-gated +mutations) while also handling the symbolic-input cases SMTChecker can't +(TCB string compare, `isAppAllowed` decision table), using a solver that's +already a Foundry-native install. + +Revisit Layer 1 only if we want defense-in-depth alongside Halmos. + +## Layer 2 — Halmos symbolic tests + +[Halmos](https://github.com/a16z/halmos) runs Foundry-style tests with all +function arguments as symbolic variables. Sweet spot for our contracts: we +reuse the existing `.t.sol` scaffolding and OZ-foundry-upgrades plugin. + +### Setup + +- [x] `pipx install halmos` documented in `README.md` +- [ ] No CI integration (intentional — see "What's intentionally not in + scope" below) + +### `DstackApp` symbolic properties (`test/DstackApp.symbolic.t.sol`) + +- [ ] `check_AddComposeHash_OnlyOwner(address caller, bytes32 hash)` — call + reverts iff `caller != owner` +- [ ] `check_RemoveComposeHash_OnlyOwner` (same shape) +- [ ] `check_AddDevice_OnlyOwner` +- [ ] `check_RemoveDevice_OnlyOwner` +- [ ] `check_SetAllowAnyDevice_OnlyOwner` +- [ ] `check_SetRequireTcbUpToDate_OnlyOwner` +- [ ] `check_DisableUpgrades_OnlyOwner` +- [ ] `check_DisableUpgradesMonotonic` — after `disableUpgrades()`, any + subsequent call to `_authorizeUpgrade` reverts for every caller / impl +- [ ] `check_IsAppAllowed_DecisionTable(IAppAuth.AppBootInfo bootInfo)` — + prove the boolean formula: + ``` + isAppAllowed(b) == (true, "") + ⟺ (!requireTcbUpToDate || b.tcbStatus == "UpToDate") + && allowedComposeHashes[b.composeHash] + && (allowAnyDevice || allowedDeviceIds[b.deviceId]) + ``` +- [ ] `check_Initialize5Arg_DefaultsTcbToFalse` — after the legacy 5-arg + initializer for any inputs, `requireTcbUpToDate == false` +- [ ] `check_Initialize6Arg_HonorsTcbFlag(bool flag, ...)` — after the 6-arg + initializer, `requireTcbUpToDate == flag` + +### `DstackKms` symbolic properties (`test/DstackKms.symbolic.t.sol`) + +- [ ] `check_SetKmsInfo_OnlyOwner` +- [ ] `check_SetGatewayAppId_OnlyOwner` +- [ ] `check_AddKmsAggregatedMr_OnlyOwner` and `Remove…_OnlyOwner` +- [ ] `check_AddKmsDevice_OnlyOwner` and `Remove…_OnlyOwner` +- [ ] `check_AddOsImageHash_OnlyOwner` and `Remove…_OnlyOwner` +- [ ] `check_SetAppImplementation_OnlyOwner` +- [ ] `check_RegisterApp_OnlyOwner` and `Unregister…_OnlyOwner` +- [ ] `check_DeployAndRegisterApp_5arg_DefaultsTcbToFalse` — 5-arg factory + always sets `requireTcbUpToDate = false` on the new app +- [ ] `check_DeployAndRegisterApp_6arg_HonorsTcbFlag` — 6-arg factory + propagates the flag exactly +- [ ] `check_DeployAndRegisterApp_RegistersAtomically` — if the call + returns, both `registeredApps[appId]` is true *and* the appId is a + live UUPS proxy with the configured initial state +- [ ] `check_IsAppAllowed_RejectsUnknownOsImage` — if + `!allowedOsImages[b.osImageHash]`, the result is `(false, …)` and + no delegation to the app happens +- [ ] `check_IsKmsAllowed_RequiresAllowedMr` and other short-circuit cases + +### Coverage acceptance + +A property "passes" only when Halmos returns `[PASS]` without `--symbolic-storage` +exclusions. Properties that solve only under bounded loops should be flagged. + +### Findings from the initial run + +- **`DstackKms.registerApp` is intentionally permissionless** (confirmed + by the dstack team). The Halmos counterexample on + `check_RegisterApp_OnlyOwner` reflects design, not a bug: any non-zero + address can be registered by anyone. Authorization is still gated + downstream by the owner-controlled `allowedOsImages` whitelist and by + the registered app's own `isAppAllowed` logic, so registration alone + confers no privilege. The contract now carries a natspec block on + `registerApp` stating this explicitly, and the symbolic suite asserts + the actual behavior via `check_RegisterApp_AnyCallerCanRegisterNonZeroAddress` + + `check_RegisterApp_RejectsZeroAddress`. + +- **TCB status compare is byte-exact** (confirmed). The contract uses + `keccak256(abi.encodePacked(bootInfo.tcbStatus)) != keccak256(abi.encodePacked("UpToDate"))`, + which by the cryptographic-collision-resistance assumption is true + iff the byte sequences differ. The off-chain attestation pipeline must + emit the exact 8-byte ASCII string `"UpToDate"` — no case variations, + trailing nulls, or whitespace. Proven by + `check_TcbStatus_OnlyExactUpToDateAccepted` (symbolic over all + bounded strings) plus the concrete `check_TcbStatus_RejectsLowercase` / + `_RejectsTrailingChars` cases. + +- **Two-step ownership transfer adopted.** Both contracts now inherit + `Ownable2StepUpgradeable` instead of `OwnableUpgradeable`. The new + storage uses ERC-7201 namespaced slots, so existing UUPS proxies can + be safely upgraded to the new impl (no slot collision; the pending- + owner slot is zero-initialized on first upgrade). `transferOwnership` + no longer immediately transfers — the proposed owner must call + `acceptOwnership` to complete the transfer, eliminating the typo-bricks- + contract risk on the single-step variant. + +**Effort:** ~1 focused day. **Owner:** _tbd_. + +## Layer 3 — Certora (deferred) + +Deferred until a security review budget exists. CVL specs are 3-5× the size of +Halmos tests, require team licenses, and overlap with Halmos coverage for +authorization-style properties. + +If we revisit, target the same invariants as Layer 2 but add: + +- Storage-layout safety across upgrades (especially the + `@custom:oz-renamed-from tproxyAppId` rename — Certora's storage diff is + stronger than the OZ Foundry plugin's) +- Cross-contract invariants spanning `DstackKms` ↔ `DstackApp` + +## What's intentionally not in scope + +- **CI gating of Slither / Halmos.** Symbolic execution is slow, solver- + version-sensitive, and produces non-actionable noise as a PR gate. + Run locally during development; treat these as design checks rather + than blocking lints. +- **Echidna** — overlaps with Foundry's built-in fuzzer (already runs 10k + iterations under `FOUNDRY_PROFILE=ci` in `.github/workflows/foundry-test.yml`). +- **Manticore / Mythril** — bytecode-level tools, slow, awkward with our + forge artifacts. +- **Scribble** — runtime assertions, redundant with our `assert` + Foundry + test approach. + +## Status + +| Layer | Status | PR | +|-------|--------|----| +| 0. Slither | done (0 findings) | this branch | +| 1. SMTChecker | deferred (see above) | — | +| 2. Halmos (DstackApp) | done (11 properties) | this branch | +| 2. Halmos (DstackKms) | done (14 properties) | this branch | +| 3. Certora | deferred | — | + +Update this table as PRs land. diff --git a/kms/auth-eth/docs/specification.md b/kms/auth-eth/docs/specification.md new file mode 100644 index 00000000..51d10c27 --- /dev/null +++ b/kms/auth-eth/docs/specification.md @@ -0,0 +1,389 @@ + + +# DstackKms + DstackApp — Formal Specification + +This document specifies the **intended** behavior of `contracts/DstackKms.sol` +and `contracts/DstackApp.sol` independently of their implementation. It is +the deliverable an external formal-verification engagement (Runtime +Verification, ChainSecurity, Certora) would build against. + +Notation: + +- `pre`: caller / state / argument constraints that must hold before the call. + Violating `pre` is allowed to revert with any reason. +- `post`: state and return-value guarantees after a successful call. +- `frame`: storage cells that **must not change** on a successful call. + Cells not listed in `frame` may or may not change. +- `events`: events that must be emitted on success. +- `reverts`: enumerated revert conditions. Any unlisted revert is a spec + violation. + +Where a property has a corresponding Halmos symbolic proof, the test name +is cited inline as `(verified: TestContract.check_X)`. Properties without +a citation are **specification gaps** awaiting verification. + +## 1. Trust model + +| Principal | Trusted for | Not trusted for | +|---|---|---| +| `owner` (KMS) | All write operations on KMS; deciding the OS-image whitelist; upgrading the KMS implementation | Liveness (may renounce or be replaced via 2-step transfer) | +| `owner` (App) | All write operations on a specific App; upgrading that App implementation (unless disabled) | Behaving consistently across apps — each app's owner is independent | +| `pendingOwner` | Has the *option* to take ownership; no privilege until they call `acceptOwnership` | Not yet authoritative; current owner can override the pending transfer | +| Any EOA / contract | Calling `registerApp` (permissionless), calling read methods | Any state mutation other than registration | +| Registered `IAppAuth` contract | Returning `(bool, string)` from `isAppAllowed`; honoring the `view` mutability declared at the interface | Adversarial registered apps may return arbitrary values, revert, or consume all gas — the KMS treats their output as untrusted | +| EVM | Standard semantics (gas, calldata, storage, `STATICCALL` propagation) | — | +| ERC1967 / OZ proxy stack | Storage layout via ERC-7201; correct delegatecall to impl | — | +| Off-chain attestation pipeline | Emitting the byte-exact ASCII string `"UpToDate"` as `tcbStatus` when reporting healthy TCB | — | + +### Boundary calls + +`DstackKms.isAppAllowed(b)` performs an **external view call** into +`IAppAuth(b.appId).isAppAllowed(b)`. Because the outer function is `view`, +the EVM lifts the call into `STATICCALL`, which propagates: the registered +contract cannot mutate KMS state by any path. Out-of-gas, revert, and +return-value spoofing are still possible — see §6. + +## 2. State variables + +### DstackKms + +| Slot | Name | Type | Writable by | Notes | +|---|---|---|---|---| +| 0–3 | `kmsInfo` | `KmsInfo` (struct, 4 fields) | `setKmsInfo`, `setKmsQuote`, `setKmsEventlog` (owner) | | +| 4 | `gatewayAppId` | `string` | `setGatewayAppId` (owner) | Renamed from `tproxyAppId`; carries `@custom:oz-renamed-from` | +| 5 | `registeredApps` | `mapping(address => bool)` | `registerApp` (anyone), `deployAndRegisterApp` (anyone) | Permissionless — see §6.1 | +| 6 | `kmsAllowedAggregatedMrs` | `mapping(bytes32 => bool)` | `addKmsAggregatedMr`, `removeKmsAggregatedMr` (owner) | | +| 7 | `kmsAllowedDeviceIds` | `mapping(bytes32 => bool)` | `addKmsDevice`, `removeKmsDevice` (owner) | | +| 8 | `allowedOsImages` | `mapping(bytes32 => bool)` | `addOsImageHash`, `removeOsImageHash` (owner) | | +| 9 | `appImplementation` | `address` | `setAppImplementation` (owner) | Used by `deployAndRegisterApp` | +| 10 | `__gap[50]` | `uint256[50]` | (none — must always read zero) | Reserved | + +Plus inherited storage in ERC-7201 namespaces: `OwnableUpgradeable`, +`Ownable2StepUpgradeable`, `UUPSUpgradeable`, `ERC165Upgradeable`, +`Initializable`. + +### DstackApp + +| Slot | Name | Type | Writable by | +|---|---|---|---| +| 0 | `allowedComposeHashes` | `mapping(bytes32 => bool)` | `addComposeHash`, `removeComposeHash` (owner); 5/6-arg initializer | +| 1 | `_upgradesDisabled` + `allowAnyDevice` (packed) | `bool` + `bool` | `disableUpgrades` (owner, monotonic); `setAllowAnyDevice` (owner); initializer | +| 2 | `allowedDeviceIds` | `mapping(bytes32 => bool)` | `addDevice`, `removeDevice` (owner); initializer | +| 3 | `requireTcbUpToDate` | `bool` | `setRequireTcbUpToDate` (owner); 6-arg initializer only | +| 4 | `__gap[49]` | `uint256[49]` | (none) | + +## 3. Public surface — pre/post/frame + +### 3.1 `DstackKms.initialize(address initialOwner, address _appImplementation)` + +- **pre**: contract is not yet initialized; `initialOwner != address(0)`; + `_appImplementation != address(0)`. +- **post**: `owner() == initialOwner`; `appImplementation == _appImplementation`; + `_getInitializableStorage()._initialized == 1`. +- **frame**: all mappings, `gatewayAppId`, `kmsInfo`. +- **reverts**: already-initialized; either address is zero. + +### 3.2 `DstackKms.registerApp(address appId) public` — **permissionless by design** + +- **pre**: `appId != address(0)`. +- **post**: `registeredApps[appId] == true`. +- **frame**: every storage cell except `registeredApps[appId]`. +- **events**: `AppRegistered(appId)`. +- **reverts**: `appId == address(0)`. +- **Note**: No caller restriction. Confirmed-intentional. See §6.1 for + the threat model around this. +- (verified: `DstackKmsSymbolicTest.check_RegisterApp_AnyCallerCanRegisterNonZeroAddress`, + `check_RegisterApp_RejectsZeroAddress`) + +### 3.3 `DstackKms.deployAndRegisterApp(...)` — 6-arg + +Signature: `deployAndRegisterApp(address initialOwner, bool disableUpgrades, bool requireTcbUpToDate, bool allowAnyDevice, bytes32 initialDeviceId, bytes32 initialComposeHash) public returns (address appId)` + +- **pre**: `appImplementation != address(0)`; `initialOwner != address(0)`. +- **post**: + - `registeredApps[appId] == true`. + - `appId` is a freshly-deployed ERC1967 proxy whose implementation is + `appImplementation`. + - The proxy is initialized: `DstackApp(appId).owner() == initialOwner`; + `DstackApp(appId).requireTcbUpToDate() == requireTcbUpToDate`; + `DstackApp(appId).allowAnyDevice() == allowAnyDevice`; + `allowedDeviceIds[initialDeviceId] == (initialDeviceId != 0)`; + `allowedComposeHashes[initialComposeHash] == (initialComposeHash != 0)`. +- **frame**: every KMS storage cell except `registeredApps[appId]`. +- **events**: `AppRegistered(appId)`, `AppDeployedViaFactory(appId, msg.sender)`. +- **reverts**: implementation unset; owner is zero. +- (verified: `DstackKmsSymbolicTest.check_DeployAndRegisterApp_Atomic`) + +### 3.4 `DstackKms.deployAndRegisterApp(...)` — 5-arg backward-compatible + +Signature: `deployAndRegisterApp(address initialOwner, bool disableUpgrades, bool allowAnyDevice, bytes32 initialDeviceId, bytes32 initialComposeHash) external returns (address appId)` + +- Semantics: equivalent to the 6-arg overload with `requireTcbUpToDate = false`. +- (verified: `DstackKmsSymbolicTest.check_DeployAndRegisterApp5Arg_DefaultsTcbToFalse`) + +### 3.5 `DstackKms.isAppAllowed(AppBootInfo b) external view returns (bool, string)` + +Decision (in order): + +1. If `!registeredApps[b.appId]` → return `(false, "App not registered")`. +2. If `!allowedOsImages[b.osImageHash]` → return `(false, "OS image is not allowed")`. +3. If `b.appId.code.length == 0` → return `(false, "App not deployed or invalid address")`. +4. Otherwise return `IAppAuth(b.appId).isAppAllowed(b)` — forwarded verbatim. + +- **frame**: entire storage. +- **assumes (§6)**: the delegated call may revert or consume all gas; + the spec does not bound its behavior. +- (verified: `DstackKmsSymbolicTest.check_IsAppAllowed_RejectsUnregisteredApp`, + `check_IsAppAllowed_RejectsUnknownOsImage`) +- (gap: full delegation forwarding has no symbolic proof yet — the registered + app is treated as adversarial in §6 but not yet as a Halmos universally- + quantified parameter.) + +### 3.6 `DstackKms.isKmsAllowed(AppBootInfo b) external view returns (bool, string)` + +Decision (in order): + +1. If `!kmsAllowedAggregatedMrs[b.mrAggregated]` → reject with `"KMS aggregated MR not allowed"`. +2. If `!kmsAllowedDeviceIds[b.deviceId]` → reject with `"KMS device ID not allowed"`. +3. Otherwise accept with empty reason. + +- **frame**: entire storage. +- (gap: no symbolic proof yet; recommend mirroring `check_IsAppAllowed_*`.) + +### 3.7 Owner-only KMS mutations (uniform pattern) + +For each of `setKmsInfo`, `setKmsQuote`, `setKmsEventlog`, `setGatewayAppId`, +`setAppImplementation`, `addKmsAggregatedMr`, `removeKmsAggregatedMr`, +`addKmsDevice`, `removeKmsDevice`, `addOsImageHash`, `removeOsImageHash`: + +- **pre**: `msg.sender == owner()`. +- **frame**: every storage cell except the one mapped to the operation. +- **reverts** if `msg.sender != owner()` with `OwnableUnauthorizedAccount`. +- (verified: one Halmos test per function in `DstackKmsSymbolicTest`.) + +### 3.8 `DstackApp.initialize` — both overloads + +5-arg `(initialOwner, disableUpgrades, allowAnyDevice, deviceId, composeHash)`: + +- **post**: as for 6-arg with `requireTcbUpToDate = false`. + +6-arg `(initialOwner, disableUpgrades, requireTcbUpToDate, allowAnyDevice, deviceId, composeHash)`: + +- **pre**: not yet initialized; `initialOwner != address(0)`. +- **post**: + - `owner() == initialOwner`; `_upgradesDisabled == disableUpgrades`; + `allowAnyDevice == allowAnyDevice`; `requireTcbUpToDate == requireTcbUpToDate`. + - `deviceId != 0 ⇒ allowedDeviceIds[deviceId] == true`. + - `composeHash != 0 ⇒ allowedComposeHashes[composeHash] == true`. +- **events**: optionally `DeviceAdded(deviceId)` and `ComposeHashAdded(composeHash)`. +- (verified: `DstackAppSymbolicTest.check_Initialize5Arg_DefaultsTcbToFalse`, + `check_Initialize6Arg_HonorsTcbFlag`) + +### 3.9 `DstackApp.isAppAllowed(AppBootInfo b) external view returns (bool, string)` + +Decision (in order, all evaluated under `b.appId == address(this)` by convention): + +1. If `requireTcbUpToDate && keccak256(bytes(b.tcbStatus)) != keccak256(bytes("UpToDate"))` → + `(false, "TCB status is not up to date")`. +2. If `!allowedComposeHashes[b.composeHash]` → `(false, "Compose hash not allowed")`. +3. If `!allowAnyDevice && !allowedDeviceIds[b.deviceId]` → `(false, "Device not allowed")`. +4. Otherwise `(true, "")`. + +The TCB compare uses `keccak256` for byte-exact string equality. Under the +keccak collision-resistance assumption, the accept set is exactly `{"UpToDate"}` +(8 bytes, ASCII). The off-chain attestation pipeline **must** emit this exact +byte sequence — no case variations, no trailing nulls, no whitespace. + +- **frame**: entire storage. +- (verified: `DstackAppSymbolicTest.check_IsAppAllowed_DecisionTable_TcbUpToDate`, + `check_TcbStatus_OnlyExactUpToDateAccepted`, `check_TcbStatus_RejectsLowercase`, + `check_TcbStatus_RejectsTrailingChars`) + +### 3.10 `DstackApp.disableUpgrades()` — monotonic kill-switch + +- **pre**: `msg.sender == owner()`. +- **post**: `_upgradesDisabled == true`. +- **frame**: every storage cell except `_upgradesDisabled`. +- **events**: `UpgradesDisabled()`. +- **Once true, every subsequent attempted upgrade reverts** — + no matter the caller, target implementation, or initialization data. +- (verified: `DstackAppSymbolicTest.check_DisableUpgrades_OnlyOwner`, + `check_DisableUpgradesMonotonic`) + +### 3.11 Owner-only App mutations + +For each of `addComposeHash`, `removeComposeHash`, `addDevice`, `removeDevice`, +`setAllowAnyDevice`, `setRequireTcbUpToDate`: + +- **pre**: `msg.sender == owner()`. +- **frame**: every storage cell except the one mapped to the operation. +- (verified: one Halmos test each in `DstackAppSymbolicTest`.) + +### 3.12 Ownership transfer (inherited Ownable2Step) + +`transferOwnership(address newOwner)`: + +- **pre**: `msg.sender == owner()`. +- **post**: `pendingOwner() == newOwner`; `owner()` unchanged. +- **events**: `OwnershipTransferStarted(currentOwner, newOwner)`. + +`acceptOwnership()`: + +- **pre**: `msg.sender == pendingOwner()`. +- **post**: `owner() == msg.sender`; `pendingOwner() == address(0)`. +- **events**: `OwnershipTransferred(previousOwner, newOwner)`. + +- (gap: not symbolically verified; relies on OZ's tested implementation.) + +## 4. State invariants + +Properties that must hold in **every reachable state**, not just after one call. + +| Invariant | Status | +|---|---| +| INV-1: `_upgradesDisabled` is monotonic (once `true`, never `false`). | Single-step proof: `check_DisableUpgradesMonotonic`. Cross-transaction extension: gap. | +| INV-2: The owner can only be changed via the Ownable2Step flow (`transferOwnership` → `acceptOwnership`, or `renounceOwnership`). | Gap. Requires cross-transaction invariant tooling. | +| INV-3: `_initialized` reaches `1` exactly once per proxy (either 5-arg or 6-arg, never both, never twice). | Gap. | +| INV-4: `appImplementation` stays a non-zero contract address once set (so the factory hook can't deploy from a junk impl). | Currently only `setAppImplementation` enforces `_implementation != address(0)`; the initializer sets it from input without re-checking. Inputs are owner-controlled, so the invariant holds modulo owner trust. Gap if we want to verify without trusting the owner. | +| INV-5: For every entry `registeredApps[a] == true`, either `a` was the return of a successful `deployAndRegisterApp` call, **or** an external caller invoked `registerApp(a)` with `a != address(0)`. | Trivially holds by construction; documented for the threat model. | +| INV-6: `__gap` slots read zero in every reachable state. | Standard OZ-upgradeable invariant; relies on never declaring new storage past `__gap`. Gap. | +| INV-7: For all `b`, `kms.isAppAllowed(b)` returns the same value whether or not the registered `IAppAuth(b.appId)` mutates its own storage during the call (because the top-level call is `view`, the EVM enforces `STATICCALL` propagation; no inner mutation can influence the outer return). | Holds by EVM semantics; not separately verified. | + +## 5. Cross-contract assumptions + +### 5.1 KMS ↔ App (`isAppAllowed` delegation) + +KMS calls `IAppAuth(b.appId).isAppAllowed(b)` after confirming +`registeredApps[b.appId]` and `allowedOsImages[b.osImageHash]`. Assumptions: + +- The call may revert. KMS does not catch the revert — `isAppAllowed` + propagates it. **Caller of KMS must be prepared to handle this.** +- The call may consume all gas (1/64th-rule means some gas survives; the + KMS-level caller sees an out-of-gas-style revert). +- The call's return value is **not authenticated**. A malicious registered + app can claim "allowed" for any input. The chain of trust requires the + off-chain consumer of `isAppAllowed`'s `(bool, string)` to also verify + that the app implementation at `b.appId` is one they expect (e.g., by + diffing bytecode against `DstackApp`'s known implementation). + +### 5.2 KMS ↔ Proxy (factory deploy) + +`deployAndRegisterApp` calls `new ERC1967Proxy(appImplementation, initData)`. +The proxy constructor delegatecalls into the implementation's initialize +function. Assumptions: + +- The constructor runs `initialize` exactly once on the new proxy. +- `appImplementation` is a contract conforming to `DstackApp`'s storage + layout. Setting it to anything else is the owner's prerogative; the + spec does not constrain it beyond non-zero. + +### 5.3 App ↔ Proxy (upgrade authorization) + +`UUPSUpgradeable._authorizeUpgrade` is overridden in `DstackApp` to +`require(!_upgradesDisabled)` plus the inherited `onlyOwner`. Assumption: + +- The OZ Foundry Upgrades plugin's storage-layout check is the primary + defense against incompatible upgrades; the on-chain `_authorizeUpgrade` + hook is only the access gate. + +## 6. Adversarial scenarios + +### 6.1 Malicious `registerApp` + +An attacker calls `kms.registerApp(maliciousContract)` where `maliciousContract` +implements `IAppAuth` and returns `(true, "")` for every input. Can they +gain authorization? + +**No, conditional on owner integrity.** The downstream gates remain: + +1. `allowedOsImages[b.osImageHash]` must be true — owner-controlled. +2. The off-chain consumer of `isAppAllowed` is expected to verify that + `b.appId`'s deployed bytecode matches the legitimate `DstackApp` + implementation. The KMS does not (and arguably cannot) do this check + on-chain because the registered app could be a proxy pointing at the + correct impl. + +**Spec gap**: the on-chain contract does not enforce that the registered +app's bytecode matches `appImplementation`. The trust assumption is +external. Future hardening could require `b.appId.code` to equal a +known proxy template that delegates to `appImplementation`. + +### 6.2 Reentrancy via delegated `isAppAllowed` + +KMS's `isAppAllowed` is `view`. The EVM lifts the inner call to +`STATICCALL`, which propagates: no path through the registered contract +can mutate KMS state. Reentrancy is structurally impossible at the +KMS level. + +### 6.3 Gas-griefing + +The registered app's `isAppAllowed` can deliberately consume all gas. +KMS's outer call sees an out-of-gas revert. Mitigation: callers should +budget gas appropriately; do not infer "allowed" from a successful call +without observing the return value. + +### 6.4 Front-running `deployAndRegisterApp` + +Alice intends to deploy at address `X` (CREATE2-style or similar +prediction). Bob calls `registerApp(X)` first. Outcome: +`registeredApps[X] = true` either way; Alice's later deploy succeeds and +re-sets the bit. No privilege escalation. + +### 6.5 Selector collision between the two `initialize` overloads + +The 5-arg and 6-arg overloads have different selectors: + +- `initialize(address,bool,bool,bytes32,bytes32)` → `0x...` (selector A) +- `initialize(address,bool,bool,bool,bytes32,bytes32)` → `0x...` (selector B) + +These are distinct under standard 4-byte selector hashing. Selector +collisions across Ethereum's full selector space exist mathematically +but are not exploitable here. + +## 7. Known specification gaps + +For a future audit-firm engagement to close: + +1. **Cross-transaction invariants** — INV-1, INV-2, INV-3, INV-6 all need + true invariant verification (Certora or Halmos `--symbolic-storage`). +2. **`isKmsAllowed` short-circuit proofs** — mirror the `isAppAllowed` + shape but for `kmsAllowedAggregatedMrs` and `kmsAllowedDeviceIds`. +3. **Delegated-call universal quantification** — verify that for any + registered app contract, `kms.isAppAllowed` either reverts or returns + the registered contract's verbatim output. Requires modeling adversarial + external code. +4. **Storage layout verification against deployed bytecode** — see + `formal-verification.md` Phase 4. The `.openzeppelin/unknown-2035.json` + manifest diverges from current source on slots 5/8/9/10; the team + believes the manifest is stale. An audit firm would confirm by + reading the live proxies. +5. **Bytecode-level verification (KEVM)** — closes the compiler-as-attack- + surface gap. Phase 5 of the FV plan. +6. **Initializer single-run invariant** — INV-3 needs explicit verification + that the two `initialize` overloads cannot both succeed on the same + proxy. + +## 8. Open questions for the team + +These are spec-level decisions the dstack team should pin down before a +formal audit: + +1. **`renounceOwnership` semantics.** Both `DstackKms` and `DstackApp` + inherit `renounceOwnership` from `OwnableUpgradeable`. Renouncing + the KMS owner permanently freezes the OS-image whitelist and all + KMS mutations. Is that acceptable, or should `renounceOwnership` be + overridden to revert? +2. **App impl drift.** If `appImplementation` is updated after several + apps have been deployed via the factory, the older proxies stay on + the older impl. Is that intended (versioning) or should the KMS + track which impl was current at deploy time? +3. **Removing an OS image.** `removeOsImageHash` does not retroactively + un-authorize already-running apps that booted under that image. Is + that intended (revocation requires explicit downstream action) or + should the spec require it? +4. **`gatewayAppId` semantics.** The string is owner-set with no + validation. Should the spec require a particular format (address, + ENS, etc.)? diff --git a/kms/auth-eth/slither.config.json b/kms/auth-eth/slither.config.json new file mode 100644 index 00000000..66c7cb62 --- /dev/null +++ b/kms/auth-eth/slither.config.json @@ -0,0 +1,4 @@ +{ + "filter_paths": "lib/|node_modules/|test/|script/|out/|cache/|contracts/test-utils/", + "detectors_to_exclude": "naming-convention,solc-version" +} diff --git a/kms/auth-eth/test/DstackApp.symbolic.t.sol b/kms/auth-eth/test/DstackApp.symbolic.t.sol new file mode 100644 index 00000000..7b69d084 --- /dev/null +++ b/kms/auth-eth/test/DstackApp.symbolic.t.sol @@ -0,0 +1,290 @@ +/* + * SPDX-FileCopyrightText: © 2025 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/DstackApp.sol"; +import "../contracts/IAppAuth.sol"; + +/// @notice Halmos symbolic tests for DstackApp. +/// Run with `halmos --contract DstackAppSymbolicTest`. +/// Each `check_*` function has its arguments treated as symbolic; bodies +/// state the property as a Solidity-level assertion. +contract DstackAppSymbolicTest is Test { + DstackApp internal app; + address internal constant OWNER = address(0xA11CE); + address internal constant NON_OWNER = address(0xB0B); + + function setUp() public { + // Deploy proxy directly via ERC1967, bypassing the OZ Upgrades plugin + // (which uses FFI and is unsuitable for symbolic execution). + DstackApp impl = new DstackApp(); + bytes memory initData = abi.encodeWithSignature( + "initialize(address,bool,bool,bytes32,bytes32)", OWNER, false, false, bytes32(0), bytes32(0) + ); + ERC1967Proxy proxy = new ERC1967Proxy(address(impl), initData); + app = DstackApp(address(proxy)); + } + + // --------------------------------------------------------------- + // Owner-gated mutations: every state-changing method reverts when + // called by anyone other than the owner. + // --------------------------------------------------------------- + + function check_AddComposeHash_OnlyOwner(address caller, bytes32 hash) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.addComposeHash.selector, hash)); + assert(!ok); + } + + function check_RemoveComposeHash_OnlyOwner(address caller, bytes32 hash) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.removeComposeHash.selector, hash)); + assert(!ok); + } + + function check_AddDevice_OnlyOwner(address caller, bytes32 deviceId) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.addDevice.selector, deviceId)); + assert(!ok); + } + + function check_RemoveDevice_OnlyOwner(address caller, bytes32 deviceId) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.removeDevice.selector, deviceId)); + assert(!ok); + } + + function check_SetAllowAnyDevice_OnlyOwner(address caller, bool flag) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.setAllowAnyDevice.selector, flag)); + assert(!ok); + } + + function check_SetRequireTcbUpToDate_OnlyOwner(address caller, bool flag) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.setRequireTcbUpToDate.selector, flag)); + assert(!ok); + } + + function check_DisableUpgrades_OnlyOwner(address caller) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.disableUpgrades.selector)); + assert(!ok); + } + + // --------------------------------------------------------------- + // disableUpgrades monotonicity: after disableUpgrades() succeeds, + // every subsequent upgrade attempt — by any caller, to any impl — + // must revert. + // --------------------------------------------------------------- + + function check_DisableUpgradesMonotonic(address upgrader, address newImpl, bytes calldata data) external { + vm.prank(OWNER); + app.disableUpgrades(); + + vm.prank(upgrader); + (bool ok,) = address(app).call(abi.encodeWithSelector(app.upgradeToAndCall.selector, newImpl, data)); + assert(!ok); + } + + // --------------------------------------------------------------- + // isAppAllowed decision table. For any symbolic bootInfo and any + // setting of the three relevant flags + whitelists, the returned + // boolean matches the policy formula exactly. + // + // We deliberately set `tcbStatus = "UpToDate"` (concrete) here. + // The string-compare branch is exercised separately in the unit + // tests; making it fully symbolic interacts poorly with Halmos's + // bounded-byte modeling and inflates the search space without + // adding signal. + // --------------------------------------------------------------- + + function check_IsAppAllowed_DecisionTable_TcbUpToDate( + bytes32 composeHash, + bytes32 deviceId, + bool addCompose, + bool addDevice, + bool anyDevice + ) + external + { + vm.startPrank(OWNER); + if (addCompose) app.addComposeHash(composeHash); + if (addDevice) app.addDevice(deviceId); + app.setAllowAnyDevice(anyDevice); + vm.stopPrank(); + + IAppAuth.AppBootInfo memory bootInfo = IAppAuth.AppBootInfo({ + appId: address(app), + composeHash: composeHash, + instanceId: address(0), + deviceId: deviceId, + mrAggregated: bytes32(0), + mrSystem: bytes32(0), + osImageHash: bytes32(0), + tcbStatus: "UpToDate", + advisoryIds: new string[](0) + }); + + (bool allowed,) = app.isAppAllowed(bootInfo); + bool expected = addCompose && (anyDevice || addDevice); + assert(allowed == expected); + } + + // --------------------------------------------------------------- + // TCB byte-exact policy. When `requireTcbUpToDate` is on, the only + // accepted `tcbStatus` is the byte-exact ASCII string "UpToDate" + // (8 bytes). Any other string — case variations, trailing nulls, + // longer prefixes — is rejected. This is the contract dstack's + // off-chain attestation pipeline must honor. + // --------------------------------------------------------------- + + function check_TcbStatus_OnlyExactUpToDateAccepted(string memory tcbStatus) external { + bytes32 composeHash = bytes32(uint256(1)); + + vm.startPrank(OWNER); + app.addComposeHash(composeHash); + app.setAllowAnyDevice(true); + app.setRequireTcbUpToDate(true); + vm.stopPrank(); + + IAppAuth.AppBootInfo memory bootInfo = IAppAuth.AppBootInfo({ + appId: address(app), + composeHash: composeHash, + instanceId: address(0), + deviceId: bytes32(0), + mrAggregated: bytes32(0), + mrSystem: bytes32(0), + osImageHash: bytes32(0), + tcbStatus: tcbStatus, + advisoryIds: new string[](0) + }); + + (bool allowed,) = app.isAppAllowed(bootInfo); + bool exactMatch = keccak256(bytes(tcbStatus)) == keccak256(bytes("UpToDate")); + assert(allowed == exactMatch); + } + + // Concrete cases nail down the byte-exactness in case Halmos's + // symbolic-string modeling has surprises. + function check_TcbStatus_RejectsLowercase() external { + bytes32 composeHash = bytes32(uint256(1)); + vm.startPrank(OWNER); + app.addComposeHash(composeHash); + app.setAllowAnyDevice(true); + app.setRequireTcbUpToDate(true); + vm.stopPrank(); + + IAppAuth.AppBootInfo memory bootInfo = IAppAuth.AppBootInfo({ + appId: address(app), + composeHash: composeHash, + instanceId: address(0), + deviceId: bytes32(0), + mrAggregated: bytes32(0), + mrSystem: bytes32(0), + osImageHash: bytes32(0), + tcbStatus: "uptodate", + advisoryIds: new string[](0) + }); + (bool allowed,) = app.isAppAllowed(bootInfo); + assert(!allowed); + } + + function check_TcbStatus_RejectsTrailingChars() external { + bytes32 composeHash = bytes32(uint256(1)); + vm.startPrank(OWNER); + app.addComposeHash(composeHash); + app.setAllowAnyDevice(true); + app.setRequireTcbUpToDate(true); + vm.stopPrank(); + + IAppAuth.AppBootInfo memory bootInfo = IAppAuth.AppBootInfo({ + appId: address(app), + composeHash: composeHash, + instanceId: address(0), + deviceId: bytes32(0), + mrAggregated: bytes32(0), + mrSystem: bytes32(0), + osImageHash: bytes32(0), + tcbStatus: "UpToDate ", + advisoryIds: new string[](0) + }); + (bool allowed,) = app.isAppAllowed(bootInfo); + assert(!allowed); + } + + // --------------------------------------------------------------- + // 5-arg legacy initializer leaves the new TCB slot at zero, + // regardless of any of the other init inputs. + // --------------------------------------------------------------- + + function check_Initialize5Arg_DefaultsTcbToFalse( + address initialOwner, + bool disableUpgrades, + bool allowAnyDevice, + bytes32 deviceId, + bytes32 composeHash + ) + external + { + vm.assume(initialOwner != address(0)); + + DstackApp impl = new DstackApp(); + bytes memory initData = abi.encodeWithSignature( + "initialize(address,bool,bool,bytes32,bytes32)", + initialOwner, + disableUpgrades, + allowAnyDevice, + deviceId, + composeHash + ); + ERC1967Proxy proxy = new ERC1967Proxy(address(impl), initData); + DstackApp fresh = DstackApp(address(proxy)); + + assert(!fresh.requireTcbUpToDate()); + } + + // --------------------------------------------------------------- + // 6-arg initializer honors the TCB flag exactly. + // --------------------------------------------------------------- + + function check_Initialize6Arg_HonorsTcbFlag( + address initialOwner, + bool flag, + bool allowAnyDevice, + bytes32 deviceId, + bytes32 composeHash + ) + external + { + vm.assume(initialOwner != address(0)); + + DstackApp impl = new DstackApp(); + bytes memory initData = abi.encodeWithSignature( + "initialize(address,bool,bool,bool,bytes32,bytes32)", + initialOwner, + false, + flag, + allowAnyDevice, + deviceId, + composeHash + ); + ERC1967Proxy proxy = new ERC1967Proxy(address(impl), initData); + DstackApp fresh = DstackApp(address(proxy)); + + assert(fresh.requireTcbUpToDate() == flag); + } +} diff --git a/kms/auth-eth/test/DstackKms.symbolic.t.sol b/kms/auth-eth/test/DstackKms.symbolic.t.sol new file mode 100644 index 00000000..3bc517f6 --- /dev/null +++ b/kms/auth-eth/test/DstackKms.symbolic.t.sol @@ -0,0 +1,180 @@ +/* + * SPDX-FileCopyrightText: © 2025 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/DstackKms.sol"; +import "../contracts/DstackApp.sol"; +import "../contracts/IAppAuth.sol"; + +/// @notice Halmos symbolic tests for DstackKms. +/// Run with `halmos --contract DstackKmsSymbolicTest`. +contract DstackKmsSymbolicTest is Test { + DstackKms internal kms; + DstackApp internal appImpl; + address internal constant OWNER = address(0xA11CE); + + function setUp() public { + appImpl = new DstackApp(); + + DstackKms kmsImpl = new DstackKms(); + bytes memory initData = abi.encodeCall(DstackKms.initialize, (OWNER, address(appImpl))); + ERC1967Proxy proxy = new ERC1967Proxy(address(kmsImpl), initData); + kms = DstackKms(address(proxy)); + } + + // --------------------------------------------------------------- + // Owner-gated mutations across the KMS write surface. + // --------------------------------------------------------------- + + function check_SetGatewayAppId_OnlyOwner(address caller, string calldata id) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.setGatewayAppId.selector, id)); + assert(!ok); + } + + function check_AddKmsAggregatedMr_OnlyOwner(address caller, bytes32 mr) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.addKmsAggregatedMr.selector, mr)); + assert(!ok); + } + + function check_RemoveKmsAggregatedMr_OnlyOwner(address caller, bytes32 mr) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.removeKmsAggregatedMr.selector, mr)); + assert(!ok); + } + + function check_AddKmsDevice_OnlyOwner(address caller, bytes32 deviceId) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.addKmsDevice.selector, deviceId)); + assert(!ok); + } + + function check_RemoveKmsDevice_OnlyOwner(address caller, bytes32 deviceId) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.removeKmsDevice.selector, deviceId)); + assert(!ok); + } + + function check_AddOsImageHash_OnlyOwner(address caller, bytes32 imageHash) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.addOsImageHash.selector, imageHash)); + assert(!ok); + } + + function check_RemoveOsImageHash_OnlyOwner(address caller, bytes32 imageHash) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.removeOsImageHash.selector, imageHash)); + assert(!ok); + } + + function check_SetAppImplementation_OnlyOwner(address caller, address impl) external { + vm.assume(caller != OWNER); + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.setAppImplementation.selector, impl)); + assert(!ok); + } + + // NOTE: `registerApp` is intentionally `public` with no access control — + // it is the factory hook called by `deployAndRegisterApp` and is also + // open to direct external use. It is NOT an owner-only function. Halmos + // confirmed this: any non-zero address can be registered by anyone. + // Authorization is still gated downstream by the owner-controlled + // `allowedOsImages` whitelist and the registered app's own + // `isAppAllowed` logic. + function check_RegisterApp_AnyCallerCanRegisterNonZeroAddress(address caller, address appId) external { + vm.assume(appId != address(0)); + vm.prank(caller); + kms.registerApp(appId); + assert(kms.registeredApps(appId)); + } + + function check_RegisterApp_RejectsZeroAddress(address caller) external { + vm.prank(caller); + (bool ok,) = address(kms).call(abi.encodeWithSelector(kms.registerApp.selector, address(0))); + assert(!ok); + } + + // --------------------------------------------------------------- + // isAppAllowed short-circuits: unregistered app and unknown OS + // image must each force a reject regardless of any other input. + // --------------------------------------------------------------- + + function check_IsAppAllowed_RejectsUnregisteredApp(IAppAuth.AppBootInfo calldata bootInfo) external view { + // No apps registered in setUp(), so any bootInfo.appId is rejected. + (bool allowed, string memory reason) = kms.isAppAllowed(bootInfo); + assert(!allowed); + assert(keccak256(bytes(reason)) == keccak256(bytes("App not registered"))); + } + + function check_IsAppAllowed_RejectsUnknownOsImage(address appId, IAppAuth.AppBootInfo calldata bootInfo) external { + vm.assume(appId != address(0)); + + // Register the appId so the registration check passes. + vm.prank(OWNER); + kms.registerApp(appId); + + // No OS image is in the allowlist, so any bootInfo.osImageHash rejects. + vm.assume(bootInfo.appId == appId); + (bool allowed, string memory reason) = kms.isAppAllowed(bootInfo); + assert(!allowed); + assert(keccak256(bytes(reason)) == keccak256(bytes("OS image is not allowed"))); + } + + // --------------------------------------------------------------- + // deployAndRegisterApp atomicity + TCB propagation: when the + // factory call succeeds, the returned address is registered AND + // the proxy's `requireTcbUpToDate` reflects the supplied flag. + // --------------------------------------------------------------- + + function check_DeployAndRegisterApp_Atomic( + address initialOwner, + bool disableUpgrades, + bool requireTcbUpToDate, + bool allowAnyDevice + ) + external + { + vm.assume(initialOwner != address(0)); + + vm.prank(OWNER); + address appId = kms.deployAndRegisterApp( + initialOwner, disableUpgrades, requireTcbUpToDate, allowAnyDevice, bytes32(0), bytes32(0) + ); + + assert(kms.registeredApps(appId)); + assert(DstackApp(appId).requireTcbUpToDate() == requireTcbUpToDate); + assert(DstackApp(appId).allowAnyDevice() == allowAnyDevice); + assert(DstackApp(appId).owner() == initialOwner); + } + + // Legacy 5-arg overload always defaults `requireTcbUpToDate` to false. + function check_DeployAndRegisterApp5Arg_DefaultsTcbToFalse( + address initialOwner, + bool disableUpgrades, + bool allowAnyDevice + ) + external + { + vm.assume(initialOwner != address(0)); + + vm.prank(OWNER); + address appId = kms.deployAndRegisterApp(initialOwner, disableUpgrades, allowAnyDevice, bytes32(0), bytes32(0)); + + assert(kms.registeredApps(appId)); + assert(!DstackApp(appId).requireTcbUpToDate()); + } +}