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.
• 14 single-call Halmos properties in test/{DstackApp,DstackKms}.symbolic.t.sol. Each check_* proves a property a unit test or bounded fuzz couldn't. Highlights:
  • check_IsAppAllowed_DelegatesFaithfully (benign-shape registered contract) + check_IsAppAllowed_PropagatesMockRevert (reverting registered contract) — the two delegation paths the spec requires
  • check_IsAppAllowed_Rejects{UnregisteredApp,UnknownOsImage} and check_IsKmsAllowed_Rejects{UnknownMr,UnknownDevice} — fully symbolic AppBootInfo, gates short-circuit correctly
  • check_DeployAndRegisterApp_PostState and _DefaultsTcbToFalse — factory post-state holds for any input combination including the conditional initial-state branches
  • check_Initialize_OnceOnly — verifies INV-3 (proxy initialized exactly once); both overloads revert for any input after setUp
  • Single-call companions for disableUpgrades and the initializer-defaults
• 1 multi-call invariant in test/DstackAppInvariants.t.sol:
  • invariant_UpgradesDisabled_Monotonic — runs under halmos --invariant-depth 2, exhaustively explores all 2-call symbolic sequences across the contract's external surface from the disabled state. Verifies INV-1 (_upgradesDisabled monotonicity). Also passes at depth 3 (1024 paths, ~20s).
• docs/specification.md — normative pre/post/frame/events/reverts for the full public surface, state invariants with verification status (INV-1 and INV-3 verified, others gap), trust model, adversarial scenarios, four open product-level questions for the team.
• docs/formal-verification.md — the layered FV roadmap, the test inventory, and an explicit list of what we deliberately do not verify (with reasons).

What's intentionally out of scope (and why)

• Per-function _OnlyOwner tests — fuzz-tests in symbolic clothing against OZ's well-tested onlyOwner modifier
• Symbolic-string TCB byte-exactness — circular under Halmos's uninterpreted-keccak model
• Universal quantification over the registered IAppAuth contract — Halmos instantiates one mock at a time; we bound the relevant shapes (faithful return; revert propagation) and the spec is explicit about treating the registered contract's output as untrusted downstream
• Cross-transaction invariants INV-2 (owner-flow) and INV-6 (__gap zeroes) — gaps; would mirror the shape of the INV-1 invariant test

Open product-level questions

The specification ends with four decisions the team should pin down:

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?

Findings

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

How to verify

pipx install slither-analyzer halmos
cd kms/auth-eth
slither .                                                                  # 0 findings
halmos --contract DstackAppSymbolicTest                                    # 4 / 4
halmos --contract DstackKmsSymbolicTest                                    # 10 / 10
halmos --contract DstackAppInvariantsTest --invariant-depth 2              # 1 / 1
forge test --ffi                                                           # 47 / 47 (46 unit + 1 invariant)

🤖 Generated with Claude Code