From e1ddeb29fed99d10bba32ec12d71fc561c7e2051 Mon Sep 17 00:00:00 2001 From: taek Date: Tue, 7 Jul 2026 13:30:17 +0900 Subject: [PATCH 1/2] docs: remove audit changelog and audit folder --- CHANGELOG_AUDIT.md | 173 ------ audit/FV_COVERAGE.md | 220 -------- audit/FV_PLAN.md | 106 ---- audit/FV_PLAN_ROUND_2.md | 157 ------ audit/fv-gap-audit.md | 117 ---- audit/fv-round-1-findings.md | 415 -------------- .../property-15-erc1271-nested-eip712.md | 532 ------------------ 7 files changed, 1720 deletions(-) delete mode 100644 CHANGELOG_AUDIT.md delete mode 100644 audit/FV_COVERAGE.md delete mode 100644 audit/FV_PLAN.md delete mode 100644 audit/FV_PLAN_ROUND_2.md delete mode 100644 audit/fv-gap-audit.md delete mode 100644 audit/fv-round-1-findings.md delete mode 100644 audit/manual-proofs/property-15-erc1271-nested-eip712.md diff --git a/CHANGELOG_AUDIT.md b/CHANGELOG_AUDIT.md deleted file mode 100644 index fc320fc1..00000000 --- a/CHANGELOG_AUDIT.md +++ /dev/null @@ -1,173 +0,0 @@ -# Kernel v4 Audit Changelog - -**Commit Range:** `ff20f6c` to `3e72921` (HEAD) -**Date Range:** October 14, 2025 - November 6, 2025 -**Files Changed:** 21 files in `src/` (+625, -500 lines) - ---- - -## Added Features - -### EntryPoint v0.9 Support -Added support for ERC-4337 EntryPoint version 0.9. -- Updated account-abstraction dependency from v0.8.0 to v0.9.0 (branch: release-v09) -- Updated EntryPoint deployment bytecode constant in test utilities -- Modified test suite to include `vm.startPrank(beneficiary, beneficiary)` calls before `ep.handleOps()` for v0.9 compatibility -- Updated remappings to support both v0.8.0 and v0.9.0 dependencies -- Gas snapshot updates reflecting v0.9 optimizations (reduced gas costs across all test scenarios) -- **Breaking Change:** UserOperation hash calculation has been changed in EntryPoint v0.9 -- **Files:** `foundry.toml`, `remappings.txt`, `soldeer.lock`, `test/utils/EntryPointLib.sol`, `test/KernelUserOpTest.sol`, `test/KernelValidatorTest.sol` -- **EntryPoint Address:** `0x43370900c8de573dB349BEd8DD53b4Ebd3Cce709` -- **Commits:** 977ca07, aa91ef1, 110c7af, 3e72921 -- **Note:** The module type ID was updated from 8 to 10 for `MODULE_TYPE_STATELESS_VALIDATOR_WITH_SENDER` as part of this upgrade -- you can find the release docs in [here](https://docs.google.com/document/d/1RKkKZsP1eYkOoBEkzJ1vWRK_bcWXaewoGPzawMjsleM/edit?usp=drivesdk), please do note that this document is not in public yet - -### Staker Contract (`src/Staker.sol`) - NEW -Factory staking management contract for ERC-4337 EntryPoint compliance. -- Factory approval whitelist (owner-controlled or EIP-712 signature-based) -- EntryPoint stake/unstake/withdraw functions -- `deployWithFactory()` - Deploy accounts through approved factories -- `approveFactory()` - Owner approves/disapproves factory -- `approveFactoryWithSignature()` - EIP-712 signature-based approval (chain-agnostic) -- **Commits:** e4431db, 52265ac -- **PR:** #20 - -### Enable Mode Signature Support -Added support for installing modules via signature in UserOp flow (enable mode). -- Allows users to install validators/modules atomically with their first UserOp -- Uses `EnableModeSignature` struct containing: nonce, packages to install, enable signature, and userOp signature -- EIP-712 signature verification with nonce replay protection -- Nonce is checked and incremented to prevent replay attacks -- **Files:** `src/Kernel.sol` (validateUserOp), `src/core/ModuleManager.sol` -- **Commits:** 7a578c2 -- **PR:** #25 - -### Root Validator Replacement -New `setRoot()` overload allows replacing root validator with automatic cleanup of previous root. -- **Function:** `setRoot(Install[] calldata pkg, bool removeCurrent, bytes calldata uninstallData)` -- Supports uninstalling validators and permissions (including policies and signers) -- Calls `onUninstall()` on removed modules -- **Commits:** a691aad, f646dec, ffe4d58 -- **PR:** #7 - -### Validator/Permission Management Functions -New internal functions for module lifecycle management: -- `_uninstallValidator()` - Uninstall validator with ValidationInfo cleanup -- `_uninstallPolicyWithVid()` - Remove policy from specific permission -- `_uninstallSignerWithVid()` - Remove signer from specific permission -- **Files:** `src/core/ModuleManager.sol`, `src/core/ValidationManager.sol` -- **Commits:** a691aad - -### ValidationId Utility Functions -Helper functions for ValidationId type extraction and creation in `lib/Utils.sol`: -- `parseNonce()` - Extract validation mode, type, and ID from nonce (moved from ValidationManager) -- `getType()` - Extract validation type from ValidationId -- `getValidator()` - Extract validator address from ValidationId -- `validatorToIdentifier()` - Create ValidationId from validator address -- `permissionToIdentifier()` - Create ValidationId from PermissionId -- `isPermissionType()` - Check if validation type is permission variant -- `calldataKeccak()` - Efficient calldata hashing for EIP-712 -- **Commits:** 5ee7a26, b6e1ee4, f67e36c, 6e3a5f5 -- **PR:** #19 - -### ERC-1271 Raw Hash Signing -Support for raw hash signing in EIP-7702 accounts (without EIP-712 wrapping). -- **Hook:** `_erc1271RawAllowed()` - Override to enable raw signing -- Enabled by default in `Kernel7702` contract -- **Files:** `src/Kernel7702.sol`, `src/lib/ERC1271.sol` -- **Commits:** 40b0ff6, 83d6e32, 776fe04, 8999222 -- **PR:** #24 - ---- - -## Changed Features - -### ValidationId Encoding (BREAKING CHANGE) -ValidationId changed from 20 bytes to 21 bytes to embed validation type in first byte. -- **Before:** `bytes20` (address only) -- **After:** `bytes21` (1 byte type + 20 bytes address/permissionId) -- **Encoding:** Byte 0 = ValidationType (ROOT=0, VALIDATOR=1, PERMISSION=2), Bytes 1-21 = address/permissionId -- **Impact:** Type checking no longer requires storage reads, eliminates `vType` field from ValidationInfo struct -- **Migration:** Use `validatorToIdentifier()` and `permissionToIdentifier()` utility functions -- **Storage Optimization:** Removed `vType` field from ValidationInfo struct -- **Commits:** 5ee7a26, b6e1ee4, f67e36c, 6e3a5f5 -- **PR:** #19 - -### Initialization Pattern Refactor -- `Kernel.initialize()` is now `virtual` and `payable` - implementation moved to derived contracts -- `KernelUUPS.initialize()` has `initializer` modifier and properly initializes in constructor -- `KernelUUPS` constructor calls `_disableInitializers()` to prevent implementation initialization -- `Kernel7702.initialize()` is NO-OP (stateless accounts don't need initialization) -- `KernelImmutableECDSA._initialize()` removed `initializer` modifier (protection at UUPS level) -- **Files:** `src/Kernel.sol`, `src/KernelUUPS.sol`, `src/Kernel7702.sol`, `src/KernelImmutableECDSA.sol` -- **Commits:** 75e788b, 69e12fb, 041bb87, a8cec2c -- **PR:** #17 - -### Factory Deployment Protection -Factory now checks if account is already deployed before calling initialize. -- Prevents re-initialization of already deployed accounts -- **Files:** `src/KernelFactory.sol` -- **Functions:** `deployImmutableECDSA()`, `deployImmutableECDSAWithExtraCall()` -- **Commits:** 75e788b -- **PR:** #17 - -### Factory Salt Calculation Optimization -Optimized to use `EfficientHashLib` instead of `keccak256(abi.encode())`. -- **File:** `src/KernelFactory.sol` -- **Function:** `_calculateSalt()` - NEW internal function using EfficientHashLib -- **Commits:** e4431db - -### Executor Authorization Check -Added installation verification in `executeFromExecutor()` flow via `executorHook` modifier. -- **Change:** Added `require(address(hook) != address(0), Unauthorized())` in `executorHook` modifier -- Prevents uninstalled executors from executing transactions -- **File:** `src/core/ModuleManager.sol` -- **Commits:** 7f55374, eff6542, dcec72e -- **PR:** #18 - -### Module Type Validation -`supportsModule()` now returns false for moduleTypeId == 0 (invalid/undefined type). -- **File:** `src/Kernel.sol` -- **Commits:** 73a61ed -- **PR:** #13 - -### Enable Mode Nonce Replay Protection -Added nonce check and increment in `validateUserOp()` enable mode flow. -- **Change:** Added `_checkAndIncrementNonce(sig.nonce)` after signature verification -- Prevents signature replay attacks -- **File:** `src/Kernel.sol` -- **Commits:** 7a578c2 -- **PR:** #25 - -### Hook Validation Logic Enhancement -Optimized hook validation check in UserOp flow. -- **Change:** Reordered conditional logic for gas optimization (root or hookless paths first) -- **File:** `src/Kernel.sol` -- **Commits:** fa6a1bd, cdf738b -- **PR:** #22 - -### Signature Verification Optimization -Use `ECDSA.tryRecoverCalldata()` instead of `ECDSA.tryRecover()` when signature is in calldata. -- **Files:** `src/KernelImmutableECDSA.sol`, `src/Kernel7702.sol` -- **Impact:** Gas savings for signature verification - -### Access Control Modifier Optimization -Changed `_onlyEntryPointOrSelf()` and `_authorizeUpgrade()` to `view` functions. -- Prevents accidental state changes in authorization checks -- **Files:** `src/Kernel.sol`, `src/KernelUUPS.sol` - ---- - -## Removed Features - -### KernelHelper.sol - DELETED -EIP-712 digest generation moved inline to `ModuleManager.sol`. -- Reduces external dependencies -- Functions moved: `installDigest()`, `_installHash()`, `_hashTypedData()`, `_hashTypedDataSansChainId()` -- Now implemented as internal functions in ModuleManager - -### Removed Functions -- `ExecutorManager.installAndExecute()` - Removed unused and potentially dangerous function -- `KernelImmutableECDSA._statelessInitializeCheck()` - Removed unused hook -- `KernelImmutableECDSA` EthSign prefix handling - Simplified to use only standard ECDSA recovery -- **Commits:** 35f65fe diff --git a/audit/FV_COVERAGE.md b/audit/FV_COVERAGE.md deleted file mode 100644 index e9a4aa55..00000000 --- a/audit/FV_COVERAGE.md +++ /dev/null @@ -1,220 +0,0 @@ -# Kernel v4 — FV Coverage Board - -> **Live status table** mapping every public/external function plus security-relevant internal helper to its formal-verification obligation, backend, and proof state. - -**Last updated**: 2026-05-25 (Round 2 remaining-gaps closure — Phase 3 composition proven) -**Branch**: `audit/fv-round-1` (PR #55, 48 commits) -**Companion docs**: -- [`audit/FV_PLAN.md`](./FV_PLAN.md) — Round 1 multi-phase plan -- [`audit/FV_PLAN_ROUND_2.md`](./FV_PLAN_ROUND_2.md) — Round 2 strategy -- [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — original gap audit -- [`audit/fv-round-1-findings.md`](./fv-round-1-findings.md) — Round 1 per-property findings - -## Legend - -**Obligation types** (per the Round 2 plan): - -- **AC** — Access Control: caller restrictions hold -- **TR** — Transition: every state change preserves the relevant invariant -- **EQ** — Equivalence: two paths agree on the audit-relevant outcome -- **NR** — Non-Replay: operations cannot be replayed -- **NB** — Non-Bypass: no path returns success without the expected predicate -- **DT** — Determinism: pure functions / CREATE2 deployments are deterministic -- **OF** — Overflow: arithmetic cannot overflow under reachable preconditions - -**Status**: - -- ✅ **PROVEN** — at least one FV backend has discharged the obligation -- 🟡 **PARTIAL** — partially proven (e.g., subset of inputs, complementary backends) -- ❌ **OPEN** — obligation identified but not yet attempted -- 🔵 **OOS** — explicitly out of scope (with rationale) - -**Backends**: - -- **H** = Halmos, **C** = Certora, **K** = Kontrol, **M** = Manual proof, **OOS** = out of scope - ---- - -## `src/Kernel.sol` - -| Visibility | Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---|---| -| external | `initialize(packages)` (declared abstract) | AC, TR | — | 🔵 OOS | Implemented by subclasses (`KernelUUPS.initialize`, `KernelImmutableECDSA._initialize`). | -| external | `validateUserOp(userOp, hash, missingFunds)` | AC, NB | C | ✅ PROVEN | Phase C #1 strict + naive rules. Spec: `certora/specs/Kernel.spec`. | -| external | `executeUserOp(userOp, hash)` | NB | C, M | ✅ PROVEN | Phase C #1 (executeUserOp inner delegatecall gated by validateUserOp). | -| external | `execute(mode, executionData)` | AC | H | ✅ PROVEN | Top-level AC proven via `test/halmos/TopLevelExecuteAcHalmos.t.sol` (entryPoint or self only). Inner calls proven by Phase 2. | -| external | `setNonce(key, seq)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `setRootPreservesNonBypass` + `_checkAndIncrementNonce` chain. Phase A #13 covers nonce no-overflow. | -| external | `setValidNonceFrom(seq)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Same. | -| external | `installModule(moduleType, module, initData)` (ERC-7579) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `_initializeValidation` + `_installValidator/Policy/Signer/Hook/Executor/Selector` writer chain. | -| external | `uninstallModule(moduleType, module, initData)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `uninstallValidationPreservesNonBypass`. | -| external | `setRoot(pkg, removeCurrent, uninstallData)` (install-overload) | AC, TR, NB | C | ✅ PROVEN | Phase D #6 (`SetRootLifo.spec`). LIFO cleanup post-conditions verified. | -| external | `setRoot(vId)` (id-overload) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | `setRootPreservesNonBypass`. | -| external | `grantAccess(vId, selectors)` | AC, TR, NB | C (Phase C writer-local) | ✅ PROVEN | `grantAccessPreservesNonBypass`. Block executeUserOp.selector for non-root in fix `0921b25`. | -| external | `installModule(packages)` (enable-mode) | AC, NR | C, H | ✅ PROVEN | Phase D #4 covers permission totality. Phase 2 `_verifyInstallSignatureRaw` proven via `test/halmos/VerifyInstallSignatureHalmos.t.sol` (signature gate + replay protection). | -| external view | `supportsExecutionMode(mode)` | — | H (Round 1 baseline) | ✅ PROVEN | Existing `KernelExecutionModeHalmos.t.sol` on `fix/audit-internal-batch-1`. | -| external pure | `supportsModule(typeId)` | — | H (Round 1 baseline) | ✅ PROVEN | Same. | -| external pure | `accountId()` | — | — | 🔵 OOS | String constant; no security obligation. | -| internal | `_onlyEntryPointOrSelf()` | AC | H | ✅ PROVEN | Phase A #3 (`KernelAccessControlHalmos.t.sol` on baseline). | -| internal | `_initialize(packages)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Through `_initializeValidation` + `_setRoot` writers. | -| internal | `_processUserOp(userOp, hash)` | NB | C | ✅ PROVEN | Phase C #1 (this is where the fast-path bug lived; fix verified). | -| internal | `_executeFromExecutor(mode, data)` | AC | C (transitively) | 🟡 PARTIAL | AC through executor module path; direct proof missing. | -| internal | `_fallback()` | AC, NB | C (transitively) | 🟡 PARTIAL | Falls back to ERC-1271 verification; Phase E #15 covers nested EIP-712. | - -## `src/core/ValidationManager.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `_initializeValidation(vId, internalData)` | TR (nonce bump), NB (no stale grants) | H + C | ✅ PROVEN | Phase A #14 (nonce bump on both paths); Phase C writer-local. | -| `_installValidator(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. | -| `_installPolicy(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_checkPermissionInstall`. | -| `_installSigner(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. | -| `_uninstallValidation(_vId)` | TR | C (Phase C writer-local) | ✅ PROVEN | `uninstallValidationPreservesNonBypass`. | -| `_uninstallValidator(...)` | TR | C (Phase C writer-local) | ✅ PROVEN | Via `_uninstallValidation`. | -| `_uninstallPolicyWithVid(_policy, vId)` | TR (LIFO order) | C | ✅ PROVEN | Phase D #6 `setRootClearsOldPermissionState`. | -| `_uninstallSignerWithVid(_signer, vId)` | TR (policies.length == 0 precondition) | C | ✅ PROVEN | Phase D #6 (after policies fully popped). | -| `_grantAccess(vId, selectors)` | AC (executeUserOp filter), TR | C (Phase C writer-local) | ✅ PROVEN | `grantAccessPreservesNonBypass` + commit `0921b25` fix. | -| `_setRoot(vId)` (id-overload) | TR (nonce bump on rotation) | C (Phase C writer-local) + commit `ce185f6` fix | ✅ PROVEN | `setRootPreservesNonBypass`. | -| `_setRoot(pkg)` (install-overload) | TR, NB | C | ✅ PROVEN | Phase D #6. | -| `_validateUserOpValidator(vId, hash, op, sig)` | NB | H | ✅ PROVEN | Phase A #5 (regression witness for moduleType filter) + Phase A #9 (fallback ECDSA). | -| `_validateUserOpPermission(vId, hash, op, sig)` | NB | C | ✅ PROVEN | Phase D #4 (policy/signer failure ⇒ aggregate failure). | -| `_validateUserOpFallback(vId, hash, op, sig)` | NB | H | ✅ PROVEN | Phase A #9. | -| `_verifySignaturePermission(vId, vInfo, requester, hash, sig)` | EQ (vs write path) | C | ✅ PROVEN | Phase D #11 (view/write paths agree on success/failure). | -| `_verifyInstallSignature(replayable, nonce, packages, sig)` | NR | H + C | ✅ PROVEN | Phase 2: `_verifyInstallSignatureRaw` signature gate + replay protection proven via Halmos. | -| `_verifyInstallSignatureRaw(...)` | NB | H | ✅ PROVEN | Phase 2 (`VerifyInstallSignatureHalmos.t.sol`): rejects bad signatures, accepts good ones, replay-protected. | -| `_checkValidation(vType, vId)` | TR (routing) | C | ✅ PROVEN | Phase 2 (`CheckValidation.spec`): all 12 rules + 3 sanity PASS. Includes HIGH-severity Rule 6 (fallback routed only when root==0). | -| `_initializeValidation` empty-data path nonce bump | TR | H | ✅ PROVEN | Phase A #14 regression witness for commit `9f9471c`. | - -## `src/core/ModuleManager.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `_checkNonce(nonce)` view | EQ (vs write path) | H | ✅ PROVEN | Phase B #7 (`NonceConsistencyHalmos.t.sol`) — below saturation. | -| `_checkAndIncrementNonce(nonce)` | TR, OF | H | ✅ PROVEN | Phase A #13 (no overflow); Phase B #7 (view/write agreement). | -| `_grantAccess(vId, selectors)` | AC (executeUserOp filter) | C (Phase C writer-local) | ✅ PROVEN | Same as ValidationManager line. | -| `_verifyInstallSignatureRaw(...)` | NB | H | ✅ PROVEN | Same as ValidationManager line — Phase 2 (`test/halmos/VerifyInstallSignatureHalmos.t.sol`): rejects bad signatures, accepts good ones, replay-protected. | -| `_installHash(packages)` | DT | H | ✅ PROVEN | Phase 2 (`InstallHashHalmos.t.sol`): determinism + field-sensitivity across moduleType / module / moduleData / internalData. | -| `_erc1271IsValidSignatureNowCalldata(hash, sig)` | NB | M + H + C | ✅ PROVEN | Manual CFG proof (`audit/manual-proofs/property-15-erc1271-nested-eip712.md`) covers Path P and Path T. Production binding by Phase A #9. | - -## `src/core/ExecutionManager.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `_execute(mode, executionData)` | AC (caller is Kernel itself) | H | ✅ PROVEN | AC top-level proven via `test/halmos/TopLevelExecuteAcHalmos.t.sol` (`Kernel.execute` reverts unless caller is entryPoint or self). | -| `_executeCall(executionData, onRevert)` | NB | H | ✅ PROVEN | Phase 2 (`ExecuteCallHalmos.t.sol`): return shape preserved across size classes 0/32/64/256; throw vs silent revert handling. | -| `_executeDelegateCall(executionData, onRevert)` | NB | H | ✅ PROVEN | Same. | -| `_executeBatchCall(executionData, onRevert)` | NB | H (Round 1 baseline) | 🟡 PARTIAL | Existing `KernelBatchExecutionHalmos.t.sol` on baseline covers single/batch × default/try; needs verification on this branch. | -| `_getReturn()` | — | — | 🔵 OOS | Pure assembly memory return; no security obligation. | -| `_call(target, value, callData)` | — | — | 🔵 OOS | Solidity primitive wrapper. | -| `_delegateCall(delegate, callData)` | — | — | 🔵 OOS | Solidity primitive wrapper. | - -## `src/core/ExecutorManager.sol` / `HookManager.sol` / `SelectorManager.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `executorConfig(executor)` view | — | — | 🔵 OOS | Pure getter. | -| `_installExecutor(...)` | TR | C | ✅ PROVEN | Phase 2 (`ModuleWriters.spec`): `installExecutorPostHookOk`. | -| `_uninstallExecutor(...)` | TR | C | ✅ PROVEN | `uninstallExecutorClearsHook`. | -| `_installHook(...)` | TR | C | ✅ PROVEN | `installHookPostEnabled`. | -| `_uninstallHook(...)` | TR | C | ✅ PROVEN | `uninstallHookPostDisabled`. | -| `_preHook(hook, data)` | TR | H (Round 1 baseline) | 🟡 PARTIAL | `KernelHookBracketingHalmos.t.sol` on baseline. | -| `_postHook(hook, context)` | TR | H (Round 1 baseline) | 🟡 PARTIAL | Same. | -| `_hookEnabled(hook)` view | — | — | 🔵 OOS | Pure view. | -| `_installSelector(...)` | TR | C + H (baseline) | ✅ PROVEN | Phase 2 (`ModuleWriters.spec`): `installSelectorPostInvariant` proves the hook-state envelope (NOT_INSTALLED entryPoint-only sentinel, NO_HOOK, or enabled hook). Writer also enforces `require(_module != 0, InvalidSelectorTarget())` since commit `7b38cad` (Gap 2 hardening); regression test in `test/unit/ModuleManagerCoverage.t.sol::test_installFallback_WhenModuleIsZeroAddress_ShouldRevertWithInvalidSelectorTarget`. | -| `_uninstallSelector(...)` | TR | C | ✅ PROVEN | `uninstallSelectorClearsTarget`. | - -## `src/KernelUUPS.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `initialize(packages)` | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Via `_initializeValidation`. | -| `upgradeToAndCall(impl, data)` | AC | H | ✅ PROVEN | Phase A #3 (`KernelUUPSHalmos.t.sol`). | -| `_authorizeUpgrade(impl)` | AC | H | ✅ PROVEN | Same. | -| `proxiableUUID()` pure | — | — | 🔵 OOS | EIP-1822 constant. | - -## `src/Kernel7702.sol` / `src/KernelImmutableECDSA.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `_verifyFallbackSignature(hash, sig)` | NB (iff ECDSA recovery) | H | ✅ PROVEN | Phase A #9 (`FallbackSignatureHalmos.t.sol`). Both variants. | -| `_fallbackValidatorAvailable()` pure | — | — | 🔵 OOS | Constant. | -| `_erc1271RawAllowed()` pure | — | — | 🔵 OOS | Constant. | -| `_initialize(packages)` (KernelImmutableECDSA) | AC, TR | C (Phase C writer-local) | ✅ PROVEN | Via base. | - -## `src/KernelFactory.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `deploy(initialPackages, nonce)` | DT, NR (no double-init) | H | ✅ PROVEN | Phase A #12. | -| `deployECDSA(signer, initialPackages, nonce)` | DT, NR | H | ✅ PROVEN | Same. | -| `getAddress(initialPackages, nonce)` view | DT | H | ✅ PROVEN | Same. | -| `getECDSAAddress(signer, initialPackages, nonce)` view | DT | H | ✅ PROVEN | Same. | -| ~~`_initialize(...)`~~ | — | — | 🔵 OOS | `KernelFactory` does not define a `_initialize` (verified by grep over `src/KernelFactory.sol`). Initialization happens inside the deployed `Kernel` proxy via `KernelUUPS.initialize` / `KernelImmutableECDSA._initialize`, both covered by Phase C writer-local and Phase 2 `_verifyInstallSignatureRaw`. Row retained as historical clarification. | - -## `src/Staker.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `deployWithFactory(factory, createData)` | — | — | 🔵 OOS | Factory call wrapper. | -| `approveFactory(factory, approval)` | AC | H | ✅ PROVEN | Phase 2 (`StakerOnlyOwnerHalmos.t.sol`): `onlyOwner` gate proven. | -| `approveFactoryWithSignature(factory, approval, sig)` | NR, chain-agnostic | H | ✅ PROVEN | Phase A #10. | -| `stake(entryPoint, unstakeDelay)` | AC | H | ✅ PROVEN | Phase 2 (`StakerOnlyOwnerHalmos.t.sol`). | -| `unlockStake(entryPoint)` | AC | H | ✅ PROVEN | Same. | -| `withdrawStake(entryPoint, recipient)` | AC | H | ✅ PROVEN | Same. | - -## `src/lib/ERC1271.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `isValidSignature(hash, sig)` public view | NB | H + M | ✅ PROVEN | Manual CFG + Phase E Halmos PersonalSign. | -| `_erc1271IsValidSignatureViaNestedEIP712(hash, sig)` | NB | M + H + K | ✅ PROVEN | Manual CFG proof closes TypedDataSign; Halmos closes PersonalSign; Kontrol partial (no CEX). | -| `_erc1271IsValidSignatureViaNestedEIP712Replayable(hash, sig)` | NB | M + H | ✅ PROVEN | Same. | -| `_erc1271Raw(hash, sig)` | NB | — | 🟡 PARTIAL | Falls back to `_erc1271IsValidSignatureNowCalldata`, which is covered. | - -## `src/lib/Lib4337.sol` - -| Function | Obligations | Backend | Status | Evidence | -|---|---|---|---|---| -| `intersectValidationData(a, b)` | TR (aggregator preservation) | H | ✅ PROVEN | Phase A #2 (`Lib4337Halmos.t.sol`, 8/8 PASS). | -| `chainAgnosticUserOpHash(sender, op)` | DT | H | ✅ PROVEN | Phase 2 follow-up (`test/halmos/ChainAgnosticHashHalmos.t.sol`): determinism + chain-id independence + field-sensitivity on sender / nonce / callData / accountGasLimits. | -| `parseNonce(nonce)` | DT | H | ✅ PROVEN | Phase A #8 (`ParseNonceHalmos.t.sol`). | - ---- - -## Summary - -| Layer | Count | Status | -|---|---|---| -| Public/external functions | 22 | 18 proven, 2 partial, 2 OOS | -| Security-relevant internal helpers | ~30 | 26 proven, 2 partial, 2 open | -| Total obligations identified | ~60 | ~50 proven, ~5 partial, ~5 open | - -**Coverage score (proof-obligation form)**: ~83% proven outright, ~8% partial, ~9% open or out-of-scope. - -**Round 2 Phase 2 closure delta (6 dispatches landed 2026-05-24)**: -- `_verifyInstallSignatureRaw` ❌→✅ -- `_executeCall` + `_executeDelegateCall` ❌→✅ -- `_checkValidation` ❌→✅ (HIGH-severity Rule 6 fallback-only-when-root-zero proven) -- `_installHash` ❌→✅ -- `Staker` AC quartet ❌→✅ -- `_installExecutor/Selector/Hook` + `_uninstallExecutor/Selector/Hook` ❌→✅ - -## Remaining open obligations - -**All Round 2 phases closed.** The remaining items are either documented limitations or properties scoped to a future round: - -1. **Phase D #4 `allSuccessImpliesAggregateSuccess` liveness retry** — when Certora's CVL `rule_sanity` bitvec-conversion gotcha is addressed in a future release. Liveness, not security. -2. **`nonRootCannotBypassFastPathWithExecuteUserOp` global invariant** — known unprovable under current CVL summaries (delegatecall havoc). Already documented in `certora/specs/Kernel.spec`. Writer-local decomposition (`certora/specs/PhaseCWriterLocal.spec`) proves the equivalent claim. -3. **`validateThenExecuteRequiresInnerSelectorAccess` post-execute variant** — dropped from `certora/specs/SystemComposition.spec` as a spec-framing issue (inner delegatecall writes invalidate the post-state observation). The `_preExecute` variant is the canonical compositional rule and PASSES. - -## Closed in Round 2 remaining-gaps pass (2026-05-25) - -- ✅ Gap 1: top-level `execute` + `executeFromExecutor` AC (Halmos, 5/5 PASS) -- ✅ Gap 2: `_installSelector` hardened with `require(_module != 0)` + regression test -- ✅ Gap 3: `validateUserOp → executeUserOp` compositional rule (Certora, `_preExecute` form, PASS) - -## How to maintain this board - -- Update after every Round N FV dispatch (success or refusal). -- Move rows between Status columns as backends close gaps. -- Add a new row whenever a PR introduces a new public/external function or a security-relevant internal helper. -- Cite the test file path or Certora job URL in the Evidence column — never leave it as "trust me". diff --git a/audit/FV_PLAN.md b/audit/FV_PLAN.md deleted file mode 100644 index faa8b5cd..00000000 --- a/audit/FV_PLAN.md +++ /dev/null @@ -1,106 +0,0 @@ -# Kernel v4 — Formal Verification Round 1 Plan - -> **Branch**: `audit/fv-round-1` (off `master` @ `a836274`) -> **Base plan**: [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — orchestrator's gap audit & dispatch decisions -> **Status as of 2026-05-20**: Phase A dispatched in parallel; B–E queued. - -## Baseline note (important for subagents) - -The orchestrator surveyed `fix/audit-internal-batch-1` which has 14 Halmos files. **This branch (master) has only `test/halmos/KernelExecutorHalmos.t.sol`.** Subagents should: - -1. Treat the existing file as the file-naming + import convention (`SymTest`, `Test`, `MockCallee`, etc.). -2. Create new Halmos files alongside it; do not assume sibling files exist. -3. Mocks live in `test/mock/*.sol` and EntryPoint helper in `test/utils/EntryPointLib.sol`. -4. **No `halmos.toml` exists yet** — `/setup-halmos` skill can be invoked if a subagent wants one, but the existing file works without it. - -### Project-specific Halmos quirks (encoded from project memory) - -- Halmos v0.3.3. Prefix is `check…` / `invariant…` (no underscore in existing file). Match it. -- Run `forge clean` before `halmos` — artifacts may lack AST otherwise. -- `vm.expectRevert(bytes4)` is unsupported. Use `try { …; assert(false); } catch {}` or `(bool ok,) = …; assertFalse(ok);`. -- Moving `new Contract()` inside `vm.expectRevert` scope captures the constructor, not the call. - -## Goals - -- Land **10 new Halmos proofs** covering the highest-severity un-touched areas on `master`. -- Land **4 Certora proofs** for multi-step + unbounded-data claims that Halmos can't reach. -- Land **1 Kontrol proof** (or accept a Halmos partial) for heavy-assembly ERC-1271 nested EIP-712. -- Do **not** introduce Tama or Clear in this round (post-release v4 cost-benefit doesn't justify). - -## Phase A — Halmos S-effort properties (in flight, parallel) - -| # | Property | File to create | Owner subagent | Status | -| -- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------- | ------------------------------- | ---------- | -| 2 | `Lib4337.intersectValidationData` preserves aggregator authority across all six precedence rules. | `test/halmos/Lib4337Halmos.t.sol` | sc-fv-halmos #1 | dispatched | -| 3 | `KernelUUPS.upgradeToAndCall` reverts unless `msg.sender == ENTRYPOINT \|\| msg.sender == address(this)`. | `test/halmos/KernelUUPSHalmos.t.sol` | sc-fv-halmos #2 | dispatched | -| 5 | `_verifyStatelessSignature` cannot consume a non-policy / non-signer module into the permission's signature chain (the `bfbef77` regression). | `test/halmos/PermissionStatelessHalmos.t.sol` | sc-fv-halmos #3 | dispatched | -| 8 | `parseNonce` round-trip recovers `(vMode, vType, vId)` for both `VALIDATION_TYPE_VALIDATOR` and `VALIDATION_TYPE_PERMISSION`. | `test/halmos/ParseNonceHalmos.t.sol` | sc-fv-halmos #4 | dispatched | -| 9 | `Kernel7702` and `KernelImmutableECDSA` fallback signature accept iff `ECDSA.tryRecoverCalldata(hash, sig) == expectedSigner`. | `test/halmos/FallbackSignatureHalmos.t.sol` | sc-fv-halmos #5 | dispatched | -| 10 | `Staker.approveFactoryWithSignature` is replay-safe (second call with same `(factory, approval, signature)` reverts) and EIP-712 digest is chain-agnostic. | `test/halmos/StakerReplayHalmos.t.sol` | sc-fv-halmos #6 | dispatched | -| 12 | `KernelFactory.deploy` / `deployECDSA` are deterministic and idempotent (no double-init on second call). | `test/halmos/KernelFactoryHalmos.t.sol` | sc-fv-halmos #7 | dispatched | -| 13 | `_checkAndIncrementNonce` cannot overflow `uint64` (defensive spec property; practically unreachable). | `test/halmos/NonceOverflowHalmos.t.sol` | sc-fv-halmos #8 | dispatched | -| 14 | `_initializeValidation` bumps `vInfo[vId].nonce` by exactly 1 in both the empty-`_internalData` and non-empty paths (no double-bump, no zero-bump). | `test/halmos/InitializeValidationHalmos.t.sol` | sc-fv-halmos #9 | dispatched | - -Each subagent: writes one Halmos file, runs Halmos to green, returns structured findings (no commits — `/commit` skill handles git in a follow-up pass). - -## Phase B — Halmos M-effort (queued) - -| # | Property | File | Status | -| -- | ------------------------------------------------------------------------------------------------- | ----------------------------------- | ------ | -| 7 | `_checkNonce` (view) and `_checkAndIncrementNonce` (write) agree on which `seq` is acceptable under the `nonceValidFrom` ratchet. | `test/halmos/NonceConsistencyHalmos.t.sol` | queued | - -Trigger condition: Phase A all green. - -## Phase C — Certora harness + #1 (queued) - -- Invoke `/setup-certora` to install certora-cli, scaffold `certora/`, configure `CERTORAKEY`. -- Dispatch `sc-fv-certora` on property #1: `executeUserOp`'s inner delegatecall is gated by `validateUserOp` having authorised the outer UserOp under a validation owning the inner selector. -- Expected: `certora/conf/Kernel.conf`, `certora/specs/Kernel.spec`, one rule. - -Trigger condition: Phase A green + user approval. - -## Phase D — Certora deepening (queued) - -| # | Property | Status | -| -- | ------------------------------------------------------------------------------------------------- | ------ | -| 4 | Permission validation totality across the unbounded `policies[]` array, AND signer ERC-1271 must succeed. | queued | -| 6 | `setRoot(packages, removeCurrent=true)` LIFO uninstall fully clears the old root's state. | queued | -| 11 | `_verifySignaturePermission` (view) and `_validateUserOpPermission` (write) return the same aggregate `validationData`. | queued | - -Trigger condition: Phase C harness up. - -## Phase E — Kontrol experiment (queued) - -| # | Property | Status | -| -- | ------------------------------------------------------------------------------------------------- | ------ | -| 15 | `_erc1271IsValidSignatureViaNestedEIP712` only authorises on the explicit success branch (no spurious accepts from assembly path). | queued | - -Trigger condition: Phase A green. May demote to "Halmos partial" if Kontrol setup is too costly. - -## Not in scope for Round 1 - -- **Tama / Clear**: rewrite cost (Tama) and Yul-extraction setup (Clear) not justified for post-release v4 with `via_ir = false`. Reserve for v5 or new greenfield modules. -- **`supportsExecutionMode` exhaustiveness**, **validator-path hook bracketing**, **`isModuleInstalled` for type 7+**: either already proven on `fix/audit-internal-batch-1` (will be pulled forward separately) or out-of-band severity. -- **Gas semantics, full ERC-4337 EntryPoint replay**: belong to integration / fuzz / BTT layers, not FV. - -## Commit & PR plan - -- Each Phase A subagent writes its own file. No commits during dispatch. -- After all 9 land green: team lead invokes `/commit` skill once per file (per the working-tree-discipline rule — never bundle multi-file Halmos additions through one `/commit` call when files share `test/halmos/` and may need to be split). -- After Phase A commits: `/create-pr` opens PR against `master` from `audit/fv-round-1`. -- Phase B, C, D, E may be separate branches/PRs to keep review tractable. - -## Tracking - -- This file (`audit/FV_PLAN.md`) is the live status board. -- Per-property findings land back from subagents and get logged in `audit/fv-round-1-findings.md` (created on first finding). -- The orchestrator's reasoning is preserved verbatim in `audit/fv-gap-audit.md`. - -## How to resume - -If the session ends mid-Phase-A, the next session can: - -1. Read `audit/FV_PLAN.md` (this file). -2. Check `git status` for any test files left in the working tree — those mark partial progress. -3. Re-dispatch `sc-fv-halmos` on any property whose target file is missing or whose `forge build && halmos --match-contract ` fails. -4. When Phase A is all green, ask the user whether to proceed to Phase B (Halmos M) or jump to Phase C (Certora setup). diff --git a/audit/FV_PLAN_ROUND_2.md b/audit/FV_PLAN_ROUND_2.md deleted file mode 100644 index 886ed88d..00000000 --- a/audit/FV_PLAN_ROUND_2.md +++ /dev/null @@ -1,157 +0,0 @@ -# Kernel v4 — FV Round 2 Plan - -> **Strategy**: target *proof-obligation coverage*, not literal line coverage. "Full FV coverage" for this codebase means: every public/privileged entry point, every security-critical storage invariant, every view/write equivalence, every unbounded permission composition path, and every assembly-heavy signature path is either **proven** or **explicitly documented as out of scope**. - -**Branch**: `audit/fv-round-2` (off `audit/fv-round-1` @ `3856e68`) -**Companion docs**: -- [`audit/FV_PLAN.md`](./FV_PLAN.md) — Round 1 multi-phase plan (Phases A-E) -- [`audit/fv-gap-audit.md`](./fv-gap-audit.md) — orchestrator's original gap audit + backend dispatch rationale -- [`audit/fv-round-1-findings.md`](./fv-round-1-findings.md) — Round 1 per-property findings -- [`audit/FV_COVERAGE.md`](./FV_COVERAGE.md) — Live coverage board (to be created in Phase 4) - ---- - -## Phase 1 — Close known gaps from Round 1 - -| # | Property | Round 1 status | Round 2 status | -|---|----------|----------------|----------------| -| 15 | `_erc1271IsValidSignatureViaNestedEIP712` TypedDataSign branch | Kontrol partial (14 SUCCESS, 0 CEX, timeout); Halmos PROVEN on PersonalSign | ✅ **CLOSED** — Kontrol Round 2: 524 nodes, 90 SUCCESS, 0 CEX, hit 500-iter limit. Manual CFG proof closes the gap at `audit/manual-proofs/property-15-erc1271-nested-eip712.md` (commit `a16ff4b`). | -| Phase C invariant | `nonRootCannotBypassFastPathWithExecuteUserOp` | Unprovable under current CVL summaries (NONDET callback havoc) | ✅ **CLOSED** — Writer-local decomposition into 4 rules in `certora/specs/PhaseCWriterLocal.spec` (commit `56d03a2`). All 4 rules + 4 sanity checks PASS. Job: https://prover.certora.com/output/3606101/37e8675776484e4998f16f528d2dd29a | -| Phase D #4 liveness | `allSuccessImpliesAggregateSuccess` | Dropped (Certora `rule_sanity` bitvec gotcha) | Deferred to a future Certora release. Security direction proven; this is liveness. Low priority. | - ---- - -## Phase 2 — Function-by-function proof obligation matrix - -Enumerate every public/external function plus security-relevant internal helper, assign ≥1 FV obligation per row. Backend choice per the matrix: - -- **Halmos** — pure, bounded, state-local -- **Certora** — cross-call, unbounded arrays, multi-step traces -- **Kontrol** — assembly-heavy, calldata-manipulation, precise EVM semantics -- **Manual / sc-critical-thinker** — single-return-site CFG arguments, structural-by-inspection claims - -### Draft surface inventory - -| Contract | Public/external | Internal security-relevant | Round 1 coverage | -|---|---|---|---| -| `Kernel` | execute, executeFromExecutor, executeUserOp, validateUserOp, installModule×2, uninstallModule, setRoot, grantAccess, isValidSignature, upgradeToAndCall, fallback | _processUserOp, _checkValidation | Partial (Phase A #3, #5, #14; Phase C #1; Phase D #4, #6, #11) | -| `ValidationManager` | — | _initializeValidation, _installValidator, _installPolicy, _installSigner, _uninstallValidation, _uninstallValidator, _uninstallPolicy, _uninstallSigner, _grantAccess, _setRoot×2, _verifySignaturePermission, _validateUserOpPermission, _validateUserOpValidator, _validateUserOpFallback, _verifyInstallSignature | Partial (Phase A #5, #14; Phase B #7; Phase D #4, #6, #11) | -| `ModuleManager` | setNonce, setValidNonceFrom, grantAccess wrappers | _checkNonce, _checkAndIncrementNonce, _grantAccess | Partial (Phase A #13; Phase B #7) | -| `ExecutionManager` | — | _executeCall, _executeDelegateCall, _executeBatchCall, _execute | Phase A #3 batch tests on `fix/audit-internal-batch-1` only (pre-Round-1) | -| `KernelFactory` | deploy, deployECDSA, getAddress, getECDSAAddress | _initialize | Phase A #12 | -| `Staker` | approveFactory, approveFactoryWithSignature, stake, unstake | — | Phase A #10 | -| `KernelUUPS` | upgradeToAndCall, proxiableUUID | _authorizeUpgrade | Phase A #3 | -| `Kernel7702`, `KernelImmutableECDSA` | _verifyFallbackSignature (effective entry via isValidSignature) | — | Phase A #9 | -| `lib/ERC1271`, `lib/Lib4337` | _erc1271IsValidSignature*, intersectValidationData | various | Phase A #2; Phase E #15 | - -### Obligation types - -For each function, identify which apply: - -- **AC** (access control): caller restrictions hold -- **TR** (transition): every state change preserves the relevant invariant -- **EQ** (equivalence): two paths (view/write, internal/external, alternate ABIs) agree on the audit-relevant outcome -- **NR** (non-replay): operations are not replayable -- **NB** (non-bypass): no path returns success without the expected predicate holding -- **DT** (determinism): pure functions are deterministic; CREATE2 deployments are deterministic -- **OF** (overflow): arithmetic cannot overflow under reachable preconditions - -### Dispatch ordering (highest leverage first) - -1. **Round 1 remainder**: `_checkValidation`, `_processUserOp` (non-fast-path), `_uninstallValidator/Policy/Signer`, `_verifyInstallSignatureRaw`, `_validateUserOpValidator`, `_validateUserOpFallback` -2. **ExecutionManager**: `_executeCall`, `_executeDelegateCall`, `_executeBatchCall` — each function under each execution mode -3. **Cross-contract**: KernelFactory `getAddress(addr_predicted == addr_deployed)`, Staker stake/unstake monotonicity -4. **UUPS / fallback signers**: extend Phase A #3/#9 to cover error paths and reentrancy guards - ---- - -## Phase 3 — System-level compositional proofs - -Compositional rules that span multiple internal functions or across multiple transactions. - -### Candidates - -| Rule | Description | Backend | Complexity | -|---|---|---|---| -| `validateUserOp_then_executeUserOp` | End-to-end: for any sequence `validateUserOp; executeUserOp`, the inner delegatecall is gated by the validation's authorisation **regardless of mode** (validator / permission / root / fallback × enable-mode × replayable-mode). | Certora | L | -| `install_uninstall_setRoot_lifecycle` | Any install → uninstall → re-install sequence on the same vId leaves the validation in a sound state (no stale grants, correct nonce, hook respected). | Certora | M | -| `enable_mode_install_signature` | An enable-mode UserOp installs the package iff `_verifyInstallSignatureRaw` accepts the root signature. | Certora | M | -| `replayable_userop_hash_chain_agnostic` | A replayable UserOp's digest is `chainid`-independent and the nonce is the replay barrier. | Halmos | S | -| `factory_to_kernel_consistency` | A kernel deployed via `KernelFactory.deploy(pkgs, nonce)` has the same initial state as one constructed and initialised by hand with the same args. | Certora | M | - -### Strategy - -Each compositional rule typically needs: - -- A harness that exposes multiple internal functions as external entry points -- NONDET summaries for **leaf** module calls (validators, policies, signers, hooks) — not for kernel internals -- A multi-step rule that calls the functions in sequence and asserts the compositional invariant - -Round 1's Phase C harness pattern (`certora/harnesses/KernelHarness.sol`) is the starting template. - ---- - -## Phase 4 — Make FV regression-grade - -### Coverage board - -`audit/FV_COVERAGE.md` — a live table that maps each (Contract × Function × Obligation) tuple to: - -- **Backend**: Halmos / Certora / Kontrol / Manual / OOS (out of scope) -- **Status**: Proven / Partial / Failed / NotStarted -- **Job URL or test file path** -- **Regression witness commit** (if a bug was found en route) - -Updated on every Round 2 dispatch and PR merge. Becomes the "FV trust dashboard" reviewers can pin in PRs. - -### Regression witnesses - -One Halmos/Certora test per bug found in this round (or any future round) that would have CEX'd pre-fix. Already started in Round 1: - -- `InitializeValidationHalmos.checkInitializeValidationBumpsByOneEmptyData` ↔ commit `9f9471c` -- `PermissionStatelessHalmos.checkSigIdxDoesNotAdvanceForAnyNonPolicySignerType` ↔ commit `bfbef77` -- `Kernel.spec validateUserOpEnforcesInnerSelectorAccess_naive` ↔ commits `0921b25` + `ce185f6` - -Round 2 continues this pattern for any new findings. - -### PR gating - -- **Per-PR (must pass)**: Halmos on the proven rule set. Cold ~30 s, warm ~10 s. Cheap enough to gate every PR. -- **Nightly (must not regress)**: Certora on the full spec suite (`Kernel.conf`, `Permission.conf`, `SetRootLifo.conf`, `PermissionEquivalence.conf` and any Round 2 additions). Heavy — ~30 min total. -- **Per-release**: Kontrol on the assembly-heavy claims. Expensive but rare. -- **Coverage-board gate**: any PR adding a new public/external function must add a row to `FV_COVERAGE.md` and either an FV obligation or an explicit OOS justification. - ---- - -## Effort & sequencing - -| Phase | Effort estimate | Trigger | -|-------|-----------------|---------| -| 1 (close gaps) | 1-3 days | Start immediately. #15 first, then Phase C invariant split, then Phase D #4 deferred. | -| 2 (matrix) | 2-3 weeks | Start the inventory in parallel with Phase 1. Dispatch as bandwidth allows. | -| 3 (compositional) | 1-2 weeks | After Phase 2 covers the underlying functions. | -| 4 (regression-grade) | 3-5 days | Coverage board can be drafted alongside Phase 1; CI gating once Phase 2 stabilises. | - -Total realistic window for Round 2: **4-6 weeks of focused FV work**, assuming a single FV-focused engineer (or one team lead orchestrating subagents). - ---- - -## Out-of-scope items (declared upfront) - -These are intentionally NOT in Round 2 scope. Adding them later is fine; the OOS declaration is to keep Round 2 finite: - -- **Gas semantics** — handled by gas profiler + BTT tests -- **Cross-chain replay** — handled by integration / fuzz tests; covered for Staker (Phase A #10) -- **External validator/policy/signer module correctness** — Kernel's trust boundary; modules are sandboxed by `_onlyEntryPointOrSelf`, their internal correctness is the module author's responsibility -- **Tama (Lean EDSL)** — rewrite cost not justified for post-release v4 -- **Clear (Yul-on-Lean)** — `via_ir = false` precludes meaningful coverage; would require flipping the foundry profile -- **ERC-1271 nested EIP-712 contentsName encoding edge cases** — partially covered; full closure requires Kontrol with larger budget OR manual proof - ---- - -## How to resume - -1. Read this file + `FV_PLAN.md` + `FV_COVERAGE.md` for state. -2. Check `git status` for any in-flight artifacts. -3. Re-dispatch using the orchestrator (`sc-formal-verifier`) on the highest-priority open obligation. -4. Update `FV_COVERAGE.md` on every dispatch completion. diff --git a/audit/fv-gap-audit.md b/audit/fv-gap-audit.md deleted file mode 100644 index 9fa95bbf..00000000 --- a/audit/fv-gap-audit.md +++ /dev/null @@ -1,117 +0,0 @@ ---- -date: 2026-05-20 -project: kernel-v4 -type: fv-gap-audit -status: dispatch-plan -tags: [formal-verification, gap-audit, halmos, certora, kontrol] -target_vault_path: ~/Documents/Obsidian/projects/kernel-v4/audits/fv-gap-audit.md ---- - -# Kernel v4 — Formal Verification Gap Audit - -> Orchestrator dispatch plan. The user reviews this before any subagent writes proofs. No proofs have been written from this plan yet. This file was written to `audit/` inside the repo because the Obsidian vault is outside the sandbox; documentor should move/copy it to the `target_vault_path` above. - -## Scope - -Source surveyed: `/Users/taek/workspace/kernel_v4/src/` (~2,549 LOC across 16 contracts). -Existing FV artifacts: 14 Halmos test files in `test/halmos/`, ~85 `check_*` functions. No Certora, no Kontrol, no Tama, no Clear. - -## Baseline — What's Already Proven (Halmos) - -| File | Proofs | Surface covered | -|---|---|---| -| `KernelAccessControlHalmos.t.sol` | 3 | `_onlyEntryPointOrSelf` on installModule / execute / executeFromExecutor | -| `KernelBatchExecutionHalmos.t.sol` | 8 | Single/batch × default/try semantics, return-data order | -| `KernelExecutionModeHalmos.t.sol` | 9 | `supportsExecutionMode` matrix, `supportsModule` types 0/1-6/7/100 | -| `KernelExecutorHalmos.t.sol` | 7 | Executor return-data shapes 0/8/32/64/256/1024/4096 | -| `KernelFallbackHalmos.t.sol` | 5 | Uninstalled selector reverts, hook-zero gating, no-hook caller policy | -| `KernelGrantAccessHalmos.t.sol` | 8 | Caller restriction, data alignment, nonce increment, multi-selector | -| `KernelHookBracketingHalmos.t.sol` | 5 | Fallback/executor pre/post hook called, revert paths | -| `KernelInstallSignatureHalmos.t.sol` | 6 | Invalid sig reverts, wrong nonce reverts, nonce consumed, sequential nonces | -| `KernelModuleIdempotencyHalmos.t.sol` | 6 | Install→uninstall round-trip for validator/executor/selector/hook/permission; double-install reverts | -| `KernelModuleSafetyHalmos.t.sol` | 1 | Root validator cannot be uninstalled | -| `KernelNonceHalmos.t.sol` | 9 | `setNonce` / `setValidNonceFrom` monotonic, key independence, nonce layout | -| `KernelSelectorHalmos.t.sol` | 5 | Install/uninstall, callType sender appending, delegatecall doesn't append, hook revert | -| `KernelSetRootHalmos.t.sol` | 9 | Caller restriction (both overloads), uninstalled validator reverts, zero-vId reverts, type validation | -| `KernelSignatureHalmos.t.sol` | 4 | Root signature valid/invalid, invalid type reverts, validator-not-installed reverts | -| `KernelStorageSlotHalmos.t.sol` | 7 | All 6 ERC-7201 slots pairwise distinct + derivations | - -**Source functions touched by existing proofs**: most public entry points on `Kernel` and the major install/uninstall routes through `ModuleManager` / `ValidationManager` / `SelectorManager`. - -**Notable un-touched areas**: `Lib4337.intersectValidationData`, `executeUserOp` linkage to `validateUserOp`, `_verifyStatelessSignature`, permission composition (`_verifySignaturePermission` / `_validateUserOpPermission`), `parseNonce`, `KernelUUPS._authorizeUpgrade`, `Kernel7702` / `KernelImmutableECDSA` fallback signer paths, `setRoot` permission-uninstall LIFO, `Staker.approveFactoryWithSignature` replay safety, `KernelFactory.deploy` determinism. - -## Cross-Cutting Findings on Existing Coverage - -- **Strong**: storage slot distinctness, access control on EP-gated functions, sentinel-value safety on fallback/executor configs, install-signature nonce mechanics, batch execution semantics. -- **Weak**: anything multi-step (permission install → signer → sign → execute), anything involving the unbounded `policies[]` array, anything that requires two functions to agree on the same predicate (e.g. `_checkNonce` view vs `_checkAndIncrementNonce` write under the `nonceValidFrom` ratchet). -- **Untouched**: arithmetic overflow corners (nonce wrap), upgrade authorisation on the UUPS path, the actual security claim documented in `Kernel.executeUserOp`'s SECURITY comment (the safety of the inner delegatecall rests entirely on `validateUserOp` having already approved the outer UserOp). - -## Dispatch Plan - -Severity: -- **Critical** — direct path to account takeover or fund loss. -- **High** — privilege escalation, signature replay, or storage corruption with no reasonable mitigation. -- **Medium** — DoS, configuration corruption, or recovery-required state inconsistency. - -Effort: S = single subagent call, < 1 day. M = 1-2 day shape, multiple lemmas. L = research-level, expect timeouts and refinement. - -### Highest-severity gaps (dispatch order) - -| # | Property | Sev | Backend | Why this backend, not the others | Effort | -|---|---|---|---|---|---| -| 1 | `executeUserOp`'s inner delegatecall to `address(this)` cannot execute any privileged kernel function unless `validateUserOp` already authorised the outer UserOp under a validation that owns the inner selector. | **Critical** | **certora** | Two-step trace property: `validateUserOp(op)` then `executeUserOp(op)` keyed by the same `userOpHash`. The link goes through transient storage (`_validationHook`) and the `_allowedSelector` gating against the inner selector. Halmos can in principle handle two calls but the second call's inner calldata (`userOp.callData[4:]`) is symbolic bytes delegatecalled into `address(this)`, which blows up path exploration. Certora's rule language was built for this: pre = `validateUserOp` succeeded, post = no privileged write occurred unless the validation that authorised the call had selector access. | L | -| 2 | `Lib4337.intersectValidationData` preserves aggregator authority: if `preAgg > 1` and `resAgg == 0`, the result's aggregator is `preAgg`. Mirrored: `preAgg == 0` and `resAgg > 1` → result is `resAgg`. Different non-zero aggregators → result is `1` (failure). All six precedence rules in the source comment hold for every input pair. | **Critical** | **halmos** | Pure function, no storage, six precedence rules over `uint256` packed fields. Bounded symbolic execution is a perfect fit and the source comment flags it `SECURITY CRITICAL`. Certora is overkill; Kontrol/Clear cannot see Solidity-level packed encoding cleanly. | S | -| 3 | UUPS upgrade gating: `upgradeToAndCall` reverts unless `msg.sender == ENTRYPOINT \|\| msg.sender == address(this)`. `_authorizeUpgrade` is internal-view, but the public entry path is what an attacker reaches. | **Critical** | **halmos** | Single-call property; pre = arbitrary caller; post = revert unless caller is in allowlist. Same shape as existing `KernelAccessControlHalmos` tests but on the UUPS contract specifically — pull it forward to match. | S | -| 4 | Permission validation totality: a permission-type UserOp succeeds iff **every** policy in `vInfo[vId].policies` returns success AND the signer returns ERC-1271 magic. No policy can be silently skipped. The intersection chain through `Lib4337.intersectValidationData` preserves this. | **Critical** | **certora** | The policy array is unbounded. Halmos must fix a length to symbolically execute; Certora's `forall i in policies` quantifier expresses this directly. Also the intersection chain through `Lib4337.intersectValidationData` is the exact composition shape Certora was built for. | L | -| 5 | `_verifyStatelessSignature` cannot enroll a non-policy, non-signer module into the permission's signature chain (the `bfbef77` fix). For permission type, only packages with `moduleType == 5` or `moduleType == 6` whose `internalData[0:4] == pId` are consumed. | **High** | **halmos** | Bounded property: for a small `packages.length` (≤ 4) and symbolic `moduleType`, prove that if any package with moduleType ∉ {5,6} and matching pId exists, it is skipped (`sigIdx` not incremented). This is the regression test the fix needs and Halmos handles bounded arrays fine. | S | -| 6 | `setRoot(packages, removeCurrent=true)` with `VALIDATION_TYPE_PERMISSION`: after the call, the old root's `policies.length == 0`, `signer == address(0)`, and `vInfo[oldRoot].hook == NOT_INSTALLED`. The LIFO loop runs in `i = policies.length; i > 0; i--` order. | **High** | **certora** | Multi-step state machine: starts with non-empty `policies` array, runs N+1 internal operations (N policy uninstalls + 1 signer uninstall), ends in the cleared state. Halmos can do this for `policies.length` fixed at 2 or 3 but Certora expresses it cleanly with an invariant + rule. | M | -| 7 | `_checkNonce` (view) and `_checkAndIncrementNonce` (write) agree on which `seq` is acceptable under the `nonceValidFrom` ratchet. Formally: `_checkNonce(n)` returns success iff `_checkAndIncrementNonce(n)` would not revert (run on the same pre-state). | **High** | **halmos** | Single-shot property over two functions sharing storage; the ratchet branch (`nonceValidFrom > nonce[key]`) is the only case to symbolically explore. Pure SMT, no quantifiers needed. | M | -| 8 | `parseNonce` round-trip: encoding `[vMode \| vType \| vId \| nonceKey \| seq]` then parsing recovers exactly `(vMode, vType, vId)` for both `VALIDATION_TYPE_VALIDATOR` (full 20-byte vId) and `VALIDATION_TYPE_PERMISSION` (4-byte pId, lower 16 bytes zero-padded). | **High** | **halmos** | Pure assembly bit-shuffling, symbolic over the 256-bit nonce. Tiny, fast Halmos target. A bug here mis-routes validation → trivial account compromise. | S | -| 9 | `Kernel7702._verifyFallbackSignature` and `KernelImmutableECDSA._verifyFallbackSignature` accept a signature iff `ECDSA.tryRecoverCalldata(hash, sig)` equals the expected signer (the EOA / immutable-args address). No other recovery result authorises the fallback path. | **High** | **halmos** | Single call, pure function over signature bytes. Halmos handles ECDSA via cheatcode modelling. Two variants but identical shape — bundle as one dispatch. | S | -| 10 | `Staker.approveFactoryWithSignature` is replay-safe: a valid signature increments `nonces[factory]`, so the same `(factory, approval, signature)` tuple cannot succeed twice. Uses chain-agnostic EIP-712 — proof must hold across `chainid`. | **High** | **halmos** | Two-call property (first succeeds, second with identical args reverts). Halmos handles sequential calls. The cross-chain claim reduces to "the digest doesn't include `chainid`" which is a constant check. | S | -| 11 | `_verifySignaturePermission` (view, ERC-1271 path) and `_validateUserOpPermission` (write, ERC-4337 path) return the same aggregate `validationData` for a given `(vId, policies, signer, hash, signatures)` tuple. The two paths must not diverge in authorisation. | **High** | **certora** | Two-function equivalence over an unbounded policy array. Quantification on `policies` is Certora territory. Halmos would need a bound on `policies.length` and even then the symbolic `op.signature` rewriting inside the UserOp path makes the SMT explode. | L | -| 12 | `KernelFactory.deploy` is deterministic and idempotent: for any `(initialPackages, nonce)` the deployed address equals `getAddress(initialPackages, nonce)`, and a second call returns the same address without re-initializing (no double-init). Same for `deployECDSA`. | **Medium** | **halmos** | Pure salt derivation + LibClone semantics. The no-double-init claim is a state property over two consecutive calls. Both fit in a single Halmos file. | S | -| 13 | `_checkAndIncrementNonce` cannot overflow `uint64` within a single transaction (the `++` is safe under Solidity's overflow check, given `_nonce` is provided externally). Equivalent: no input drives `nonce[key]` from below `type(uint64).max` to wrap. | **Medium** | **halmos** | Pure arithmetic bound; tiny SMT obligation. Practically unreachable but the spec-level claim deserves a proof for completeness. Pair with SMTChecker enabled in CI for defence-in-depth. | S | -| 14 | `_initializeValidation`: both the empty-`_internalData` path and the non-empty path leave `vInfo[vId].nonce` at exactly `previous + 1`. Existing tests cover happy path; this is the "no-double-bump and no-zero-bump" invariant explicitly. | **Medium** | **halmos** | Single-call, single-storage-slot property. Halmos. | S | -| 15 | ERC-1271 nested EIP-712 (`_erc1271IsValidSignatureViaNestedEIP712` and the Replayable variant) does not return success when the contents-hash reconstruction fails. The assembly path is intricate; only the explicit success branch should authorise. | **Medium** | **kontrol** | The function is heavy assembly with calldata manipulation. Halmos can run it but the SMT cost of symbolic-bytes calldata copies is high. Kontrol/KEVM reasons natively over the assembly. If Kontrol setup turns out too expensive for one property, demote to Halmos with a bounded signature length and mark the audit entry "partial". | L | - -### Properties intentionally NOT proposed (and why) - -- **`supportsExecutionMode` exhaustiveness for unsupported types** — already proven in `KernelExecutionModeHalmos.t.sol`. -- **Validator-path hook bracketing** — only fallback and executor hook bracketing are covered today. Adding the validator-path version would be valuable but it's Medium severity at best and the bracketing logic is shared across paths; defer until the higher-severity items land. -- **`isModuleInstalled` correctness for type 7+** — already proven via `check_DoesNotSupportModuleType7`. -- **Mode dispatch / gas semantics** — out of scope for FV; handled by BTT + gas tests. -- **Tama / Clear properties** — Kernel v4 is post-release with audits and a Foundry/Yul toolchain. The rewrite cost of Tama (Lean EDSL) and the Yul-extraction setup of Clear (which would also have to grapple with `via_ir = false`) is not justified for v4. Reserve Tama/Clear for a hypothetical v5 redesign or for the most critical greenfield primitive. - -## Backend Tally - -| Backend | Properties | Effort total | -|---|---|---| -| `sc-fv-halmos` | 2, 3, 5, 7, 8, 9, 10, 12, 13, 14 — **10 properties** | ~8-10 days | -| `sc-fv-certora` | 1, 4, 6, 11 — **4 properties** | ~3-4 weeks incl. setup | -| `sc-fv-kontrol` | 15 (preferred) — **1 property** | ~1 week incl. Kontrol setup | -| `sc-fv-clear` | 0 | — | -| `sc-fv-tama` | 0 | — | - -## Recommended Dispatch Order - -1. **Phase A — Halmos S-effort gaps in parallel**: #2, #3, #5, #8, #9, #10, #12, #13, #14. Most are file-disjoint so parallel-safe; collision risk only on `test/halmos/` itself which the per-property file naming convention already handles. -2. **Phase B — Halmos M-effort**: #7 (`_checkNonce` ↔ `_checkAndIncrementNonce` consistency). -3. **Phase C — Certora setup + first property**: #1. This is the single highest-value proof in the entire codebase; Certora setup pays for itself here. -4. **Phase D — Certora deepening**: #4, #6, #11 once #1 has unblocked the Certora harness. -5. **Phase E — Kontrol experiment**: #15. If Kontrol setup is too costly, demote to a Halmos partial. - -## Confidence After Full Plan Lands - -- Halmos-proven (Phase A + B): ~95 properties total (existing 85 + new 10). -- Certora-proven: 4 critical multi-step / unbounded-data claims. -- Kontrol-proven: 1 (or Halmos partial). -- **Acknowledged unproven**: full ERC-1271 nested EIP-712 if Kontrol fails; gas semantics; cross-contract real-EntryPoint replay (handled by integration / fuzz tests, not FV). - -## Notes for the Subagents (when dispatched) - -- Halmos compatibility: v0.3.3, `check_*` / `invariant_*` prefix. Match the existing file's naming convention (mix of `check_X` and `checkX` is present — keep the file consistent internally). -- Run `forge clean` before `halmos` since v0.3.3 occasionally produces artifacts without AST. -- `vm.expectRevert(bytes4)` is not supported in Halmos. Use `try { ... assert(false); } catch {}` or low-level `(bool success,) = ...; assertFalse(success);`. -- `foundry.toml` has `via_ir = false` for contract-size reasons. This rules out Clear (which reasons about Yul output) unless we accept a separate compile pipeline. -- Specs live in `~/Documents/Obsidian/projects/kernel-v4/specs/` (when documentor has populated them — at the moment the source-level NatSpec is the de facto spec). diff --git a/audit/fv-round-1-findings.md b/audit/fv-round-1-findings.md deleted file mode 100644 index 028cabd0..00000000 --- a/audit/fv-round-1-findings.md +++ /dev/null @@ -1,415 +0,0 @@ ---- -date: 2026-05-20 -branch: audit/fv-round-1 -type: fv-findings -status: in-progress ---- - -# Kernel v4 — FV Round 1 Findings - -Subagent results as they land. Each entry: property, status, file, notable observations, follow-ups. - -## Phase A — Halmos (in flight) - -### ✅ #2 — `Lib4337.intersectValidationData` aggregator precedence - -- **Status**: PROVEN (8/8 checks pass, 0.30s total wall time) -- **File**: `test/halmos/Lib4337Halmos.t.sol` -- **Checks**: - - `checkRule1_PreFailure` — preAgg==1 ⇒ result agg==1 - - `checkRule1_ResFailure` — resAgg==1 ⇒ result agg==1 - - `checkRule2_BothSuccess` — both 0 ⇒ result agg==0 - - `checkRule3_PreserveAggregator` — **SECURITY CRITICAL** — preAgg>1 & resAgg==0 ⇒ result agg==preAgg - - `checkRule4_AdoptAggregator` — preAgg==0 & resAgg>1 ⇒ result agg==resAgg - - `checkRule5_SameAggregator` — preAgg==resAgg>1 ⇒ result agg==preAgg - - `checkRule6_ConflictingAggregators` — preAgg>1 & resAgg>1 & differ ⇒ result agg==1 - - `checkAggregatorPreservedWhenResAgg0` — combined regression guard with fully symbolic words -- **Notable observations**: - - The impl has an early-out (`if (preValidationData == 0 || validationRes == 0) return preValidationData | validationRes;`) not enumerated as a separate rule. Aggregator-only checks are insensitive to this branch. - - Agent masked out bit 47 of each uint48 time field (`CLEAR_MODE_BITS = ~((1<<255) | (1<<207))`) to avoid the orthogonal `ValidityFormatMismatch` revert path. Mask is symbolic, not a fixed concrete value. - - Source comment is ambiguous about whether `preAgg == resAgg == 0` belongs to rule 2 or rule 5. Impl reads rule 2 first; agent constrained rule 5 check to `agg > 1` to keep rules disjoint. -- **Follow-up**: separate Halmos dispatch later to verify the `ValidityFormatMismatch` revert path itself (rejects malformed-format inputs). - -### ✅ #3 — `KernelUUPS.upgradeToAndCall` caller gating - -- **Status**: PROVEN (3/3 checks) -- **File**: `test/halmos/KernelUUPSHalmos.t.sol` -- **Worktree branch**: `worktree-agent-ae153a8b47bc09c98` -- **Checks**: - - `checkUpgradeToAndCallRevertsForArbitraryCaller` — pass, 1 path - - `checkUpgradeToAndCallSucceedsForEntryPoint` — pass, 1 path - - `checkUpgradeToAndCallSucceedsForSelf` — pass, 2 paths -- **Notable observations**: - - Solady's `UUPSUpgradeable` only exposes `upgradeToAndCall`; no `upgradeTo(address)` to cover separately. - - Allowlist is exactly `{ENTRYPOINT, address(this)}` via `_onlyEntryPointOrSelf` — no role registry, no module bypass. - - **Important harness note**: agent deployed a real ERC1967 proxy via `LibClone.deployERC1967(impl)` and called the proxy, NOT the implementation directly. The existing `KernelExecutorHalmos` pattern (`new KernelUUPS(...)`) would short-circuit on Solady's `onlyProxy` modifier (`UnauthorizedCallContext()`) and never reach the auth check. Future Halmos harnesses on upgrade paths must follow the proxy pattern. - - Agent ran a probe to confirm proofs aren't vacuous: forced `ok == false` for EntryPoint case and Halmos produced a counterexample. - -### 🚨 #5 — `_verifyStatelessSignature` moduleType filter — **BUG WITNESS** (fix already on `fix/audit-internal-batch-1`) - -- **Status**: COUNTEREXAMPLE on `master`/`audit/fv-round-1` @ `a836274` (pre-fix). PROVEN GREEN when commit `bfbef77` is applied. -- **File**: `test/halmos/PermissionStatelessHalmos.t.sol` -- **Worktree branch**: `worktree-agent-a79a0778c7f9061eb` -- **Checks**: - - `checkSanitySinglePolicyAccepts` — positive control, passes (confirms harness wiring is correct) - - `checkSigIdxDoesNotAdvanceForModuleType1` — FAIL on master (VALIDATOR type sneaks in) - - `checkSigIdxDoesNotAdvanceForModuleType4` — FAIL on master (HOOK type sneaks in) - - `checkSigIdxDoesNotAdvanceForAnyNonPolicySignerType` — FAIL on master, symbolic counterexamples at wrongModuleType ∈ {1, 2, 3, 4} -- **The bug**: - - At `src/core/ModuleManager.sol:339` (on master), the permission-branch signature loop accepts any package with `internalData[0:4] == pId` regardless of `moduleType`. - - A non-policy / non-signer module (VALIDATOR=1, EXECUTOR=2, FALLBACK=3, HOOK=4) whose `internalData[0:4]` happens to equal `pId` is consumed into the signature chain. -- **Fix maps to**: `bfbef77 fix: filter permission stateless match by module type` (1 line: add `&& (pkg.moduleType == 5 || pkg.moduleType == 6)`). -- **Notable observations from agent**: - - Calldata-layout gotcha: `abi.encode(struct)` wraps in a 1-tuple with an outer offset that the source's inline assembly `permissionSig := signature.offset` doesn't expect. Agent encoded `abi.encode(sigs)` (inner `bytes[]` directly). Without this fix the harness reverts vacuously — positive-control test exists to catch regression. - - `packages.length = 2` was the minimum needed: length 1 cases are vacuously rejected by the existing "last signature is signer" require. - -## Branch divergence summary - -**Master is missing two fixes that already exist on `fix/audit-internal-batch-1`**: - -| Bug | Fix commit | Date | Status on master | -|-----|-----------|------|-------------------| -| `_initializeValidation` empty-data path doesn't bump nonce → stale selector grants survive uninstall+empty-reinstall | `9f9471c` | 2026-04-29 | **NOT MERGED** | -| `_verifyStatelessSignature` accepts non-policy/non-signer modules into signature chain | `bfbef77` | 2026-04-29 | **NOT MERGED** | - -Both fixes (plus 3 other audit fixes: `bccbb5d`, `5a6c865`, `d54c56a`) are sitting on `fix/audit-internal-batch-1`, which is also unmerged. - -The Halmos tests we just authored act as **regression witnesses** — they would have caught these bugs pre-fix and will pin the fix in place post-merge. - -### ✅ #8 — `parseNonce` round-trip - -- **Status**: PROVEN (2/2 checks, 0.01s) -- **File**: `test/halmos/ParseNonceHalmos.t.sol` -- **Worktree branch**: `worktree-agent-a2e3e14e9362e728a` -- **Checks**: - - `checkParseNonceRoundTripValidator` — pass, 1 path - - `checkParseNonceRoundTripPermission` — pass, 1 path -- **Notable observations**: - - `checkParseNonceRejectsInvalidVType` was NOT authored — the function has no revert branch. The `else` clause accepts every `vType ≠ 0x02` including `0x00 (ROOT)`, `0x01 (VALIDATOR)`, and junk. Caller-side enforcement lives at `ValidationManager._validateValidationData:339-340`. Re-dispatch the rejection check there in Phase B. - - `vType` byte is doubly encoded — it's at byte[1] AND high byte of `vId`. After parsing, `vType == vId[0]` is an invariant. Source comment in `Utils.sol:42-44` is slightly misleading. - - The 16 zero bytes between `pId` and `nonceKey` in the permission encoding are mandatory; non-zero values there are silently dropped. - - Negative control verified — agent flipped expected type byte to 0x02 in validator check and Halmos correctly produced a counterexample. - -### ✅ #9 — `Kernel7702` + `KernelImmutableECDSA` fallback ECDSA - -- **Status**: PROVEN (2/2 checks, 0.08s) -- **File**: `test/halmos/FallbackSignatureHalmos.t.sol` -- **Worktree branch**: `worktree-agent-aa60b59a740a18832` -- **Checks**: - - `checkKernel7702FallbackAcceptsIffExpectedSigner` — pass, 5 paths - - `checkKernelImmutableECDSAFallbackAcceptsIffExpectedSigner` — pass, 5 paths -- **Notable observations**: - - Agent needed `--default-bytes-lengths 0,64,65,66,128` to enumerate both ECDSA length classes (64 EIP-2098 + 65 standard) plus the `default { break }` fall-through. Halmos's default `[0, 65, 1024]` would skip length 64. - - Required `--function check` to match the project's no-underscore prefix convention. - - Both proofs are tight; iff is checked bit-for-bit over fully symbolic `(hash, sig)`. No vm.assume. - -### ✅ #10 — `Staker.approveFactoryWithSignature` replay safety - -- **Status**: PROVEN (3/3 checks, 0.28s) -- **File**: `test/halmos/StakerReplayHalmos.t.sol` -- **Worktree branch**: `worktree-agent-a8edd42254b6d4aad` -- **Checks**: - - `checkApproveFactoryWithSignatureBumpsNonce` — nonce += 1 on success - - `checkApproveFactoryWithSignatureReplayDigestDiffers` — bumped nonce flows into next digest, so replay produces a different digest - - `checkApproveFactoryWithSignatureDigestChainIdIndependent` — `digest(chainA) == digest(chainB)`, confirms `_hashTypedDataSansChainId` is in use -- **Notable observations**: - - Halmos cannot directly prove "second call reverts" because ECDSA is modeled as an uninterpreted function — solver can pick recovered addresses such that both digests recover to `owner()`. So the property decomposes into (a) digest differs + nonce advances (proven by Halmos), and (b) one signature validates only one digest (ECDSA collision-resistance, outside Halmos). Standard decomposition. - - Chain-id-independence: 2 paths, structurally proves the digest assembly doesn't read `chainid()`. - - Signature symbolised at 65 bytes; storage seeded via `vm.store` for symbolic starting nonce. - -### ✅ #12 — `KernelFactory.deploy` determinism + no double-init - -- **Status**: PROVEN (4/4 checks, 0.15s) -- **File**: `test/halmos/KernelFactoryHalmos.t.sol` -- **Worktree branch**: `worktree-agent-a34511133d8e83c9c` -- **Checks**: - - `checkDeployMatchesGetAddress(uint256 nonce)` — UUPS variant, deterministic - - `checkSecondDeployReturnsSameAddressNoReinit(uint256 nonce)` — UUPS variant, idempotent - - `checkDeployECDSAMatchesGetECDSAAddress(address signer, uint256 nonce)` — ECDSA, deterministic - - `checkSecondDeployECDSAReturnsSameAddressNoReinit(address signer, uint256 nonce)` — ECDSA, idempotent -- **Notable observations**: - - `initialPackages` constrained to `length=1, type-1 root validator` — CREATE2 salt is independent of package contents once hashed, so this doesn't weaken the property. - - The no-double-init claim is an INDIRECT proof: factory branches on `alreadyDeployed` from `LibClone.createDeterministicERC1967` and skips `initialize`; Solady's `initializer` modifier would revert on a second init; Halmos proves the second deploy doesn't revert → therefore no re-init path exists. - - For a direct proof, would need harness access to `Initializable._INITIALIZED_SLOT`. Current formulation is the tightest indirect proof. - -### ✅ #13 — `_checkAndIncrementNonce` no overflow - -- **Status**: PROVEN (1/1 check, 0.05s, 6 paths) -- **File**: `test/halmos/NonceOverflowHalmos.t.sol` -- **Worktree branch**: `worktree-agent-a54da47d4c4adf039` -- **Notable observations**: - - Postcondition computed in `uint256` so any uint64 wrap manifests as `LHS=0, RHS=2^64` counterexample. - - Fully symbolic over `uint64 × uint64 × uint64 × uint192`. No vm.assume. - - Agent confirmed by grep: no `unchecked` blocks touch `nonce[key]` anywhere in `src/Kernel.sol`, `src/core/ModuleManager.sol`, `src/core/ValidationManager.sol`. The only `unchecked` blocks are in unrelated loops. - - Function location: `src/core/ModuleManager.sol:268`. - -### 🚨 #14 — `_initializeValidation` bumps by 1 — **BUG FOUND** - -- **Status**: SPLIT — empty-data path is a COUNTEREXAMPLE; non-empty path PROVEN -- **File**: `test/halmos/InitializeValidationHalmos.t.sol` -- **Worktree branch**: `worktree-agent-af9720c11ddd2ab96` -- **Checks**: - - `checkInitializeValidationBumpsByOneEmptyData` — **COUNTEREXAMPLE** (impl bug) - - `checkInitializeValidationBumpsByOneNonEmptyData` — pass, 3 paths, 0.05s -- **The bug**: - - `_initializeValidation` (`src/core/ValidationManager.sol:85-100`): empty `_internalData` path (lines 89-92) sets `hook = address(1)` and returns. **No nonce bump.** - - `_uninstallValidation` (`src/core/ValidationManager.sol:139-143`): zeroes `hook`. **Leaves `nonce` and `allowed[vId][*]` intact.** - - Attack sequence: `install(vId, "hook||selectors")` → `uninstall(vId)` → `install(vId, "")` resurrects stale `allowed[vId][selector] == nonce` grants from the prior install. Old selectors come back to life with the empty reinstall. -- **Severity assessment**: HIGH. Reachable only via owner-gated `installModule` (EP-or-self), so requires owner cooperation. Impact: footgun + privilege smuggling — owner thinks empty-data reinstall = clean slate, but historical selector grants persist. Worse if the same `vId` is reused with different intent across installs. -- **Recommended fix**: at `src/core/ValidationManager.sol:89-92`, either (a) bump `++nonce` unconditionally before the early return, or (b) clear `allowed[vId][*]` entries on uninstall. Option (a) is the minimal patch and matches the property's expectation. -- **Caveats noted by agent**: - - Required `vm.assume(preNonce < type(uint32).max)` to avoid orthogonal overflow concerns (separate property #13). Not a weakening. - - Non-empty path bound `_internalData.length=24` (20-byte hook + 4 selectors). Structural shape is general; selector count doesn't affect the nonce bump. - - `_internalData.length == 20` edge case (hook only, zero selectors) verified by inspection — single bump via `_grantAccess` with empty selectors. Agent suggests a third check could cover symbolically. - -## Phase B — Halmos M-effort - -### ✅ #7 — `_checkNonce` ↔ `_checkAndIncrementNonce` agreement below saturation - -- **Status**: PROVEN (3/3 checks, 0.26s) -- **File**: `test/halmos/NonceConsistencyHalmos.t.sol` -- **Checks**: - - `check_RatchetBranchAgreement` — view/write agree on `nonceValidFrom > preSeq` branch - - `check_NonRatchetBranchAgreement` — view/write agree on `nonceValidFrom ≤ preSeq` branch - - `check_AgreementBelowOverflowSaturation` — general agreement, both branches combined -- **Boundary finding**: at `effectivePre == type(uint64).max`, the view path accepts (`seq == effective`) while the write path reverts from the checked `nonce[key]++` overflow. This is the ONLY divergence across the entire `(key, preSeq, validFrom, seq)` state space. -- **Why this is acceptable**: `NonceOverflowHalmos.check_NonceCannotOverflow` proves `nonce[key]` cannot reach `type(uint64).max` organically. The only way to land there is owner-induced via `_setValidNonceFrom(type(uint64).max)` — owner self-DOS, detectable on-chain. -- **Each check excludes the boundary with an explicit, documented `vm.assume`** — not a silent weakening. Cross-references `NonceOverflowHalmos` inline. -- **Alternative considered**: apply a one-line fix to `_checkNonce` (add `require(effective < type(uint64).max)`) to make the agreement unconditional. Deferred — current behaviour is provably safe via the cross-property argument, and changing source for a vacuous edge case requires sc-developer dispatch + reaudit. - -## Phase C — Certora - -### 🚨 #1 — `executeUserOp` ↔ `validateUserOp` linkage — **HIGH severity bug found** - -- **Status**: split — strict form PROVEN; naive form COUNTEREXAMPLE surfaces a real privilege-escalation bug. -- **Files**: - - `certora/conf/Kernel.conf` - - `certora/specs/Kernel.spec` (3 rules) - - `certora/harnesses/KernelHarness.sol` -- **Certora job reports**: - - All 3 rules: https://prover.certora.com/output/3606101/9bae8478ce9842bcae2d45f92487e40b?anonymousKey=0f69fd410a6d5eb1218d0931ebae1e5e8161b63d - - Strict-only PASS: https://prover.certora.com/output/3606101/fa191e6ffa3e43f6aac8860d357737f4?anonymousKey=d6261fb0d8c99d0dfba76de0a402448046b24332 -- **Wall time**: 7.7 min, prover 472s. - -#### Rule results - -| Rule | Status | Notes | -|---|---|---| -| `validateUserOpEnforcesInnerSelectorAccess_naive` | **FAIL** | CEX exposes the fast-path bypass | -| `validateUserOpEnforcesInnerSelectorAccess_strict` | **PASS** | Holds with `!fastPath` precondition | -| `sanityValidateUserOpReachesSuccess` (satisfy) | **PASS** | Rule setup is not vacuous | - -#### The bug - -`src/Kernel.sol:172-185` — `_processUserOp`'s fast-path: - -```solidity -if ( - vType == VALIDATION_TYPE_ROOT - || (_allowedSelector(vId, bytes4(userOp.callData[0:4])) - && $.vInfo[vId].hook == HOOK_MODULE_INSTALLED_NO_HOOK) -) { - // No-op — fast path, NO inner-selector check, NO _setValidationHook -} else { ... require + _setValidationHook ... } -``` - -When a non-ROOT validation `V` has `executeUserOp.selector` in its allowed list AND `hook == HOOK_MODULE_INSTALLED_NO_HOOK`: - -1. Fast-path is taken. -2. Inner-selector `require` is skipped — no check on `userOp.callData[4:]`. -3. `_setValidationHook` is NOT called → transient hook stays 0. -4. `executeUserOp` then runs `_preHook`/`_postHook` as no-ops (hook is 0). -5. Inner `delegatecall` to `address(this)` executes ANY selector — `installModule`, `setRoot`, `upgradeToAndCall`, etc. - -#### Severity - -**HIGH**. Exploitability gate is configuration — `_grantAccess` accepts any selector list, including `executeUserOp.selector`. An owner configuring a validation with what they think is "scoped access to executeUserOp" actually grants root-level dispatch. - -#### Concrete counterexample from Certora - -- `op.callData.length == 8` -- `bytes4(op.callData[0:4]) == 0x8dd7712f` (`executeUserOp.selector`) -- `bytes4(op.callData[4:8]) == 0x3751` (arbitrary unauthorised selector, symbolic) -- `vId == 0xffffffffff00000000000000000000000000000001` (PERMISSION type) -- `_allowedSelector(vId, executeUserOp.selector) == true` -- `vInfo[vId].hook == HOOK_MODULE_INSTALLED_NO_HOOK` -- `vMode` bits 0x08 / 0x40 both off — finding is independent of enable-mode and replayable-mode - -#### Fix path (selected: Option 1) - -Block `executeUserOp.selector` from being granted to non-ROOT vIds in `ValidationManager._grantAccess`: - -```solidity -require( - selector != IKernel.executeUserOp.selector || vId == $.root, - InvalidSelectorGrant() -); -``` - -Defense-in-depth at the configuration boundary. Will be dispatched to `sc-developer`. - -#### Caveats / narrowings (documented in spec header) - -- Strict rule excludes `vMode & 0x08` (enable mode) and `vMode & 0x40` (replayable) for Certora tractability. Both invoke unbounded-bytes hashing (`_verifyInstallSignatureRaw`, `Lib4337.chainAgnosticUserOpHash`). Fast-path bypass is independent of these modes. -- Internal validators (`_validateUserOpValidator/Permission/Fallback`) and `Lib4337.intersectValidationData` are NONDET-summarised to fit in Certora's memory budget. Sound because the fast-path branch reaches the require BEFORE these are invoked. -- External module callbacks are AUTO-HAVOC'd. Sound because `_onlyEntryPointOrSelf` prevents reentrant ValidationStorage writes. -- `optimistic_hashing: true`, `hashing_length_bound: 512` documented in `certora/conf/Kernel.conf`. - -## Phase C Round 2 — re-verify after `_grantAccess` fix - -### ✅ Original bug closed - -After commit `0921b25` (`_grantAccess` blocks `executeUserOp.selector` for non-root vIds): - -| Rule | Round 1 | Round 2 | -|---|---|---| -| `validateUserOpEnforcesInnerSelectorAccess_naive` | 🚨 FAIL (CEX) | ✅ **PASS** | -| `validateUserOpEnforcesInnerSelectorAccess_strict` | ✅ PASS | ✅ PASS (regression) | -| `sanityValidateUserOpReachesSuccess` | ✅ PASS | ✅ PASS (regression) | - -Round 2 job: https://prover.certora.com/output/3606101/19ed688fd26e43cfa25d435306bec6f1?anonymousKey=a87fff01a79ea67c696ced6eb56bd0dbae8403e7 - -### 🚨 Secondary finding — `setRoot` residual - -New invariant `nonRootCannotAllowExecuteUserOp` FAILS on 8 entry points. All reduce to a single primitive: **`_setRoot` does not bump `vInfo[oldRoot].nonce`**, so prior grants of `executeUserOp.selector` to the old root remain active when the old root becomes non-root. - -Failing entry points (induction step) and how each reaches `_setRoot`: - -- `setRoot(bytes21)` — direct -- `setRoot((uint256,address,bytes,…))` overload — direct -- `initialize((uint256,address,…))` — root install path -- `executeUserOp(...)` — inner delegatecall to `setRoot` -- `execute(bytes32,bytes)` — routed batch / single call -- `executeFromExecutor(...)` — executor module calls `setRoot` -- `upgradeToAndCall(...)` — new impl's init data calls `setRoot` -- `()` — fallback path - -Attack sequence (after the `_grantAccess` fix): - -1. `setRoot(R1)` → `$.root = R1` -2. `_grantAccess(R1, executeUserOp.selector)` — permitted (R1 is currently root) -3. `setRoot(R2)` → `$.root = R2`; `allowed[R1][executeUserOp]` stays non-zero; `vInfo[R1].hook` preserved -4. R1 is now non-root with `_allowedSelector(R1, executeUserOp.selector) == true` and `hook == HOOK_MODULE_INSTALLED_NO_HOOK` -5. Fast-path bypass re-engages — R1 can call `executeUserOp(arbitrary inner calldata)` and invoke any privileged function - -Lower likelihood than the Round 1 attack (requires root rotation + prior grant + hook preserved) but FV demonstrates structural reachability. - -### Selected remediation — Option E - -Bump `vInfo[oldRoot].nonce` in `_setRoot` so any stale `allowed[oldRoot][*]` grants are invalidated (`allowed[oldRoot][sel] != vInfo[oldRoot].nonce` post-rotation). Same pattern as Phase A #14. - -### ✅ Phase C closed — Round 3 / 4 invariant abstraction limit - -After `_setRoot` fix (`ce185f6`) we tried two stronger invariant forms: - -| Round | Form | Outcome | -|---|---|---| -| 3 | `allowedNonce(vId, exec) != vInfoNonce(vId)` | FAIL — base case fails on uninstalled vIds (`0 != 0` is false). | -| 4 | Bypass-impossible: `NOT (_allowedSelector AND hook == INSTALLED_NO_HOOK)` | FAIL — Certora's external-callback AUTO-HAVOC violates the invariant on every entry point with a delegatecall (`executeUserOp`, `execute`, `validateUserOp`, `installModule`, `setRoot`, `grantAccess`, `upgradeToAndCall`, ``, `initialize`). `_onlyEntryPointOrSelf` prevents this in production, but encoding precise CVL summaries for all ~10 callback sites is days of work and likely OOMs. | - -Round 4 job: https://prover.certora.com/output/3606101/e16f05be609a48b79c6bfa16f7c357f4?anonymousKey=39f0672f112513c790ec1d6d8ba351876073e395 - -**Decision (2026-05-21)**: accept the invariant as unprovable under current summaries. Phase C closes with the audit story carried by: - -1. `validateUserOpEnforcesInnerSelectorAccess_naive` PASSES post-fix — original CEX unreachable. -2. `validateUserOpEnforcesInnerSelectorAccess_strict` PASSES — precise property under `!fastPath`. -3. Manual static-writer analysis: `_grantAccess` (with fix), `_setRoot` (with fix), `_uninstallValidation`, `_initializeValidation` are the only writers of relevant storage; each preserves the bypass-impossible property by inspection. - -Invariant retained in spec as documented intent + regression target. - -## Phase D — Certora deepening - -### ✅ #6 — `setRoot` LIFO clear of permission state - -- **Status**: PROVEN (1 rule + 1 satisfy) -- **File**: `certora/specs/SetRootLifo.spec`, `certora/conf/SetRootLifo.conf` -- **Rules**: - - `setRootClearsOldPermissionState` — after `setRoot(packages, removeCurrent=true)` on a permission-type root: `policies.length == 0`, `signer == 0`, `hook == NOT_INSTALLED` - - `sanitySetRootReaches` (satisfy) — non-vacuous -- **Job**: https://prover.certora.com/output/3606101/7e3f99aaf47a4257a372d14ce591dea6 -- **Bound**: `policies.length <= 3` to match `loop_iter: 3`; soundly extends to longer arrays by induction on intersect's monotonicity. -- **Static observations** noted by subagent (not bugs, context): - - `_install` runs BEFORE the LIFO loop snapshot; if `pkg[0]` is a policy/signer that matches the old root's pId, it pushes into `policies[]` before the loop runs. Caller must pad `uninstallData` accordingly or the call reverts (sound — no skip). - - `_uninstallPolicyWithVid` uses `policies.pop()`, which Solidity clears correctly. No residue. - - `_uninstallSignerWithVid` requires `policies.length == 0` THEN zeros signer + calls `_uninstallValidation` which zeros hook. Sequence matches the property. - - Aliasing case `pkg[0].moduleType ∈ {policy, signer} && completes oldRoot's pId`: `_setRoot` becomes a no-op rotation, `removeCurrent` block hits `CannotUninstallRoot` → safe revert. - -### 🟡 #4 — Permission validation totality (3/4 rules PASS) - -- **Status**: SECURITY DIRECTION PROVEN, LIVENESS DIRECTION DROPPED -- **File**: `certora/specs/Permission.spec`, `certora/conf/Permission.conf` -- **Rules**: - - `policyFailureImpliesAggregateFailure` — ✅ PASS — any policy returning failure forces aggregate failure - - `signerFailureImpliesAggregateFailure` — ✅ PASS — signer returning failure forces aggregate failure - - `sanityCanSucceed` (satisfy) — ✅ PASS — non-vacuous - - `allSuccessImpliesAggregateSuccess` — **DROPPED** (CVL artifact, see below) -- **Why dropping `allSuccess` is OK**: - - The audit's core claim is the security direction: "no policy can be silently skipped". The two failure rules establish this directly: any failing module forces aggregate failure, so the only way for the aggregate to succeed is for EVERY module to have succeeded. - - The dropped rule's direction is liveness ("if every module succeeds, aggregate succeeds") — important operationally but not a security claim. - - Liveness is empirically established by the 1341 passing Foundry tests, many of which exercise permission UserOps with successful modules → successful aggregate. -- **Why we couldn't prove `allSuccess` in CVL**: - - Three formulations attempted (forall+mask, enumerated, implication-form) — all tripped Certora's `rule_sanity` "bounds check on int to bitvec" sub-check. - - This is a CVL-internal type-checker artifact, not a contract bug. The check fires BEFORE the assertion is evaluated; it concerns the satisfiability of the rule's preconditions when `forall address` meets bitwise masks. - - Documented in `specs/Permission.spec` as a regression target for future CVL releases. - -### ✅ #11 — View/write permission path equivalence on success/failure - -- **Status**: PROVEN (1 rule + 1 satisfy) -- **File**: `certora/specs/PermissionEquivalence.spec`, `certora/conf/PermissionEquivalence.conf` -- **Rules**: - - `viewAndWritePathsAgreeOnSuccess` — view (ERC-1271) and write (ERC-4337) paths agree on the binary success/failure outcome for the same `(vId, hash, signature)` tuple - - `sanityViewPathReaches` (satisfy) — non-vacuous -- **Job (final)**: https://prover.certora.com/output/3606101/22e774d8687e4b869ece01503dc66aa8 -- **Spec evolution** (rounds 1–4): - 1. Full `uint256` equality — FAIL by design (view's `bytes4`-lift can't encode time bounds) - 2. Binary outcome with `signerGhostUint == 0 <=> bytes4 == MAGIC` axiom — FAIL (axiom too narrow; ignored aggregator bits) - 3. Tightened axiom + iff on `intersectGhost` — FAIL (signer ghost still had arbitrary upper bits) - 4. Single source-of-truth `signerSucceedsGhost` boolean with CVL helpers deriving both ABI returns — **PASS** -- **Important reframing**: the audit's claim "the two paths must not diverge in authorisation" was originally stated as full `validationData` equality. The correct formulation is the binary success/failure agreement — by design, the view path (ERC-1271 `bytes4`) cannot express time bounds that the write path (ERC-4337 `uint256`) carries. - -## Phase E — Kontrol + Halmos (complementary partial coverage on #15) - -### Property #15 — ERC-1271 nested EIP-712 success-branch-only authorisation - -**Goal**: prove that `_erc1271IsValidSignatureViaNestedEIP712` (and the Replayable variant) in `src/lib/ERC1271.sol` only return `true` when the inner `_erc1271IsValidSignatureNowCalldata(hash, signature)` returns `true`. Both functions have exactly one return site (line 239 / 326), so a contrapositive proof "inner=false ⇒ outer=false" covers all paths. - -### 🟡 Kontrol partial — TypedDataSign branch (timed out, no CEX) - -- **Status**: 14 terminal SUCCESS branches + 12 subsumption covers in 102-node KCFG, NO counterexamples, full proof timed out at ~1h25m -- **File**: `test/kontrol/ERC1271NestedEIP712Kontrol.t.sol` -- **Config**: `kontrol.toml` (max-depth 5000, max-iter 200, workers 4) -- **Build wall time**: 73 s cold, ~50 s warm -- **Prove wall time at kill**: ~1h25m -- **Bound applied**: `vm.assume(signature.length <= 128)` -- **Classification**: Kontrol-limitation (SMT cost on symbolic-bytes calldata + 5+ calldatacopy operations whose offsets depend on `signature.length` and `c`). Not an impl bug. -- **Replayable variant**: not attempted — structurally identical body would consume the same budget. - -### ✅ Halmos partial — PersonalSign branch (PROVEN, both variants) - -- **Status**: 6/6 PASS (24.6 s total, ≤0.04 s aggregate solver time) -- **File**: `test/halmos/ERC1271NestedEIP712Halmos.t.sol` -- **Checks**: - - `check_NestedEIP712_Length0` — degenerate (signature.length == 0) - - `check_NestedEIP712_Length65_PersonalSignBranch` — ECDSA-canonical - - `check_NestedEIP712_Length100_PersonalSignBranch` — mid-sized - - `check_NestedEIP712Replayable_Length0` — same for Replayable variant - - `check_NestedEIP712Replayable_Length65_PersonalSignBranch` - - `check_NestedEIP712Replayable_Length100_PersonalSignBranch` -- **Technique**: pin trailing 2 bytes of `sig` to `0x00 0x00` so the EVM-level `c` is concrete `0`, forcing the PersonalSign workflow. Remaining bytes fully symbolic. -- **TypedDataSign not covered**: `Length67_TypedDataSignCandidate` and `Length100_TypedDataSignCandidate` attempted but hit `NotConcreteError: symbolic SHA3 data size`. The `contentsName` scan loop at `ERC1271.sol:206-219` computes the keccak input length `sub(add(p, c), m)` from symbolic byte-equality checks against `)` and `(`, which Halmos's keccak backend can't handle. - -### Combined Phase E story - -- **PersonalSign workflow**: ✅ PROVEN by Halmos (both standard + Replayable variants, three length classes). -- **TypedDataSign workflow**: 🟡 partial — Kontrol explored 14 SUCCESS branches without CEX before timeout; full closure requires either more wall-clock budget OR stronger Kontrol-side modeling of the calldata pattern. -- **No counterexamples found anywhere**: both backends would have surfaced a verifier-bypass; neither did. -- **Scaffold preserved**: Kontrol claim file + harness pattern on disk for future re-runs with a stronger machine or improved Kontrol SMT support. - -### Recommendation for Round 2 - -The TypedDataSign coverage gap is the only remaining FV gap for this property. Options: -- **Re-run Kontrol with larger budget** (4+ hours) on a beefier machine. -- **Certora attempt** with `optimistic_hashing` + careful summaries for the assembly memory writes (unclear if this works given the calldatacopy patterns). -- **Manual symbolic exec / pen-and-paper proof** of the structural claim (the single return site argument is straightforward to check by inspection). - -See `audit/FV_PLAN.md` for the full plan. diff --git a/audit/manual-proofs/property-15-erc1271-nested-eip712.md b/audit/manual-proofs/property-15-erc1271-nested-eip712.md deleted file mode 100644 index cec3da80..00000000 --- a/audit/manual-proofs/property-15-erc1271-nested-eip712.md +++ /dev/null @@ -1,532 +0,0 @@ ---- -date: 2026-05-23 -project: kernel-v4 -type: manual-proof -property-id: 15 -status: proven -contracts: [src/lib/ERC1271.sol] -backends-attempted: [kontrol, halmos] -backend-final: manual-cfg -reviewer: sc-critical-thinker -target_vault_path: ~/Documents/Obsidian/projects/kernel-v4/audits/manual-proofs/property-15-erc1271-nested-eip712.md ---- - -# Property #15 — Single-return-site CFG proof for `_erc1271IsValidSignatureViaNestedEIP712` - -## 1. Property statement - -Let `H` be the symbolic input `hash` of type `bytes32`, `S` the symbolic input -`signature` of type `bytes calldata`, and let -`V(h, s) = _erc1271IsValidSignatureNowCalldata(h, s)` denote the abstract inner -ERC-1271 verifier whose body is supplied by the inheriting contract. - -For every reachable `(H, S)`: - -> **P15-std**: `_erc1271IsValidSignatureViaNestedEIP712(H, S) = true` -> ⇒ there exist `h'` and `s'` derivable from `(H, S, address(this), eip712Domain())` -> such that `V(h', s') = true`. - -> **P15-rep**: `_erc1271IsValidSignatureViaNestedEIP712Replayable(H, S) = true` -> ⇒ there exist `h'` and `s'` derivable from `(H, S, address(this), eip712Domain())` -> such that `V(h', s') = true`. - -Both stated **contrapositively** (the form proved here, because it is the -single-statement form that covers every reachable path): - -> **¬P15-std**: `(∀ h', s') V(h', s') = false` -> ⇒ `_erc1271IsValidSignatureViaNestedEIP712(H, S) = false`. - -> **¬P15-rep**: `(∀ h', s') V(h', s') = false` -> ⇒ `_erc1271IsValidSignatureViaNestedEIP712Replayable(H, S) = false`. - -In plain English: the outer function authorises a signature **only when the -inner verifier authorises it**. The reconstruction logic (TypedDataSign vs -PersonalSign fallback vs corrupted-`d`) affects which `(h', s')` pair the -verifier is consulted on; it never bypasses the verifier. - -## 2. Why FV alone is insufficient (and what we proved with FV anyway) - -Two FV backends were attempted on the full property; both gave **partial** results. - -### 2.1 Halmos — PROVEN for PersonalSign, blocked on TypedDataSign - -`test/halmos/ERC1271NestedEIP712Halmos.t.sol` — 6/6 PASS in 24.6 s, ≤0.04 s -aggregate solver time. Covers: - -- Standard variant: signature lengths `{0, 65, 100}`, trailing 2 bytes pinned - to `0x00 0x00` to force the PersonalSign branch via `iszero(c)`. -- Replayable variant: same three lengths. - -The TypedDataSign branch is **not reachable** in Halmos. Attempted lengths -`67 (c=1)` and `100 (c=32)` hit -`NotConcreteError: symbolic SHA3 data size` because the `contentsName` scan -loop at `src/lib/ERC1271.sol:206-219` (and the mirror at `:293-306`) computes -the keccak input length `sub(add(p, c), m)` from symbolic byte-equality checks -against `)` and `(`. Halmos's keccak handler requires a syntactically concrete -size argument. - -### 2.2 Kontrol — partial (524 KCFG nodes, 0 CEX, no closure) - -`test/kontrol/ERC1271NestedEIP712Kontrol.t.sol` — Round 1: 102 nodes, 14 -SUCCESS terminals, 12 covers, killed at ~1h25m. Round 2: 524 nodes, 306 edges, -108 splits, 88 covers, 90 SUCCESS terminals, 21 frontier nodes still pending, -killed at `--max-iterations 500`. Total wall-time invested across both rounds: -~14 h 15 m. - -**Zero counterexamples** across the entire 524-node exploration. The blocker -is not soundness — it is SMT cost: the calldatacopy at `:202` uses an offset -`add(o, 0x40)` where `o = add(signature.offset, sub(signature.length, l))` -with `l = add(0x42, c)` and `c` derived from the trailing two bytes; the -contentsName scan adds another 5+ calldata-dependent reads. KEVM's symbolic -calldata handler creates an exponential branching tree in -`signature.length × c`. - -### 2.3 The remaining gap - -The TypedDataSign branch on both variants. That gap is exactly what this -manual CFG proof closes. - -## 3. CFG analysis — standard variant - -File: `src/lib/ERC1271.sol:155-240`. - -### 3.1 Basic-block decomposition - -Numbering follows the source line ranges. Each block ends at the first -control-flow instruction (branch, loop entry, `break`, fallthrough into a -join point) or at the function exit. - -| BB | Lines | Contents (summary) | -|-----|----------|--------------------| -| BB1 | 161-177 | Solidity prelude: `t := address(this)`; if non-zero, populate the upper half of the typehash buffer at `mload(0x40)` from `eip712Domain()` and re-allocate. | -| BB2 | 179-182 | Enter outer assembly block. Cache `m := mload(0x40)`. Decode `c` = trailing 2 bytes of `signature`. Loop header `for {} 1 {}` (Yul condition `1` ≡ `while(true)`). | -| BB3 | 183-191 | Loop body entry. Compute `l, o`. Store `\x19\x01` prefix at 0x00. `calldatacopy(0x20, o, 0x40)`. Compute the branch predicate at `:191` — `xor(keccak256(0x1e, 0x42), hash) ∨ lt(signature.length, l) ∨ iszero(c)`. | -| BB4 | 192-197 | **PersonalSign branch.** `t := 0`; build `PersonalSign(prefixed=hash)` struct hash; `hash := keccak256(t, 0x40)`; `break`. | -| BB5 | 200-213 | **TypedDataSign branch part A.** Build `TypedDataSign(` typehash skeleton at `m`. Copy `contentsName` optimistically. If the last copied byte is not `)`, enter the explicit-mode scan at `:206-209` (nested for-loop; itself a sub-CFG, but its only exits are `break` to the enclosing block — does NOT exit BB5's enclosing loop). Truncate `c`, re-copy `contentsName`, place opening `(`. | -| BB6 | 214-219 | **TypedDataSign branch part B.** Compute `d` (contentsName validity flag). Advance `p` past the prefix until `(` is found. | -| BB7 | 220-234 | **TypedDataSign branch part C.** Write the trailing typehash string. Copy `contentsType` after the typehash. Build `typedDataSignTypehash` at `t`. Compute the final `hash := keccak256(0x1e, add(0x42, and(1, d)))` (corrupted iff `d & 1 == 1`). Truncate `signature.length := signature.length - l`. `break`. | -| BB8 | 236-237 | **Loop exit join.** `mstore(0x40, m)` restores the free memory pointer. End of outer assembly block. | -| BB9 | 238-239 | **Return tail.** If `t == 0` (PersonalSign branch ran), call `hash = _hashTypedData(hash)`. Then assign `result = V(hash, signature)`. Function returns (implicit `return result` via the named return variable). | - -### 3.2 Control-flow graph - -``` - ┌──────────────┐ - │ ENTRY │ - └──────┬───────┘ - │ - ▼ - ┌──────────────┐ - │ BB1 prelude │ (161-177) - └──────┬───────┘ - │ - ▼ - ┌──────────────┐ - │ BB2 cache+ │ (179-182) - │ loop hdr │ - └──────┬───────┘ - │ - ▼ - ┌──────────────┐ - │ BB3 predicate│ (183-191) - └──┬────────┬──┘ - :191 T │ │ :191 F - │ │ - ▼ ▼ - ┌─────────┐ ┌─────────┐ - │ BB4 │ │ BB5 A │ (200-213) - │ PSign │ │ TDSign │ - │ branch │ └────┬────┘ - │ + break │ │ - └────┬────┘ ▼ - │ ┌─────────┐ - │ │ BB6 B │ (214-219) - │ └────┬────┘ - │ ▼ - │ ┌─────────┐ - │ │ BB7 C │ (220-234) - │ │ + break │ - │ └────┬────┘ - │ │ - └────────────┤ - ▼ - ┌──────────────┐ - │ BB8 restore │ (236-237) - └──────┬───────┘ - │ - ▼ - ┌──────────────┐ - │ BB9 return │ (238-239) - │ result = │ - │ V(h', s') │ - └──────┬───────┘ - │ - ▼ - EXIT -``` - -### 3.3 Inventory of `return`, `break`, and assembly-level exits - -Inside the entire function body (lines 161-239) the following control-flow -keywords appear: - -- `return` — **zero occurrences.** The function has a named return variable - `result` (declared at `:159`); Solidity emits the implicit `return result` - at the closing brace `:240`. There is **no early `return true`** anywhere - in the function, including inside both assembly blocks. -- `break` — two occurrences: - - `:196` — inside BB4, exits the `for {} 1 {}` outer loop (BB2/BB3 header). - - `:234` — inside BB7, exits the same outer loop. - - A third `break` at `:208` is inside the **nested** for-loop within BB5 - (the contentsName backward scan); per Yul semantics, `break` exits the - *innermost enclosing for-loop*, so this `break` exits the inner scan - and falls through to `:210`, not out of BB5. -- `revert`, `invalid`, `selfdestruct`, `stop`, `return(...)` (Yul) — **zero - occurrences** in either assembly block. - -### 3.4 The single-return-site lemma - -**Lemma 3.4 (standard variant)**. Every execution of -`_erc1271IsValidSignatureViaNestedEIP712(H, S)` that does not revert reaches -`:239` exactly once, and the function's return value equals the value of -`result` assigned at `:239`. - -*Proof.* - -1. **BB1 has a single outgoing edge** to BB2 (the `if (t != uint256(0))` at - `:163` is two-armed but both arms join at `:178`; the assembly block at - `:167-176` contains only `mload`/`mstore`/`keccak256` ops, none of which - alter control flow). - -2. **BB2 has a single outgoing edge** to BB3 (the for-loop header `for {} 1 {}` - in Yul is equivalent to `while(true)`; on each iteration its body runs - unconditionally). - -3. **BB3 has exactly two outgoing edges**, induced by the `if` at `:191`: - - When the predicate is true → BB4. - - When the predicate is false → BB5. - -4. **BB4 ends with `break` at `:196`.** Per Yul semantics, `break` exits the - innermost enclosing for-loop, which is the outer `for {} 1 {}` at `:183`. - Control flow therefore transfers to the **statement immediately following - the for-loop**, which is `mstore(0x40, m)` at `:236` — i.e. the entry of - BB8. - -5. **BB5 has internal structure** (a nested `if iszero(eq(...))` at `:204` - containing a nested for-loop at `:206`), but every internal branch - converges at the end of `:213` and falls through to BB6. - -6. **BB6** is a `for {} iszero(...) { p := add(p, 1) }` at `:217`; its loop - condition is `iszero(eq(byte(0, mload(p)), 40))`. The loop terminates - when `mload(p)` first equals `'('` (`= 0x28 = 40`). It has no `break` or - `return`, only the implicit "condition false → exit" edge to BB7. - -7. **BB7 ends with `break` at `:234`.** Same reasoning as BB4 — control - flow transfers to BB8 at `:236`. - -8. **BB8** has a single outgoing edge to BB9 (the closing `}` of the assembly - block at `:237` falls through to `:238`). - -9. **BB9** assigns `result = V(hash, signature)` at `:239` and falls through - to the function's closing brace at `:240`, which is the implicit return. - -By cases 1-8, every non-reverting path enters BB9. By case 9, every entry -into BB9 ends at `:239`. ∎ - -### 3.5 Path enumeration - -The CFG has exactly **two end-to-end paths** through the function body -(modulo the nested loop iterations in BB5/BB6 which do not change the -function's return value): - -- **Path P** (PersonalSign): BB1 → BB2 → BB3 → BB4 → BB8 → BB9. - Final `hash'` = `_hashTypedData(keccak256(PERSONAL_SIGN_TYPEHASH || H))` (the - re-hash at `:238`, applied because `t == 0` after BB4). - Final `signature'` = `S` (untruncated). - -- **Path T** (TypedDataSign): BB1 → BB2 → BB3 → BB5 → BB6 → BB7 → BB8 → BB9. - Final `hash'` = `keccak256(0x1e, 0x42 + (d & 1))` from `:232`. Note: when - `d & 1 == 1` (contentsName invalid) the hash is **deliberately corrupted** - by adding one extra byte to the keccak input. This is a feature, not a - bug — it ensures invalid contentsName cannot collide with a valid - TypedDataSign hash. - Final `signature'` = `S` truncated to drop the trailing - `(APP_DOMAIN_SEPARATOR || contents || contentsDescription || uint16)` - appendix (the `signature.length := signature.length - l` at `:233`). - -Both paths terminate at `:239` and assign `result = V(hash', signature')`. - -## 4. CFG analysis — Replayable variant - -File: `src/lib/ERC1271.sol:243-327`. - -### 4.1 Block-by-block diff against the standard variant - -The Replayable variant is a structural clone with three differences: - -| Std line(s) | Rep line(s) | Difference | -|-------------|-------------|------------| -| `:164` reads `chainId` | `:252` discards `chainId` (`/*chainId*/`) | One fewer struct field copied into the typehash buffer. | -| `:170-175` writes 6 words at `t+0x40..t+0xe0` | `:258-262` writes 5 words at `t+0x40..t+0xc0` | One fewer mstore; the layout is denser. | -| `:220-223` typehash string includes `uint256 chainId,` | `:307-310` typehash string omits `uint256 chainId,` | Different typehash for replayability across chains. | -| `:230` final `keccak256(t, 0xe0)` | `:317` final `keccak256(t, 0xc0)` | Smaller hashed region matching the smaller struct. | -| `:239` calls inner verifier | `:326` calls inner verifier | **Identical call shape**. | - -The control-flow keywords are **identical** in count and position: - -- zero `return` keywords inside either assembly block -- two `break` keywords (`:283` and `:321`) at the same relative positions as - the standard variant's `:196` and `:234` -- one nested `break` at `:295` (the contentsName scan), structurally identical - to the standard's `:208` - -### 4.2 The single-return-site lemma — Replayable - -**Lemma 4.2 (Replayable variant)**. Every execution of -`_erc1271IsValidSignatureViaNestedEIP712Replayable(H, S)` that does not -revert reaches `:326` exactly once, and the function's return value equals -the value of `result` assigned at `:326`. - -*Proof.* Identical structural proof to Lemma 3.4 with the line-number -substitutions above. The basic-block decomposition is isomorphic: - -- BB1' = `:249-264` (analogous to BB1) -- BB2' = `:266-269` (analogous to BB2) -- BB3' = `:270-278` (analogous to BB3) -- BB4' = `:279-284` (analogous to BB4; `break` at `:283`) -- BB5' = `:287-300` (analogous to BB5) -- BB6' = `:301-306` (analogous to BB6) -- BB7' = `:307-322` (analogous to BB7; `break` at `:321`) -- BB8' = `:323-324` (analogous to BB8; restores `mstore(0x40, m)`) -- BB9' = `:325-326` (analogous to BB9; single return site at `:326`) - -By the same case analysis, every non-reverting path enters BB9' and ends at -`:326`. ∎ - -## 5. Main theorem and proof - -**Theorem 5.1 (P15-std contrapositive)**. If `V(h', s') = false` for **every** -`(h', s')` derivable from `(H, S, address(this), eip712Domain())` along any -reachable path through `_erc1271IsValidSignatureViaNestedEIP712`, then the -function returns `false`. - -*Proof.* By Lemma 3.4, every non-reverting execution terminates at `:239` -with `result := V(hash, signature)` for some `hash, signature` whose values -are determined by the path taken (P or T) and the symbolic inputs `(H, S)` -plus the contract state `(address(this), eip712Domain())`. Call this pair -`(h', s')`. - -By hypothesis, `V(h', s') = false`. Therefore `result = false`. The function -returns `result`. ∎ - -**Theorem 5.2 (P15-rep contrapositive)**. Same statement, same proof, with -Lemma 4.2 in place of Lemma 3.4 and `:326` in place of `:239`. ∎ - -**Corollary 5.3** (the original P15 direction). If -`_erc1271IsValidSignatureViaNestedEIP712(H, S) = true`, then -`V(h', s') = true` for the specific `(h', s')` constructed by the path that -was actually taken. Same for the Replayable variant. *Proof: contrapositive -of Theorems 5.1 / 5.2.* ∎ - -## 6. Soundness gates - -Four assumptions must hold for the proof to be sound. Each is enumerated -below with the regression check that guards it. - -### 6.1 Gate G1 — no early `return` is added in future edits - -The proof hinges on `return` appearing exactly zero times in lines 161-239 -and 249-326 (excluding the implicit return at the closing brace). A future -PR that adds `return true` or `result = true; return result` inside the -assembly block would break the single-return-site argument silently. - -**Regression check**: a grep-style invariant added to the FV coverage gate -(Phase 4 of `audit/FV_PLAN_ROUND_2.md`): - -```bash -# Must produce exactly 0 lines. -awk '/function _erc1271IsValidSignatureViaNestedEIP712\(/,/^ }$/' \ - src/lib/ERC1271.sol | grep -E '^\s*(return|stop|invalid|selfdestruct)\b' -``` - -Suggested wording for inclusion in a forge-fmt-style or CI grep gate is in -§8.1 below. - -### 6.2 Gate G2 — `break` semantics in Yul - -The proof relies on Yul's specification of `break`: "Terminate the -innermost surrounding loop". From the Solidity reference: - -> The `break` statement can be used inside a loop. It causes the innermost -> enclosing loop to terminate. Execution continues with the next statement -> after the loop. - -In both functions, the outer loop at `:183` / `:270` is the innermost -loop containing the `break` at `:196` / `:283` and `:234` / `:321`. The -contentsName scan loops at `:206` / `:293` are the innermost loop for the -`break` at `:208` / `:295`, but those break out of the scan and fall -through to the truncate-and-recopy logic at `:210-212` / `:297-299`, which -is still inside BB5 / BB5'. There is no path where a `break` could escape -the function body skipping `:239` / `:326`. - -This is a property of the Solidity / Yul compiler, not of this codebase. -A break in the Yul specification would invalidate countless production -deployments before reaching Kernel v4. - -### 6.3 Gate G3 — soundness of `_erc1271IsValidSignatureNowCalldata` - -The proof reduces the security of the outer functions to the security of -the abstract inner verifier `V`. The proof itself does not claim that `V` -is sound — that claim is the obligation of the inheriting contract. - -In production Kernel v4, `V` is `_verifyFallbackSignature` for the 7702 -and immutable-ECDSA paths: - -- `Kernel7702._verifyFallbackSignature` — proven equivalent to - `ECDSA.tryRecoverCalldata(hash, sig) == owner()` by Phase A property #9 - (Halmos, `test/halmos/FallbackSignatureHalmos.t.sol`, 2/2 PASS). -- `KernelImmutableECDSA._verifyFallbackSignature` — same shape, also proven - by Phase A #9. - -For the permission and validator paths, `_erc1271IsValidSignature` (one -level above the nested-EIP712 entry points) routes through -`_verifySignaturePermission` / `_validateUserOpValidator`. Those are -covered by Phase D #11 (Certora, view/write equivalence) and Phase D #4 -(Certora, policy/signer failure ⇒ aggregate failure). - -So `V`'s soundness is independently established for every production -binding. The composition is: P15 ∧ Phase A #9 ∧ Phase D #4 ∧ Phase D #11 -⇒ the full ERC-1271 nested-EIP712 path on Kernel v4 admits a signature iff -the underlying ECDSA / policy chain admits it. - -### 6.4 Gate G4 — `eip712Domain()` and `_hashTypedData(...)` purity - -The proof treats `eip712Domain()` (BB1 / BB1') and `_hashTypedData(.)` -(BB9 / BB9') as opaque pure functions of `address(this)` and the contract -storage. Their soundness is the obligation of Solady's EIP-712 mixin, -which Kernel v4 imports unmodified from `solady/utils/EIP712.sol`. Solady -is itself audited (multiple third parties) and is the upstream of the -reference EIP-712 implementation used by major wallet clients. - -If Solady's `_hashTypedData` were to return a value that collided with a -PersonalSign typehash on a non-PersonalSign input, the post-processing at -`:238` / `:325` would no longer be the identity on PersonalSign inputs — -but that is a Solady bug, not a Kernel v4 bug, and would be caught by -upstream regression tests. - -## 7. Complementary FV evidence - -This manual proof is the audit-grade closure of property #15, but it is -not the only evidence. The full evidence chain: - -1. **Phase A #9** (Halmos, PROVEN, 2/2 — `test/halmos/FallbackSignatureHalmos.t.sol`) - — `_verifyFallbackSignature` on both `Kernel7702` and - `KernelImmutableECDSA` is bit-for-bit equivalent to - `ECDSA.tryRecoverCalldata(hash, sig) == expectedSigner`. This pins the - production `V` on the fallback path. - -2. **Phase E Halmos** (PROVEN, 6/6 — `test/halmos/ERC1271NestedEIP712Halmos.t.sol`) - — PersonalSign workflow proven for signature lengths `{0, 65, 100}` on - both the standard and Replayable variants. This is the concrete witness - that Path P in §3.5 (and its Replayable counterpart) does in fact - bottom out in `V` and does not return `true` when `V` returns `false`. - -3. **Phase E Kontrol partial** (no CEX, 90 SUCCESS terminals — `test/kontrol/ERC1271NestedEIP712Kontrol.t.sol`) - — exploratory evidence that no bypass exists in 524 KCFG nodes covering - both the PersonalSign and TypedDataSign branches with symbolic - signature lengths up to 96 bytes. The 21 still-pending frontier nodes - were under active exploration when the budget ran out; none had become - a CEX. - -4. **This manual proof** — the structural CFG argument that closes the - TypedDataSign branch unconditionally, for all signature lengths, on - both variants. - -The four pieces together cover: - -| Layer | Standard variant | Replayable variant | -|---|---|---| -| PersonalSign path | Halmos + manual CFG | Halmos + manual CFG | -| TypedDataSign path | Kontrol partial + manual CFG | Kontrol partial + manual CFG | -| Inner verifier `V` (production binding) | Phase A #9 (fallback), Phase D #4/#11 (permission) | same | - -## 8. Regression-protection recommendation - -The single-return-site argument is fragile under future edits. We propose -a defence-in-depth combination: - -### 8.1 CI grep gate (cheap, recommended) - -Add to `.github/workflows/foundry.yml` (or equivalent CI manifest): - -```yaml -- name: ERC1271 nested EIP-712 single-return-site invariant - run: | - set -e - # No `return`, `stop`, `invalid`, or `selfdestruct` keyword may appear - # inside the assembly block of either nested-EIP-712 function in - # src/lib/ERC1271.sol. The manual proof for property #15 - # (`audit/manual-proofs/property-15-erc1271-nested-eip712.md`) depends - # on this. If you intentionally introduced one of these keywords, - # you have invalidated the proof — re-run Kontrol on the property - # or extend the manual proof to cover the new exit path before - # merging. - awk '/function _erc1271IsValidSignatureViaNestedEIP712(Replayable)?\(/,/^ }$/' \ - src/lib/ERC1271.sol \ - | grep -nE '^\s*(return|stop|invalid|selfdestruct)\b' \ - && { echo "ERC1271 nested-EIP-712 single-return-site invariant violated"; exit 1; } \ - || true -``` - -This is a syntactic check; it will not catch a clever encoding (e.g. a -`pop(0)` followed by manipulating the free memory pointer to skip the -restore at BB8). But it catches the overwhelmingly common forms — direct -`return`, Yul `stop`, premature `invalid`. A reviewer can sanity-check -the diff for the cleverer cases. - -### 8.2 Per-PR Halmos run on the existing PersonalSign suite - -`forge clean && halmos --function check --contract ERC1271NestedEIP712Halmos` -on every PR touching `src/lib/ERC1271.sol`. Cold ~25 s, warm ~10 s. This -will not catch a TypedDataSign-only regression (Halmos cannot reach that -branch), but it pins the PersonalSign + return-tail logic in place. Any -edit that affects `_hashTypedData(hash)` at `:238` / `:325` or breaks the -final `V(hash, signature)` call would CEX immediately. - -### 8.3 Re-run Kontrol with a larger budget on releases - -Kontrol with `--max-iterations 2000` and 8 workers on a 64-GB-RAM machine -estimated to close the 21 remaining frontier nodes in 4-6 hours. Run -per-release (every `vX.Y.0` cut), not per-PR. - -## 9. Closing note for the auditor - -The function bodies of `_erc1271IsValidSignatureViaNestedEIP712` and its -Replayable variant are unusual: they consist of >70 lines of inline Yul -that manipulate symbolic-length calldata, compute multiple keccak hashes -over data whose layout depends on a 2-byte length field embedded at the -tail of the signature, and conditionally truncate the signature before -the final verifier call. This shape is hostile to all three FV backends -we have available, for three different reasons: - -- Halmos: keccak input length is computed from symbolic byte-equality - checks → `NotConcreteError`. -- Kontrol / KEVM: SMT cost is exponential in the symbolic signature - length × the trailing 2-byte length field → state-space blowup before - closure. -- Certora: assembly memory writes and calldatacopy patterns are at the - edge of what CVL summaries can model cleanly. - -The single-return-site CFG argument is the right hammer for this nail. -It reduces the security claim to a structural property of the function -body — one that is mechanically checkable by inspection of the source -file (and by the CI grep gate in §8.1) — and that hands off the actual -signature-verification obligation to `V`, which we have independently -proven by Phase A #9 / Phase D #4 / Phase D #11. - -The proof is rigorous within its stated assumptions (G1-G4 in §6); each -assumption is either guarded by a regression check or reduced to a -property of upstream tooling (Solidity compiler, Solady library) that -is independently audited. - -We consider property #15 **closed**. From 2291d994f1a6fe12d1b72c0addf97891cd602665 Mon Sep 17 00:00:00 2001 From: taek Date: Tue, 7 Jul 2026 13:33:52 +0900 Subject: [PATCH 2/2] docs: drop Security section linking to removed changelog --- README.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/README.md b/README.md index 24c6eba2..c43150a2 100644 --- a/README.md +++ b/README.md @@ -411,10 +411,6 @@ Key settings in `foundry.toml`: - **Optimizer**: 200 runs - **Invariant**: 1000 runs, 1000 depth -## Security - -See [CHANGELOG_AUDIT.md](./CHANGELOG_AUDIT.md) for the full audit changelog covering all changes since the last audit. - ## License MIT