feat(kms/auth-eth): formal verification — Slither + Halmos + spec

[h4x3rotab]

Layers static analysis + a focused symbolic-execution suite on top of #252. Depends on #252 merging first — base is the foundry branch.

What's verified

• Slither static analysis with project-tuned suppressions in slither.config.json. Baseline: 0 findings.
• 15 Halmos symbolic properties (5 in DstackApp.symbolic.t.sol, 10 in DstackKms.symbolic.t.sol). Each proves something a unit test or bounded fuzz couldn't. Highlights:
  • check_UpgradesDisabled_StepPreservation — INV-1 inductive step: from the disabled state, no single call to any enumerated mutating function (symbolic selector + args + caller, issued against the proxy) flips _upgradesDisabled back to false. Validated by mutation testing — a permissionless flag-reset and an owner-callable flag-reset are both caught.
  • check_IsAppAllowed_DelegatesFaithfully + check_IsAppAllowed_PropagatesMockRevert — the two delegation paths (faithful return; revert propagation) for a registered IAppAuth
  • check_IsAppAllowed_Rejects{UnregisteredApp,UnknownOsImage} + check_IsKmsAllowed_Rejects{UnknownMr,UnknownDevice} — fully symbolic AppBootInfo, gates short-circuit correctly
  • check_DeployAndRegisterApp_PostState / _DefaultsTcbToFalse — factory post-state including the conditional initial-state branches
  • check_Initialize_OnceOnly — INV-3 (proxy initialized exactly once)
• docs/specification.md — normative pre/post/frame/events/reverts, state invariants with honest verification status, trust model, adversarial scenarios, four open product questions.
• docs/formal-verification.md — roadmap, test inventory, and an explicit list of what we do not verify (with reasons).

Honesty notes (what this is NOT)

• INV-1 is not a complete cross-transaction proof. It has a verified inductive step (from the canonical disabled state) plus a source-inspection closure (the slot has exactly two writers; the initializer path is closed by check_Initialize_OnceOnly). Quantifying the step over arbitrary disabled pre-states needs symbolic storage, which Halmos 0.3.3 lacks — documented as a residual gap. An earlier invariant-mode attempt was discarded because it passed vacuously (the auto-target fuzzer drove the implementation while the assertion read the proxy); the current step-test reads and writes the same proxy storage and is mutation-tested.
• Per-function _OnlyOwner tests omitted — fuzz-tests in symbolic clothing against OZ's onlyOwner.
• TCB byte-exactness left to the spec (circular under Halmos's uninterpreted-keccak).
• Universal quantification over registered contracts, INV-2/INV-6, frame conditions — documented gaps.

Findings

DstackKms.registerApp is permissionless by design (confirmed, in natspec). The delegation tests prove an attacker who registers their own contract is still gated by the owner-controlled allowedOsImages whitelist, and that their contract's revert propagates rather than being silently mapped to a rejection.

Open product questions

1. Should renounceOwnership be overridden to revert?
2. Should KMS track which appImplementation was current per app at deploy time?
3. Should removeOsImageHash retroactively un-authorize already-running apps?
4. Should gatewayAppId validate format?

How to verify

pipx install slither-analyzer halmos
cd kms/auth-eth
slither .                                  # 0 findings
halmos --contract DstackAppSymbolicTest    # 5 / 5
halmos --contract DstackKmsSymbolicTest    # 10 / 10
forge test --ffi                           # 46 / 46

🤖 Generated with Claude Code