feat(kms/auth-eth): formal verification — Slither + Halmos + spec#689
Open
h4x3rotab wants to merge 2 commits into
Open
feat(kms/auth-eth): formal verification — Slither + Halmos + spec#689h4x3rotab wants to merge 2 commits into
h4x3rotab wants to merge 2 commits into
Conversation
Layers a verification stack on top of the Hardhat→Foundry migration:
- Slither static analysis with project-tuned suppressions
(kms/auth-eth/slither.config.json): excludes naming-convention and
solc-version detectors that hit OZ-idiom noise across our codebase,
plus four per-line justified `// slither-disable-next-line` comments
in contracts/DstackKms.sol (factory reentrancy-benign on
deployAndRegisterApp's `new ERC1967Proxy`, named-return-forward
unused-return on the IAppAuth delegation, two unindexed-event-address
for backward compatibility with deployed log indexers). Baseline:
0 findings.
- Halmos symbolic execution: 28 properties across
test/{DstackApp,DstackKms}.symbolic.t.sol, each `check_*` function
treats its arguments as symbolic. Owner-only mutations, isAppAllowed
decision tables (including the byte-exact TCB compare), disableUpgrades
monotonicity, factory atomicity + TCB flag propagation, both 5- and
6-arg initializer overloads. All pass.
- docs/formal-verification.md is the layered roadmap (Slither → Halmos
→ optional Certora). SMTChecker (Layer 1) is deferred — forge's solc
binaries lack z3 linkage and BMC alone gives zero useful output on
OZ-upgradeable patterns. Halmos subsumes its coverage for our
contracts.
Both tools run locally (pipx install). Intentionally not in CI —
symbolic execution is slow, solver-version-sensitive, and most valuable
as an interactive design check rather than a PR gate.
Findings worth review:
- DstackKms.registerApp is permissionless by design (no access control,
only require !=0). Confirmed-intentional; the downstream
allowedOsImages whitelist + delegated isAppAllowed gate authorization.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Normative pre/post/frame conditions, state invariants, cross-contract assumptions, and adversarial scenarios for DstackKms + DstackApp, independent of code. Each property cites the Halmos test that verifies it; properties without a citation are explicit gaps. Sections: - Trust model (principals, environment, off-chain pipeline) - Storage layout per contract with frame-condition rules - Per-function pre/post/frame/events/reverts specs for the entire public surface - Decision-table semantics for isAppAllowed - State invariants INV-1 through INV-7 with verification status - Adversarial scenarios: malicious registerApp + downstream gates, reentrancy structural-impossibility argument, gas-griefing, front-running, initializer selector collision - Known verification gaps (cross-transaction invariants, universal-quantification over registered apps, KEVM bytecode-level) - Open product-level questions for the team: 1. Should renounceOwnership be overridden to revert? 2. Should KMS track which appImplementation was current per app? 3. Should removeOsImageHash retroactively un-authorize? 4. Should gatewayAppId validate format? Deliverable for any future external audit-firm engagement. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Layers a formal-verification stack on top of #252. Depends on #252 merging first — base is the
foundrybranch.What
slither.config.json+ four per-line// slither-disable-next-linejustifications inDstackKms.sol). Baseline: 0 findings.check_*properties acrosstest/DstackApp.symbolic.t.solandtest/DstackKms.symbolic.t.sol. Each function's arguments are symbolic; properties cover owner gates,isAppAlloweddecision tables, byte-exact TCB compare,disableUpgradesmonotonicity, factory atomicity, both 5- and 6-arg initializer overloads. All pass.docs/formal-verification.md— layered FV roadmap. SMTChecker (Layer 1) is deferred with rationale (forge's solc binaries lack z3 linkage).docs/specification.md— normative pre/post/frame conditions, state invariants, cross-contract assumptions, adversarial scenarios, open spec questions for the team.Both tools run locally (
pipx install slither-analyzer halmos). Intentionally not in CI — symbolic execution is slow, solver-version-sensitive, and most valuable as an interactive design check rather than a PR gate.Finding worth review
DstackKms.registerAppis permissionless by design (already confirmed-intentional). Halmos's firstcheck_RegisterApp_OnlyOwnertest failed and was rewritten to assert the actual permissive behavior. The downstreamallowedOsImageswhitelist + delegatedisAppAllowedgate authorization, so registration alone confers no privilege.Open product-level questions
The specification document ends with four decisions the team should pin down:
renounceOwnershipbe overridden to revert?appImplementationwas current per app at deploy time?removeOsImageHashretroactively un-authorize already-running apps?gatewayAppIdvalidate format?How to verify
🤖 Generated with Claude Code