From 703f890b3d0c38f3abbee0d431e965dee5946c68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Thu, 17 Jul 2025 17:00:50 +0200 Subject: [PATCH] Certora formal verification specifications and CI --- .github/workflows/certora-prover.yml | 116 +--- .github/workflows/certora.yml | 62 --- certora/confs/core/AllocationManager.conf | 97 ++-- .../core/AllocationManagerOverslashing.conf | 62 +++ .../confs/core/AllocationManagerSanity.conf | 4 +- .../core/AllocationManagerValidState.conf | 48 ++ certora/confs/core/DelegationManager.conf | 1 - .../core/DelegationManagerValidState.conf | 3 +- certora/confs/core/StrategyManager.conf | 7 +- .../multichain/BN254CertificateVerifier.conf | 24 + .../multichain/BaseConfForInheritance.conf | 30 ++ .../confs/multichain/CrossChainRegistry.conf | 44 ++ .../multichain/ECDSACertificateVerifier.conf | 22 + certora/confs/multichain/KeyRegistrar.conf | 34 ++ .../multichain/OperatorTableUpdater.conf | 27 + certora/confs/permissions/Pausable.conf | 1 - certora/confs/pods/EigenPodManagerRules.conf | 12 +- certora/confs/strategies/StrategyBase.conf | 4 +- .../harnesses/AllocationManagerHarness.sol | 35 ++ .../harnesses/CrossChainRegistryHarness.sol | 47 ++ certora/harnesses/KeyRegistrarHarness.sol | 25 + certora/harnesses/OperatorSetHelper.sol | 14 + .../harnesses/OperatorTableUpdaterHarness.sol | 50 ++ certora/harnesses/StrategyManagerHarness.sol | 3 +- certora/specs/Merkle.spec | 3 + .../specs/core/AllocationManagerRules.spec | 196 ++++++- .../core/AllocationManagerValidState.spec | 128 ++++- certora/specs/core/DelegationManager.spec | 1 - .../core/DelegationManagerValidState.spec | 1 - certora/specs/core/StrategyManager.spec | 36 +- certora/specs/libraries/BN254-nondet.spec | 24 + .../multichain/BN254CertificateVerifier.spec | 117 ++++ .../specs/multichain/CrossChainRegistry.spec | 502 ++++++++++++++++++ .../multichain/ECDSACertificateVerifier.spec | 101 ++++ certora/specs/multichain/EnumerableSet.spec | 54 ++ .../multichain/OperatorTableUpdater.spec | 224 ++++++++ certora/specs/permissions/KeyRegistrar.spec | 328 ++++++++++++ 37 files changed, 2244 insertions(+), 243 deletions(-) delete mode 100644 .github/workflows/certora.yml create mode 100644 certora/confs/core/AllocationManagerOverslashing.conf create mode 100644 certora/confs/core/AllocationManagerValidState.conf create mode 100644 certora/confs/multichain/BN254CertificateVerifier.conf create mode 100644 certora/confs/multichain/BaseConfForInheritance.conf create mode 100644 certora/confs/multichain/CrossChainRegistry.conf create mode 100644 certora/confs/multichain/ECDSACertificateVerifier.conf create mode 100644 certora/confs/multichain/KeyRegistrar.conf create mode 100644 certora/confs/multichain/OperatorTableUpdater.conf create mode 100644 certora/harnesses/AllocationManagerHarness.sol create mode 100644 certora/harnesses/CrossChainRegistryHarness.sol create mode 100644 certora/harnesses/KeyRegistrarHarness.sol create mode 100644 certora/harnesses/OperatorSetHelper.sol create mode 100644 certora/harnesses/OperatorTableUpdaterHarness.sol create mode 100644 certora/specs/Merkle.spec create mode 100644 certora/specs/libraries/BN254-nondet.spec create mode 100644 certora/specs/multichain/BN254CertificateVerifier.spec create mode 100644 certora/specs/multichain/CrossChainRegistry.spec create mode 100644 certora/specs/multichain/ECDSACertificateVerifier.spec create mode 100644 certora/specs/multichain/EnumerableSet.spec create mode 100644 certora/specs/multichain/OperatorTableUpdater.spec create mode 100644 certora/specs/permissions/KeyRegistrar.spec diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index 696a94b1cd..6d513c118b 100644 --- a/.github/workflows/certora-prover.yml +++ b/.github/workflows/certora-prover.yml @@ -6,37 +6,43 @@ on: types: [closed] branches: - main - + # Run on any pushes to certora/* branches push: branches: - 'certora/**' - + # Biweekly schedule (1st and 15th of each month at midnight UTC) schedule: - cron: '0 0 1,15 * *' - + # Manual trigger workflow_dispatch: jobs: - # First job: Compile the contracts for Certora verification - compile: - name: Compile + # Compile the contracts and run verification + compile_and_verify: + name: Compile and verify # Run if it meets one of these conditions: # 1. It's a merged PR from a feat/* branch to dev # 2. It's a push to a certora/* branch # 3. It's a scheduled run # 4. It's a manually triggered run if: > - (github.event_name == 'pull_request' && - github.event.pull_request.merged == true && - startsWith(github.head_ref, 'feat/')) || - (github.event_name == 'push' && + (github.event_name == 'pull_request' && + github.event.pull_request.merged == true && + startsWith(github.head_ref, 'feat/')) || + (github.event_name == 'push' && startsWith(github.ref, 'refs/heads/certora/')) || - github.event_name == 'schedule' || + github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' - runs-on: protocol-x64-16core + runs-on: ubuntu-latest +# runs-on: protocol-x64-16core + permissions: + contents: read + statuses: write + pull-requests: write + id-token: write steps: - uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911 with: @@ -49,82 +55,20 @@ jobs: # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }} - # Install the Foundry toolchain - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de - with: - version: stable - - # Install dependencies using Forge - - name: Install forge dependencies - run: forge install - - # Run Certora compilation step only - - uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc - with: - # List of configuration files for different contracts to verify - configurations: |- - certora/confs/core/AllocationManager.conf - certora/confs/core/AllocationManagerSanity.conf - certora/confs/core/DelegationManager.conf - certora/confs/core/DelegationManagerValidState.conf - certora/confs/core/StrategyManager.conf - certora/confs/permissions/Pausable.conf - certora/confs/pods/EigenPodManagerRules.conf - certora/confs/strategies/StrategyBase.conf - use-beta: true - solc-versions: 0.8.27 - solc-remove-version-prefix: "0." - job-name: "Eigenlayer Contracts" - certora-key: ${{ secrets.CERTORAKEY }} - # Only compile, don't run verification yet - compilation-steps-only: true - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - - # Second job: Run the actual verification after compilation succeeds - verify: - name: Verify - runs-on: protocol-x64-16core - # This job depends on the compile job - needs: compile - # Same conditions as the compile job - if: > - (github.event_name == 'pull_request' && - github.event.pull_request.merged == true && - startsWith(github.head_ref, 'feat/')) || - (github.event_name == 'push' && - startsWith(github.ref, 'refs/heads/certora/')) || - github.event_name == 'schedule' || - github.event_name == 'workflow_dispatch' - steps: - - uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911 - with: - egress-policy: audit - - # Checkout the repository with submodules - - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 - with: - submodules: recursive - # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow - ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }} - - # Install the Foundry toolchain. - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@82dee4ba654bd2146511f85f0d013af94670c4de - with: - version: stable - - # Install dependencies using Forge - - name: Install forge dependencies - run: forge install - - # Run Certora verification with the same configurations - - uses: Certora/certora-run-action@56c6a98e84eee5cd3a135967a9a4bc06ef6d38cc + # Run Certora compilation and verification + - name: Run Certora compilation and verification + uses: Certora/certora-run-action@11979c68d2ffab0b1b2fe6c72ec9d7a38855822d with: # List of configuration files for different contracts to verify configurations: |- + certora/confs/multichain/CrossChainRegistry.conf + certora/confs/multichain/KeyRegistrar.conf + certora/confs/multichain/OperatorTableUpdater.conf + certora/confs/multichain/ECDSACertificateVerifier.conf + certora/confs/multichain/BN254CertificateVerifier.conf certora/confs/core/AllocationManager.conf + certora/confs/core/AllocationManagerOverslashing.conf + certora/confs/core/AllocationManagerValidState.conf certora/confs/core/AllocationManagerSanity.conf certora/confs/core/DelegationManager.conf certora/confs/core/DelegationManagerValidState.conf @@ -132,10 +76,8 @@ jobs: certora/confs/permissions/Pausable.conf certora/confs/pods/EigenPodManagerRules.conf certora/confs/strategies/StrategyBase.conf - use-beta: true solc-versions: 0.8.27 - solc-remove-version-prefix: "0." - job-name: "Eigenlayer Contracts" + job-name: "Verified Rules" certora-key: ${{ secrets.CERTORAKEY }} env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml deleted file mode 100644 index f784e824d1..0000000000 --- a/.github/workflows/certora.yml +++ /dev/null @@ -1,62 +0,0 @@ -# name: Certora - -# on: -# workflow_dispatch: -# pull_request: -# branches: -# - dev -# push: -# branches: -# - dev -# - master -# - release-v* -# - formal-verification -# - m2-mainnet -# - testnet-holesky - -# jobs: -# certora: -# name: Test - -# runs-on: ubuntu-latest -# steps: - -# - uses: actions/checkout@v3 -# with: -# submodules: recursive - -# - name: Install Foundry -# uses: foundry-rs/foundry-toolchain@v1 -# with: -# version: stable - -# - name: Install forge dependencies -# run: forge install - -# - name: Install Python -# uses: actions/setup-python@v2 -# with: -# python-version: '3.10' -# cache: 'pip' - -# - name: Install Java -# uses: actions/setup-java@v2 -# with: -# distribution: temurin -# java-version: '17' - -# - name: Install Certora CLI -# run: pip install certora-cli - -# - name: Install Solidity Compiler -# run: | -# pip install solc-select -# solc-select use 0.8.27 --always-install - -# - name: Run Certora Verification -# run: | -# for script in $(ls certora/scripts/{,**}/*.sh | grep -v '\WnoCI\W'); do -# bash "$script" -# done -# env: -# CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/confs/core/AllocationManager.conf b/certora/confs/core/AllocationManager.conf index 3338a30598..1955b944d9 100644 --- a/certora/confs/core/AllocationManager.conf +++ b/certora/confs/core/AllocationManager.conf @@ -1,45 +1,56 @@ { - "assert_autofinder_success": true, - "files": [ - "src/contracts/core/AllocationManager.sol", - "src/contracts/permissions/PauserRegistry.sol", - "src/contracts/permissions/PermissionController.sol", - "src/contracts/core/DelegationManager.sol", - "src/contracts/pods/EigenPodManager.sol", - "src/contracts/core/StrategyManager.sol", - "src/contracts/strategies/StrategyBase.sol", - "certora/mocks/CertoraAVSRegistrar.sol", - "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", - "src/contracts/libraries/OperatorSetLib.sol" + "assert_autofinder_success": true, + // "build_cache": true, + "files": [ + "certora/harnesses/AllocationManagerHarness.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/strategies/StrategyBase.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", + "src/contracts/libraries/OperatorSetLib.sol", + "certora/harnesses/ShortStringsUpgradeableHarness.sol" + ], + "java_args": [], + "link": [ + "AllocationManagerHarness:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "AllocationManagerHarness:delegation=DelegationManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager" + ], + "loop_iter": "1", + "msg": "AllocationManager", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" + ], + "parametric_contracts": [ + "AllocationManagerHarness" + ], + "rule": [ + "pendingDiffStateTransitions", + "pendingDiffStateTransitionModifyAllocations", + "redistributionRecipientCannotBeDeadAddress" ], - "java_args": [ - ], - "link": [ - "AllocationManager:pauserRegistry=PauserRegistry", - "DelegationManager:permissionController=PermissionController", - "DelegationManager:allocationManager=AllocationManager", - "AllocationManager:permissionController=PermissionController", - "DelegationManager:strategyManager=StrategyManager", - "AllocationManager:delegation=DelegationManager", - "EigenPodManager:delegationManager=DelegationManager", - "DelegationManager:eigenPodManager=EigenPodManager" - ], - "loop_iter": "1", - "optimistic_fallback": true, - "optimistic_loop": true, - "packages": [ - "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", - "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" - ], - "parametric_contracts": [ - "AllocationManager" - ], - "process": "emv", - "prover_args": [ - " -recursionErrorAsAssert false -recursionEntryLimit 3" - ], - "solc": "solc8.27", - "solc_optimize": "1", - "verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec", - "server": "production", -} + "process": "emv", + "prover_args": [ + "-recursionErrorAsAssert false -recursionEntryLimit 3", + "-splitParallel true", + "-dontStopAtFirstSplitTimeout true" + ], + "rule_sanity": "basic", + "server": "production", + // "solc_via_ir": true, + "solc_optimize": "1", + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec", + "wait_for_results": "none" +} \ No newline at end of file diff --git a/certora/confs/core/AllocationManagerOverslashing.conf b/certora/confs/core/AllocationManagerOverslashing.conf new file mode 100644 index 0000000000..cbdb0cf30a --- /dev/null +++ b/certora/confs/core/AllocationManagerOverslashing.conf @@ -0,0 +1,62 @@ +{ + // "build_cache": true, + "files": [ + "certora/harnesses/AllocationManagerHarness.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/strategies/StrategyBase.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", + "src/contracts/libraries/OperatorSetLib.sol", + "certora/harnesses/ShortStringsUpgradeableHarness.sol" + ], + "java_args": [], + "link": [ + "AllocationManagerHarness:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "AllocationManagerHarness:delegation=DelegationManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager" + ], + "loop_iter": "1", + "msg": "AllocationManager No Overslashing", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" + ], + "parametric_contracts": [ + "AllocationManagerHarness" + ], + "rule": [ + "noOverslashingOfShares", + "noOverslashingOfOperatorShares", + "overslashingOfSharesAtMostOne", + ], + "process": "emv", + "prover_args": [ + "-recursionErrorAsAssert", + "false", + "-recursionEntryLimit", + "3", + "-dontStopAtFirstSplitTimeout", + "true", + "-split", + "false" + ], + "smt_timeout": "7200", + "rule_sanity": "basic", + "server": "production", + "solc_via_ir": true, + "solc_optimize": "1", + "disable_solc_optimizers": ["cse" , "peephole"], + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec", + "wait_for_results": "none" +} \ No newline at end of file diff --git a/certora/confs/core/AllocationManagerSanity.conf b/certora/confs/core/AllocationManagerSanity.conf index 7c46c258c9..68358d257e 100644 --- a/certora/confs/core/AllocationManagerSanity.conf +++ b/certora/confs/core/AllocationManagerSanity.conf @@ -12,8 +12,7 @@ "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", "src/contracts/libraries/OperatorSetLib.sol" ], - "java_args": [ - ], + "java_args": [], "link": [ "AllocationManager:pauserRegistry=PauserRegistry", "DelegationManager:permissionController=PermissionController", @@ -38,7 +37,6 @@ "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "AllocationManager:certora/specs/core/AllocationManagerSanity.spec" diff --git a/certora/confs/core/AllocationManagerValidState.conf b/certora/confs/core/AllocationManagerValidState.conf new file mode 100644 index 0000000000..093a90b2c7 --- /dev/null +++ b/certora/confs/core/AllocationManagerValidState.conf @@ -0,0 +1,48 @@ +{ + "files": [ + "certora/harnesses/AllocationManagerHarness.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/strategies/StrategyBase.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol", + "src/contracts/libraries/OperatorSetLib.sol", + "certora/harnesses/ShortStringsUpgradeableHarness.sol" + ], + "java_args": [], + "link": [ + "AllocationManagerHarness:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManagerHarness", + "AllocationManagerHarness:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "AllocationManagerHarness:delegation=DelegationManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager" + ], + "loop_iter": "1", + "msg": "AllocationManagerValidState", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0" + ], + "parametric_contracts": [ + "AllocationManagerHarness" + ], + "process": "emv", + "prover_args": [ + " -recursionErrorAsAssert false -recursionEntryLimit 3" + ], + "rule_sanity": "basic", + "server": "production", + "solc_optimize": "1", + "solc_via_ir": true, + // "build_cache": true, + "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerValidState.spec", + "wait_for_results": "none" +} \ No newline at end of file diff --git a/certora/confs/core/DelegationManager.conf b/certora/confs/core/DelegationManager.conf index 47d798e2e0..475560341f 100644 --- a/certora/confs/core/DelegationManager.conf +++ b/certora/confs/core/DelegationManager.conf @@ -43,7 +43,6 @@ ], "rule_sanity": "basic", "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "DelegationManagerHarness:certora/specs/core/DelegationManager.spec" diff --git a/certora/confs/core/DelegationManagerValidState.conf b/certora/confs/core/DelegationManagerValidState.conf index 2f3dfc081e..2e85c4efb2 100644 --- a/certora/confs/core/DelegationManagerValidState.conf +++ b/certora/confs/core/DelegationManagerValidState.conf @@ -34,9 +34,8 @@ "parametric_contracts": [ "DelegationManagerHarness" ], - "rule_sanity": "basic", + "rule_sanity": "basic", "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "DelegationManagerHarness:certora/specs/core/DelegationManagerValidState.spec" diff --git a/certora/confs/core/StrategyManager.conf b/certora/confs/core/StrategyManager.conf index f4902d46f8..56c06e6ce1 100644 --- a/certora/confs/core/StrategyManager.conf +++ b/certora/confs/core/StrategyManager.conf @@ -14,7 +14,8 @@ "link": [ "DelegationManager:allocationManager=AllocationManager", "DelegationManager:eigenPodManager=EigenPodManager", - "StrategyManagerHarness:delegation=DelegationManager" + "StrategyManagerHarness:delegation=DelegationManager", + "StrategyManagerHarness:allocationManager=AllocationManager", ], "loop_iter": "2", "optimistic_fallback": true, @@ -29,9 +30,9 @@ "StrategyManagerHarness" ], "process": "emv", - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "StrategyManagerHarness:certora/specs/core/StrategyManager.spec", - "rule_sanity": "basic" + "rule_sanity": "basic", + "server": "production" } diff --git a/certora/confs/multichain/BN254CertificateVerifier.conf b/certora/confs/multichain/BN254CertificateVerifier.conf new file mode 100644 index 0000000000..d7aff68d0e --- /dev/null +++ b/certora/confs/multichain/BN254CertificateVerifier.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "src/contracts/multichain/BN254CertificateVerifier.sol", + "src/contracts/multichain/OperatorTableUpdater.sol", + "certora/harnesses/OperatorSetHelper.sol" + ], + "link": [ + "BN254CertificateVerifier:operatorTableUpdater=OperatorTableUpdater" + ], + "msg": "BN254CertificateVerifier", + "verify": "BN254CertificateVerifier:certora/specs/multichain/BN254CertificateVerifier.spec", + "override_base_config": "certora/confs/multichain/BaseConfForInheritance.conf", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-allowArrayLengthUpdates true", + "-linearInvariantBound 4", + "-assumeFPStrictlyMonotonic false" + ], + "optimistic_hashing": true +} diff --git a/certora/confs/multichain/BaseConfForInheritance.conf b/certora/confs/multichain/BaseConfForInheritance.conf new file mode 100644 index 0000000000..03a9b12259 --- /dev/null +++ b/certora/confs/multichain/BaseConfForInheritance.conf @@ -0,0 +1,30 @@ +{ + "assert_autofinder_success": true, + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "solc": "solc", + "solc_optimize": "200", + "solc_via_ir": false, + "server": "production", + "packages": [ + "husky=node_modules/husky", + "@commitlint/cli=node_modules/@commitlint/cli", + "@commitlint/config-conventional=node_modules/@commitlint/config-conventional", + "forge-std=lib/forge-std/src", + "ds-test=lib/ds-test/src", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0", + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0", + "openzeppelin-contracts-upgradeable=lib/openzeppelin-contracts-upgradeable-v4.9.0" + ], + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-allowArrayLengthUpdates true", + "-linearInvariantBound 4" + ], + "build_cache": true +} diff --git a/certora/confs/multichain/CrossChainRegistry.conf b/certora/confs/multichain/CrossChainRegistry.conf new file mode 100644 index 0000000000..8d9d1dd74c --- /dev/null +++ b/certora/confs/multichain/CrossChainRegistry.conf @@ -0,0 +1,44 @@ +{ + "files": [ + "certora/harnesses/CrossChainRegistryHarness.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/core/AllocationManager.sol", + "src/contracts/permissions/KeyRegistrar.sol", + "src/contracts/permissions/PermissionController.sol", + "src/test/mocks/OperatorTableCalculatorMock.sol", + "certora/harnesses/OperatorSetHelper.sol" + ], + "link": [ + "CrossChainRegistryHarness:pauserRegistry=PauserRegistry", + "CrossChainRegistryHarness:allocationManager=AllocationManager", + "CrossChainRegistryHarness:keyRegistrar=KeyRegistrar", + "CrossChainRegistryHarness:permissionController=PermissionController" + ], + "msg": "CrossChainRegistry Rules", + "mutations": { + "gambit": [ + { + "filename": "src/contracts/multichain/CrossChainRegistryHarness.sol", + "num_mutants": 5 + } + ] + }, + "packages": [ + "husky=node_modules/husky", + "@commitlint/cli=node_modules/@commitlint/cli", + "@commitlint/config-conventional=node_modules/@commitlint/config-conventional", + "forge-std=lib/forge-std/src", + "ds-test=lib/ds-test/src", + "@openzeppelin=lib/openzeppelin-contracts-v4.9.0", + "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0" + ], + "parametric_contracts": [ + "CrossChainRegistryHarness" + ], + "optimistic_contract_recursion": true, + "contract_recursion_limit": "2", + "optimistic_summary_recursion": true, + "summary_recursion_limit": "2", + "verify": "CrossChainRegistryHarness:certora/specs/multichain/CrossChainRegistry.spec", + "override_base_config": "certora/confs/multichain/BaseConfForInheritance.conf" +} diff --git a/certora/confs/multichain/ECDSACertificateVerifier.conf b/certora/confs/multichain/ECDSACertificateVerifier.conf new file mode 100644 index 0000000000..1235c4910e --- /dev/null +++ b/certora/confs/multichain/ECDSACertificateVerifier.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/contracts/multichain/ECDSACertificateVerifier.sol", + "src/contracts/multichain/OperatorTableUpdater.sol", + "lib/openzeppelin-contracts-upgradeable-v4.9.0/contracts/mocks/ERC1271WalletMockUpgradeable.sol", + "certora/harnesses/OperatorSetHelper.sol" + ], + "link": [ + "ECDSACertificateVerifier:operatorTableUpdater=OperatorTableUpdater" + ], + "msg": "ECDSACertificateVerifier", + "mutations": { + "gambit": [ + { + "filename": "src/contracts/multichain/ECDSACertificateVerifier.sol", + "num_mutants": 5 + } + ] + }, + "verify": "ECDSACertificateVerifier:certora/specs/multichain/ECDSACertificateVerifier.spec", + "override_base_config": "certora/confs/multichain/BaseConfForInheritance.conf" +} diff --git a/certora/confs/multichain/KeyRegistrar.conf b/certora/confs/multichain/KeyRegistrar.conf new file mode 100644 index 0000000000..a7ed5ef537 --- /dev/null +++ b/certora/confs/multichain/KeyRegistrar.conf @@ -0,0 +1,34 @@ +{ + "files": [ + "certora/harnesses/KeyRegistrarHarness.sol", + "certora/mocks/CertoraAVSRegistrar.sol", + "src/contracts/core/AllocationManager.sol", + "src/contracts/core/DelegationManager.sol", + "src/contracts/permissions/PermissionController.sol", + "src/contracts/libraries/OperatorSetLib.sol", + "src/contracts/pods/EigenPodManager.sol", + "src/contracts/core/StrategyManager.sol", + "src/contracts/permissions/PauserRegistry.sol", + "src/contracts/strategies/StrategyBase.sol" + ], + "link": [ + "KeyRegistrarHarness:allocationManager=AllocationManager", + "KeyRegistrarHarness:permissionController=PermissionController", + "AllocationManager:delegation=DelegationManager", + "AllocationManager:pauserRegistry=PauserRegistry", + "DelegationManager:permissionController=PermissionController", + "DelegationManager:allocationManager=AllocationManager", + "AllocationManager:permissionController=PermissionController", + "DelegationManager:strategyManager=StrategyManager", + "EigenPodManager:delegationManager=DelegationManager", + "DelegationManager:eigenPodManager=EigenPodManager" + ], + "parametric_contracts": [ + "KeyRegistrarHarness" + ], + "msg": "KeyRegistrar", + "verify": "KeyRegistrarHarness:certora/specs/permissions/KeyRegistrar.spec", + "override_base_config": "certora/confs/multichain/BaseConfForInheritance.conf", + "optimistic_hashing": true, + "build_cache": true +} diff --git a/certora/confs/multichain/OperatorTableUpdater.conf b/certora/confs/multichain/OperatorTableUpdater.conf new file mode 100644 index 0000000000..f4ee53ac84 --- /dev/null +++ b/certora/confs/multichain/OperatorTableUpdater.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "src/contracts/multichain/BN254CertificateVerifier.sol", + "src/contracts/multichain/ECDSACertificateVerifier.sol", + "src/contracts/permissions/PauserRegistry.sol", + "certora/harnesses/OperatorTableUpdaterHarness.sol" + ], + "link": [ + "OperatorTableUpdaterHarness:bn254CertificateVerifier=BN254CertificateVerifier", + "OperatorTableUpdaterHarness:ecdsaCertificateVerifier=ECDSACertificateVerifier", + "OperatorTableUpdaterHarness:pauserRegistry=PauserRegistry", + "BN254CertificateVerifier:operatorTableUpdater=OperatorTableUpdaterHarness" + ], + "msg": "OperatorTableUpdater", + "verify": "OperatorTableUpdaterHarness:certora/specs/multichain/OperatorTableUpdater.spec", + "override_base_config": "certora/confs/multichain/BaseConfForInheritance.conf", + "prover_args": [ + "-verifyCache", + "-verifyTACDumps", + "-testMode", + "-checkRuleDigest", + "-callTraceHardFail on", + "-allowArrayLengthUpdates true", + "-linearInvariantBound 4" + ], + "optimistic_hashing": true +} diff --git a/certora/confs/permissions/Pausable.conf b/certora/confs/permissions/Pausable.conf index 384256e4ab..32adb2059e 100644 --- a/certora/confs/permissions/Pausable.conf +++ b/certora/confs/permissions/Pausable.conf @@ -13,7 +13,6 @@ "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "PausableHarness:certora/specs/permissions/Pausable.spec" diff --git a/certora/confs/pods/EigenPodManagerRules.conf b/certora/confs/pods/EigenPodManagerRules.conf index 269c2660f1..830c36d727 100644 --- a/certora/confs/pods/EigenPodManagerRules.conf +++ b/certora/confs/pods/EigenPodManagerRules.conf @@ -5,8 +5,6 @@ "summary_recursion_limit": "1", "optimistic_contract_recursion": true, "contract_recursion_limit": "1", -// "optimistic_hashing": true, -// "hashing_length_bound": "4700", "files": [ "src/contracts/pods/EigenPodManager.sol", "src/contracts/core/DelegationManager.sol", @@ -16,14 +14,9 @@ "src/contracts/permissions/PauserRegistry.sol", "src/contracts/pods/EigenPod.sol", "src/test/mocks/ETHDepositMock.sol:ETHPOSDepositMock", - "lib/openzeppelin-contracts-v4.9.0/contracts/utils/Create2.sol", -// -// "src/contracts/strategies/StrategyBase.sol", -// "certora/mocks/CertoraAVSRegistrar.sol", -// "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol" - ], - "java_args": [ + "lib/openzeppelin-contracts-v4.9.0/contracts/utils/Create2.sol" ], + "java_args": [], "link": [ "EigenPodManager:delegationManager=DelegationManager", "AllocationManager:pauserRegistry=PauserRegistry", @@ -48,7 +41,6 @@ "prover_args": [ " -recursionErrorAsAssert false -recursionEntryLimit 3" ], - "solc": "solc8.27", "solc_optimize": "1", "solc_via_ir": true, "verify": "EigenPodManager:certora/specs/pods/EigenPodManagerRules.spec", diff --git a/certora/confs/strategies/StrategyBase.conf b/certora/confs/strategies/StrategyBase.conf index 53eb14c4df..3706661ac7 100644 --- a/certora/confs/strategies/StrategyBase.conf +++ b/certora/confs/strategies/StrategyBase.conf @@ -19,9 +19,7 @@ "StrategyBase" ], "process": "emv", - "prover_args": [ - ], - "solc": "solc8.27", + "prover_args": [], "solc_optimize": "1", "solc_via_ir": true, "verify": "StrategyBase:certora/specs/strategies/StrategyBase.spec" diff --git a/certora/harnesses/AllocationManagerHarness.sol b/certora/harnesses/AllocationManagerHarness.sol new file mode 100644 index 0000000000..77628df3b5 --- /dev/null +++ b/certora/harnesses/AllocationManagerHarness.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "../../src/contracts/core/AllocationManager.sol"; +contract AllocationManagerHarness is AllocationManager { + constructor( + IDelegationManager _delegation, + IStrategy _eigenStrategy, + IPauserRegistry _pauserRegistry, + IPermissionController _permissionController, + uint32 _DEALLOCATION_DELAY, + uint32 _ALLOCATION_CONFIGURATION_DELAY, + string memory _version + ) AllocationManager( + _delegation, + _eigenStrategy, + _pauserRegistry, + _permissionController, + _DEALLOCATION_DELAY, + _ALLOCATION_CONFIGURATION_DELAY, + _version + ) {} + + function getOperatorKey(address avs, uint32 operatorSetId) external view returns (bytes32) { + return OperatorSetLib.key(OperatorSet(avs, operatorSetId)); + } + + function getOperatorSetFromKey(bytes32 key) external view returns (OperatorSet memory) { + return OperatorSetLib.decode(key); + } + + function getOperatorKeyFromSet(OperatorSet calldata os) external view returns (bytes32) { + return OperatorSetLib.key(os); + } +} \ No newline at end of file diff --git a/certora/harnesses/CrossChainRegistryHarness.sol b/certora/harnesses/CrossChainRegistryHarness.sol new file mode 100644 index 0000000000..48a5d0c397 --- /dev/null +++ b/certora/harnesses/CrossChainRegistryHarness.sol @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "../../src/contracts/multichain/CrossChainRegistry.sol"; + +/** + * @title CrossChainRegistryWrapper + * @notice Exposes internal checkCanCall logic as an external function + */ +contract CrossChainRegistryHarness is CrossChainRegistry { + + + /** + * @dev Constructor that passes required parameters to the CrossChainRegistry base constructor + * @param _allocationManager Address of the allocation manager contract + * @param _keyRegistrar Address of the key registrar contract + * @param _permissionController Address of the permission controller contract + * @param _pauserRegistry Address of the pauser registry contract + * @param _version Semantic version string + */ + constructor( + IAllocationManager _allocationManager, + IKeyRegistrar _keyRegistrar, + IPermissionController _permissionController, + IPauserRegistry _pauserRegistry, + string memory _version + ) + CrossChainRegistry( + _allocationManager, + _keyRegistrar, + _permissionController, + _pauserRegistry, + _version + ) + {} + + + /** + * @notice External function to check whether a given address can call privileged functions + * @param caller The address to check permissions for + */ + function canCall(address caller, address sender, uint32 selector) external returns (bool) { + + return permissionController.canCall(caller, sender, address(this), bytes4(selector)); + + } +} \ No newline at end of file diff --git a/certora/harnesses/KeyRegistrarHarness.sol b/certora/harnesses/KeyRegistrarHarness.sol new file mode 100644 index 0000000000..74a7f015d5 --- /dev/null +++ b/certora/harnesses/KeyRegistrarHarness.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "src/contracts/permissions/KeyRegistrar.sol"; + +contract KeyRegistrarHarness is KeyRegistrar { + using OperatorSetLib for OperatorSet; + constructor( + IPermissionController _permissionController, + IAllocationManager _allocationManager, + string memory _version + ) + KeyRegistrar(_permissionController, _allocationManager, _version) + {} + + /// @notice Returns the operatorSet key derived from avs and id + function getOperatorSetKey(OperatorSet calldata os) external pure returns (bytes32) { + return os.key(); // calls OperatorSetLib.key() + } + + + function getOperatorKeyDataHash(bytes32 key, address operator) external view returns (bytes32) { + return keccak256(_operatorKeyInfo[key][operator].keyData); + } +} \ No newline at end of file diff --git a/certora/harnesses/OperatorSetHelper.sol b/certora/harnesses/OperatorSetHelper.sol new file mode 100644 index 0000000000..fe3552ae2d --- /dev/null +++ b/certora/harnesses/OperatorSetHelper.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "src/contracts/libraries/OperatorSetLib.sol"; + +contract OperatorSetHelper { + using OperatorSetLib for OperatorSet; + constructor(){} + + /// @notice Returns the operatorSet key derived from avs and id + function getOperatorSetKey(OperatorSet calldata os) external pure returns (bytes32) { + return os.key(); // calls OperatorSetLib.key() + } +} \ No newline at end of file diff --git a/certora/harnesses/OperatorTableUpdaterHarness.sol b/certora/harnesses/OperatorTableUpdaterHarness.sol new file mode 100644 index 0000000000..f21a9c4f49 --- /dev/null +++ b/certora/harnesses/OperatorTableUpdaterHarness.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: BUSL-1.1 +pragma solidity ^0.8.27; + +import "src/contracts/multichain/OperatorTableUpdater.sol"; +import "src/contracts/interfaces/IKeyRegistrar.sol"; +import "src/contracts/interfaces/IBaseCertificateVerifier.sol"; + +contract OperatorTableUpdaterHarness is OperatorTableUpdater { + constructor( + IBN254CertificateVerifier _bn254CertificateVerifier, + IECDSACertificateVerifier _ecdsaCertificateVerifier, + IPauserRegistry _pauserRegistry, + string memory _version + ) OperatorTableUpdater( + _bn254CertificateVerifier, + _ecdsaCertificateVerifier, + _pauserRegistry, + _version + ) {} + + /// @notice Decodes operator table bytes and returns the latest reference timestamp + /// for the operator set in the corresponding certificate verifier. + function latestTsForOperatorTableBytes(bytes calldata operatorTableBytes) + external + view + returns (uint32) + { + (OperatorSet memory set, IKeyRegistrar.CurveType curve,,) = _decodeOperatorTableBytes(operatorTableBytes); + + return IBaseCertificateVerifier(getCertificateVerifier(curve)) + .latestReferenceTimestamp(set); + } + + + function isReferenceTimestampSet(bytes calldata operatorTableBytes, uint32 referenceTimestamp) external view returns (bool){ + + (OperatorSet memory set, IKeyRegistrar.CurveType curve,,) = _decodeOperatorTableBytes(operatorTableBytes); + + return IBaseCertificateVerifier(getCertificateVerifier(curve)) + .isReferenceTimestampSet(set, referenceTimestamp); + } + + function validCurvetype (bytes calldata operatorTableBytes) external view returns (bool){ + + (,IKeyRegistrar.CurveType curvetype,,) = _decodeOperatorTableBytes(operatorTableBytes); + + return curvetype == CurveType.BN254 || curvetype == CurveType.ECDSA; + } + +} \ No newline at end of file diff --git a/certora/harnesses/StrategyManagerHarness.sol b/certora/harnesses/StrategyManagerHarness.sol index 83b326906d..522a933566 100644 --- a/certora/harnesses/StrategyManagerHarness.sol +++ b/certora/harnesses/StrategyManagerHarness.sol @@ -5,10 +5,11 @@ import "../../src/contracts/core/StrategyManager.sol"; contract StrategyManagerHarness is StrategyManager { constructor( + IAllocationManager _allocationManager, IDelegationManager _delegation, IPauserRegistry _pauseRegistry, string memory _version - ) StrategyManager(_delegation, _pauseRegistry, _version) + ) StrategyManager(_allocationManager, _delegation, _pauseRegistry, _version) {} function strategy_is_in_stakers_array(address staker, IStrategy strategy) public view returns (bool) { diff --git a/certora/specs/Merkle.spec b/certora/specs/Merkle.spec new file mode 100644 index 0000000000..183e404c22 --- /dev/null +++ b/certora/specs/Merkle.spec @@ -0,0 +1,3 @@ +methods { + function Merkle._ external => NONDET; +} \ No newline at end of file diff --git a/certora/specs/core/AllocationManagerRules.spec b/certora/specs/core/AllocationManagerRules.spec index ba4acd6e87..96cac3a061 100644 --- a/certora/specs/core/AllocationManagerRules.spec +++ b/certora/specs/core/AllocationManagerRules.spec @@ -1,17 +1,7 @@ import "./AllocationManagerValidState.spec"; +using DelegationManager as DelegationManager; -use invariant maxMagnitudeHistoryKeysMonotonicInc; -use invariant maxMagnitudeHistoryKeysLessThanCurrentBlock; -use invariant maxMagnitudeMonotonicallyDecreasing; -use invariant SetInRegisteredIFFStatusIsTrue; -use invariant encumberedMagnitudeEqSumOfCurrentMagnitudesAndPositivePending; -use invariant negativePendingDiffAtMostCurrentMagnitude; -use invariant deallocationQueueDataUniqueness; -use invariant noZeroKeyInDealocationQ; -use invariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne; -use invariant deallocationQueueEffectBlockAscesndingOrder; -use invariant noPositivePendingDiffInDeallocationQ; -use invariant effectBlockZeroHasNoPendingDiff; +definition DEFAULT_BURN_ADDRESS() returns address = 0x00000000000000000000000000000000000E16E4; /* This rule applies to all methods except modifyAllocation because this function makes valid transitions, @@ -47,3 +37,185 @@ filtered {f -> f.selector == sig:modifyAllocations(address,IAllocationManagerTyp assert didMakeInvalidPendingDiffTransition == false; } + +/* +slashedMagnitude / currentMagnitudeBefore >= totalDepositSharesToSlash / (operatorSharesBefore + sharesInQueueBefore) +If this is false, it implies an AVS can “overslash” an operator, i.e. they can remove a larger percentage of funds. +We prove the mathematical equivalent: +slashedMagnitude * (totalShares + sharesInQueue) >= totalDepositSharesToSlash * currentMagnitude +*/ +rule noOverslashingOfOperatorShares(env e, address avs, IAllocationManagerTypes.SlashingParams params){ + + bytes32 operatorKey = getOperatorKey(avs, params.operatorSetId); + + // Assume some already proven invariants + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(params.operator, params.strategies[0]); + requireInvariant currentMagnitudeLeqWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant encumberedMagnitudeLeqWAD(e, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGEencumberedMagnitude(params.operator, params.strategies[0]); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGECurrentMagnitude(operatorKey, params.operator, params.strategies[0]); + + require (e.block.number < currentContract.allocations[params.operator][operatorKey][params.strategies[0]].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + // cannot allocate type IAllocationManagerTypes.Allocation in CVL directly but can access fields of primitive types + uint64 currentMagnitudeBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + int128 pendingDiffBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].pendingDiff; + require (pendingDiffBefore == 0, "prove an underapproximation assuming no pendingDiff, as pendingDiff changes currentMagnitude throughout the computation of slashOperator in _getUpdatedAllocation()"); + uint64 maxMagnitudeBefore = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesBefore = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesBefore = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + // Note: the totalDepositSharesToSlash usually also account for slashableSharesInQueue that have been removed + // Due to known rounding issues in the computation of DelegationManager.getSlashableSharesInQueue() + // we underapproximate and assume no slashableSharesInQueue but check no overslashing for operatorShares only + require queuedSharesBefore == 0; + require (operatorSharesBefore > 1, "1 share is an edge case that will always fail due to mulWadUp" ); + + slashOperator(e, avs, params); + + uint64 currentMagnitudeAfter = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + uint64 maxMagnitudeAfter = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesAfter = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + + // currentMagnitude should not increase from a slash + assert(currentMagnitudeBefore >= currentMagnitudeAfter); + // operatorShares should not increase from a slash + assert(operatorSharesBefore >= operatorSharesAfter); + + uint64 slashedMagnitude = require_uint64(currentMagnitudeBefore - currentMagnitudeAfter); + uint256 totalDepositSharesToSlash = require_uint256(operatorSharesBefore - operatorSharesAfter); + + // assert slashedMagnitude / currentMagnitude >= totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore); + assert slashedMagnitude != 0 => slashedMagnitude * operatorSharesBefore >= totalDepositSharesToSlash * currentMagnitudeBefore; +} + + +/* +slashedMagnitude / currentMagnitudeBefore >= totalDepositSharesToSlash / (operatorSharesBefore + sharesInQueueBefore) +If this is false, it implies an AVS can “overslash” an operator, i.e. they can remove a larger percentage of funds. +We prove the mathematical equivalent: +slashedMagnitude * (totalShares + sharesInQueue) >= totalDepositSharesToSlash * currentMagnitude +*/ +rule noOverslashingOfShares(env e, address avs, IAllocationManagerTypes.SlashingParams params){ + + bytes32 operatorKey = getOperatorKey(avs, params.operatorSetId); + + // Assume some already proven invariants + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(params.operator, params.strategies[0]); + requireInvariant currentMagnitudeLeqWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant encumberedMagnitudeLeqWAD(e, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGEencumberedMagnitude(params.operator, params.strategies[0]); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGECurrentMagnitude(operatorKey, params.operator, params.strategies[0]); + + require (e.block.number < currentContract.allocations[params.operator][operatorKey][params.strategies[0]].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + // cannot allocate type IAllocationManagerTypes.Allocation in CVL directly but can access fields of primitive types + uint64 currentMagnitudeBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + int128 pendingDiffBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].pendingDiff; + require (pendingDiffBefore == 0, "prove an underapproximation assuming no pendingDiff, as pendingDiff changes currentMagnitude throughout the computation of slashOperator in _getUpdatedAllocation()"); + uint64 maxMagnitudeBefore = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesBefore = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesBefore = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + // Note: the totalDepositSharesToSlash usually also account for slashableSharesInQueue that have been removed + // Due to known rounding issues in the computation of DelegationManager.getSlashableSharesInQueue() + // we underapproximate and assume no slashableSharesInQueue but check no overslashing for operatorShares only + require (operatorSharesBefore + queuedSharesBefore >= 1, "+" ); + + slashOperator(e, avs, params); + + uint64 currentMagnitudeAfter = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + uint64 maxMagnitudeAfter = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesAfter = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesAfter = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + + // currentMagnitude should not increase from a slash + assert(currentMagnitudeBefore >= currentMagnitudeAfter); + // operatorShares should not increase from a slash + assert(operatorSharesBefore >= operatorSharesAfter); + + uint64 slashedMagnitude = require_uint64(currentMagnitudeBefore - currentMagnitudeAfter); + uint256 totalDepositSharesToSlash = require_uint256(operatorSharesBefore - operatorSharesAfter + queuedSharesBefore - queuedSharesAfter); + + // assert slashedMagnitude / currentMagnitude >= totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore); + assert slashedMagnitude != 0 => assert_uint256(slashedMagnitude / currentMagnitudeBefore) >= assert_uint256(totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore)); +} + +/* +slashedMagnitude / currentMagnitudeBefore >= totalDepositSharesToSlash / (operatorSharesBefore + sharesInQueueBefore) +If this is false, it implies an AVS can “overslash” an operator, i.e. they can remove a larger percentage of funds. +We prove the mathematical equivalent: +slashedMagnitude * (totalShares + sharesInQueue) >= totalDepositSharesToSlash * currentMagnitude +*/ +rule overslashingOfSharesAtMostOne(env e, address avs, IAllocationManagerTypes.SlashingParams params){ + + bytes32 operatorKey = getOperatorKey(avs, params.operatorSetId); + + // Assume some already proven invariants + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(params.operator, params.strategies[0]); + requireInvariant currentMagnitudeLeqWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant encumberedMagnitudeLeqWAD(e, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGEencumberedMagnitude(params.operator, params.strategies[0]); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, params.operator, params.strategies[0]); + requireInvariant maxMagnitudeGECurrentMagnitude(operatorKey, params.operator, params.strategies[0]); + + require (e.block.number < currentContract.allocations[params.operator][operatorKey][params.strategies[0]].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + // cannot allocate type IAllocationManagerTypes.Allocation in CVL directly but can access fields of primitive types + uint64 currentMagnitudeBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + int128 pendingDiffBefore = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].pendingDiff; + require (pendingDiffBefore == 0, "prove an underapproximation assuming no pendingDiff, as pendingDiff changes currentMagnitude throughout the computation of slashOperator in _getUpdatedAllocation()"); + uint64 maxMagnitudeBefore = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesBefore = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesBefore = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + // Note: the totalDepositSharesToSlash usually also account for slashableSharesInQueue that have been removed + // Due to known rounding issues in the computation of DelegationManager.getSlashableSharesInQueue() + // we underapproximate and assume no slashableSharesInQueue but check no overslashing for operatorShares only + require (operatorSharesBefore + queuedSharesBefore >= 1, "+" ); + + slashOperator(e, avs, params); + + uint64 currentMagnitudeAfter = currentContract.allocations[params.operator][operatorKey][params.strategies[0]].currentMagnitude; + uint64 maxMagnitudeAfter = getMaxMagnitude(params.operator, params.strategies[0]); + + uint256 operatorSharesAfter = DelegationManager.operatorShares[params.operator][params.strategies[0]]; + uint256 queuedSharesAfter = DelegationManager.getSlashableSharesInQueue(e, params.operator, params.strategies[0]); + + // currentMagnitude should not increase from a slash + assert(currentMagnitudeBefore >= currentMagnitudeAfter); + // operatorShares should not increase from a slash + assert(operatorSharesBefore >= operatorSharesAfter); + + uint64 slashedMagnitude = require_uint64(currentMagnitudeBefore - currentMagnitudeAfter); + uint256 totalDepositSharesToSlash = require_uint256(operatorSharesBefore - operatorSharesAfter + queuedSharesBefore - queuedSharesAfter); + + // assert slashedMagnitude / currentMagnitude >= totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore); + assert slashedMagnitude != 0 => assert_uint256(slashedMagnitude / currentMagnitudeBefore) + 1 >= assert_uint256(totalDepositSharesToSlash / (operatorSharesBefore + queuedSharesBefore)); +} + + +/// @title redistributionRecipient should not be dead address after a successful run +rule redistributionRecipientCannotBeDeadAddress(AllocationManager.OperatorSet operatorSet) { + env e; + + IAllocationManagerTypes.CreateSetParams[] params; + require (params[0].operatorSetId == operatorSet.id, "assume we're setting the recipient for the fixed operatorSet"); + + address[] recipients; + createRedistributingOperatorSets(e, operatorSet.avs, params, recipients); + + address finalRecipient = getRedistributionRecipient(e, operatorSet); + + assert params.length != 0 => finalRecipient != DEFAULT_BURN_ADDRESS(); +} diff --git a/certora/specs/core/AllocationManagerValidState.spec b/certora/specs/core/AllocationManagerValidState.spec index 8ae63decc1..e665004f4f 100644 --- a/certora/specs/core/AllocationManagerValidState.spec +++ b/certora/specs/core/AllocationManagerValidState.spec @@ -1,7 +1,14 @@ import "../optimizations.spec"; +import "../ptaHelpers.spec"; + +using AllocationManagerHarness as AllocationManager; -using AllocationManager as AllocationManager; methods { + + //harnessed + function getOperatorKey(address, uint32) external returns (bytes32) envfree; + function getOperatorSetFromKey(bytes32) external returns (AllocationManagerHarness.OperatorSet) envfree; + function AllocationManager.DEALLOCATION_DELAY() external returns(uint32) envfree; function AllocationManager.getMaxMagnitude(address,address) external returns (uint64) envfree; @@ -24,6 +31,22 @@ methods { // function AllocationManager._addInt128(uint64 a, int128 b) internal returns (uint64) => cvlAddInt128(a, b); } +function requireNoOverflow(env e){ + requireInvariant maxMagnitudeHistoryKeysLessThanCurrentBlock(e); + requireInvariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); + // prevent overflows in deallocationQueue + require (forall address _operator. forall address _strategy. (currentContract.deallocationQueue[_operator][_strategy]._end < max_uint64 - 1), "reasonable length of deallocationQueue"); + // assuming deallocation block indices dont overflow + require (forall address _operator . forall address _strategy . (deallocationQueueEndGhost[_operator][_strategy] < max_uint64 - 1), "reasonable length of deallocationQueue"); + // would happen around the year 2833 to get block number equal to half of max_uint32 + require (e.block.number < max_uint32 + AllocationManager.DEALLOCATION_DELAY + 1, "reasonable block numbers"); + require (e.block.number > 0, "reasonable block numbers"); + // prevent overflows for loop iter = 2 + require (forall address operator_. forall address strategy_. maxMagnitudeHistoryLengths[operator_][strategy_] < max_uint256 - 1, "reasonable length of snapshots"); + require (forall address operator_. forall address strategy_. currentContract._maxMagnitudeHistory[operator_][strategy_]._snapshots.length < max_uint256 - 1, "reasonable length of snapshots"); + +} function cvlAddInt128(uint64 a, int128 b) returns uint64 { require(b >= 0 || to_mathint(a) > to_mathint(-b)); // Prevent underflow require(b <= 0 || a < to_mathint(max_uint64) -to_mathint(b)); // Prevent overflow @@ -617,7 +640,7 @@ invariant deallocationQueueDataUniqueness() // would happen around the year 2833 to get block number equal to half of max_uint32 require e.block.number < max_uint32 - AllocationManager.DEALLOCATION_DELAY - 1; require e.block.number > 0; - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); } } @@ -665,7 +688,7 @@ invariant deallocationQueueEffectBlocLessThanCurrBlockNumberPlushDelayPlusOne(en // assuming deallocation block indices dont overflow require forall address operator . forall address strategy . (deallocationQueueEndGhost[operator][strategy] < max_uint64 - 1); - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e1); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e1); } } @@ -676,7 +699,7 @@ except when an effect block is zero, which must have been less than or equal to This prevents out-of-order deallocations and ensures a valid execution sequence. */ /// @property Deallocation Queue Effect Block Ascending Order Invariant -invariant deallocationQueueEffectBlockAscesndingOrder(env e1) +invariant deallocationQueueEffectBlockAscendingOrder(env e1) forall address operator . forall address strategy . forall int128 index1 . forall int128 index2 . (index1 <= index2) && inBound(operator, strategy, index1) && inBound(operator, strategy, index2) => ((allocationsEffectBlock[operator][deallocationQueueDataGhost[operator][strategy][index1]][strategy] <= @@ -734,6 +757,101 @@ invariant noPositivePendingDiffInDeallocationQ() // would happen around the year 2833 to get block number equal to half of max_uint32 require e.block.number < max_uint32 - AllocationManager.DEALLOCATION_DELAY - 1; require e.block.number > 0; - requireInvariant deallocationQueueEffectBlockAscesndingOrder(e); + requireInvariant deallocationQueueEffectBlockAscendingOrder(e); + } + } + +invariant maxMagnitudeGECurrentMagnitude(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude <= getMaxMagnitude(operator, strategy) + { + preserved with (env e) { + requireValidState(); + SumTrackingSetup(); + requireNoOverflow(e); + // magnitudes cannot go beyond 1e18 + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant currentMagnitudeLeqWAD(operatorKey, operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); } + preserved slashOperator( + address avs2, + IAllocationManagerTypes.SlashingParams params + ) with (env e) { + bytes32 opKey = getOperatorKey(avs2, params.operatorSetId); + require (opKey == operatorKey, "need to ensure that the parameter opKey is the same operatorKey as used in the invariant"); + + requireValidState(); + SumTrackingSetup(); + requireNoOverflow(e); + // magnitudes cannot go beyond 1e18 + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant currentMagnitudeLeqWAD(operatorKey, operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + } } + +invariant maxMagnitudeLeqWAD(address operator, address strategy) + getMaxMagnitude(operator, strategy) <= WAD(); + +invariant currentMagnitudeLeqWAD(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude <= WAD() { + preserved with (env e) { + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + requireInvariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(operatorKey, operator, strategy); + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + } + } + +invariant encumberedMagnitudeLeqWAD(env e, address operator, address strategy) + getEncumberedMagnitude(e, operator, strategy) <= WAD() { + preserved { + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + } + } + +invariant sumOfPendingDiffCurrentMagnitudeRespectsWAD(bytes32 operatorKey, address operator, address strategy) + currentContract.allocations[operator][operatorKey][strategy].currentMagnitude + currentContract.allocations[operator][operatorKey][strategy].pendingDiff <= WAD() { + preserved with (env e) { + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + } + preserved modifyAllocations( + address op, + IAllocationManagerTypes.AllocateParams[] params + ) with (env e) { + // require (forall uint256 i. forall uint256 j. params[i].newMagnitudes[j] <= WAD(), "assume new magnitudes respect WAD()"); + + // AllocationManager.OperatorSet opSet = getOperatorSetFromKey(operatorKey); + // require (forall uint256 i. forall uint256 j. params[i].operatorSet.avs == opSet.avs => + // params[i].newMagnitudes[j] + currentContract.allocations[operator][operatorKey][strategy].pendingDiff <= WAD(), "assume new magnitude + current pending diff respect WAD()"); + + require (e.block.number < currentContract.allocations[operator][operatorKey][strategy].effectBlock, "require to not trigger a change of values throughout computation by _getUpdatedAllocation()"); + + SumTrackingSetup(); + requireValidState(); + requireNoOverflow(e); + requireInvariant maxMagnitudeLeqWAD(operator, strategy); + requireInvariant encumberedMagnitudeLeqWAD(e, operator, strategy); + requireInvariant maxMagnitudeGEencumberedMagnitude(operator, strategy); + } + } diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec index 4c8d3d7c0a..811913c677 100644 --- a/certora/specs/core/DelegationManager.spec +++ b/certora/specs/core/DelegationManager.spec @@ -57,7 +57,6 @@ methods { function isDelegated(address staker) external returns (bool) envfree; function isOperator(address operator) external returns (bool) envfree; function delegationApproverSaltIsSpent(address delegationApprover, bytes32 salt) external returns (bool) envfree; - function owner() external returns (address) envfree; function strategyManager() external returns (address) envfree; function eigenPodManager() external returns (address) envfree; function calculateWithdrawalRoot(IDelegationManagerTypes.Withdrawal) external returns (bytes32) envfree; diff --git a/certora/specs/core/DelegationManagerValidState.spec b/certora/specs/core/DelegationManagerValidState.spec index ec211e6b64..1fbd13ffb0 100644 --- a/certora/specs/core/DelegationManagerValidState.spec +++ b/certora/specs/core/DelegationManagerValidState.spec @@ -56,7 +56,6 @@ methods { function isDelegated(address staker) external returns (bool) envfree; function isOperator(address operator) external returns (bool) envfree; function delegationApproverSaltIsSpent(address delegationApprover, bytes32 salt) external returns (bool) envfree; - function owner() external returns (address) envfree; function strategyManager() external returns (address) envfree; function eigenPodManager() external returns (address) envfree; function calculateWithdrawalRoot(IDelegationManagerTypes.Withdrawal) external returns (bytes32) envfree; diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec index 88574489d7..c19bbe535c 100644 --- a/certora/specs/core/StrategyManager.spec +++ b/certora/specs/core/StrategyManager.spec @@ -89,8 +89,8 @@ invariant arrayExhibitsProperties(address staker) /** * a staker's amount of shares in a strategy (i.e. `stakerDepositShares[staker][strategy]`) should only increase when -* `depositIntoStrategy`, `depositIntoStrategyWithSignature`, or `depositBeaconChainETH` has been called -* *OR* when completing a withdrawal +* `depositIntoStrategy`, `depositIntoStrategyWithSignature`, +* `withdrawSharesAsTokens`, or `addShares` is called. */ definition methodCanIncreaseShares(method f) returns bool = f.selector == sig:depositIntoStrategy(address,address,uint256).selector @@ -100,7 +100,7 @@ definition methodCanIncreaseShares(method f) returns bool = /** * a staker's amount of shares in a strategy (i.e. `stakerDepositShares[staker][strategy]`) should only decrease when -* `queueWithdrawal`, `slashShares`, or `recordBeaconChainETHBalanceUpdate` has been called +`removeDepositShares` is called */ definition methodCanDecreaseShares(method f) returns bool = f.selector == sig:removeDepositShares(address,address,uint256).selector; @@ -117,10 +117,11 @@ rule sharesAmountsChangeOnlyWhenAppropriateFunctionsCalled(address staker, addre } /** -* Verifies that the `totalShares` returned by an Strategy increases appropriately when new Strategy shares are issued by the StrategyManager +* Verifies that the `totalShares` returned by a Strategy increases appropriately when new Strategy shares are issued by the StrategyManager * contract (specifically as a result of a call to `StrategyManager.depositIntoStrategy` or `StrategyManager.depositIntoStrategyWithSignature`). -* This rule excludes the `addShares` and `removeShares` functions, since these are called only by the DelegationManager, and do not +* This rule excludes the `addShares` function, since this is called only by the DelegationManager, and do not * "create new shares", but rather represent existing shares being "moved into a withdrawal". +* for the `addShares` case, we instead check that the totalShares value does not change as a result of the call */ rule newSharesIncreaseTotalShares(address strategy) { method f; @@ -129,7 +130,6 @@ rule newSharesIncreaseTotalShares(address strategy) { uint256 totalSharesBefore = totalShares(strategy); if ( f.selector == sig:addShares(address, address, uint256).selector -// || f.selector == sig:removeShares(address, address, uint256).selector ) { uint256 totalSharesAfter = totalShares(strategy); assert(totalSharesAfter == totalSharesBefore, "total shares changed unexpectedly"); @@ -181,9 +181,29 @@ rule safeApprovalUse(address user) { bytes signature; require balanceOfCVL(token, strategy) + amount <= max_uint256; // Require no overflows on balances as valid env assumption depositIntoStrategyWithSignature(e, strategy, token, amount, staker, expiry, signature); - } + } else if (f.selector == sig:clearBurnOrRedistributableSharesByStrategy(StrategyManager.OperatorSet,uint256,address).selector) { + StrategyManager.OperatorSet operatorSet; + uint256 slashId; + address strategy; + + // User is not the target strategy. + // (This withrdraws from that strategy) + require user != strategy; + + clearBurnOrRedistributableSharesByStrategy(e, operatorSet, slashId, strategy); + + } else if (f.selector == sig:clearBurnOrRedistributableShares(StrategyManager.OperatorSet,uint256).selector) { + StrategyManager.OperatorSet operatorSet; + uint256 slashId; + + // User is not one of the strategies. + // (This withrdraws from zero or more strategies) + require user != StrategyBase; + require user != currentContract; + + clearBurnOrRedistributableShares(e, operatorSet, slashId); // otherwise just perform an arbitrary function call - else { + } else { calldataarg args; f(e,args); } diff --git a/certora/specs/libraries/BN254-nondet.spec b/certora/specs/libraries/BN254-nondet.spec new file mode 100644 index 0000000000..2683f050e2 --- /dev/null +++ b/certora/specs/libraries/BN254-nondet.spec @@ -0,0 +1,24 @@ +methods { + // BN254 implements elliptic curve operations, let's NONDET all of them + function BN254.plus(BN254.G1Point memory a, BN254.G1Point memory b) internal returns (BN254.G1Point memory) => CVL_randomPoint(); + function BN254.pairing(BN254.G1Point memory a1, BN254.G2Point memory a2, BN254.G1Point memory b1, BN254.G2Point memory b2) internal returns (bool) => NONDET; + function BN254.safePairing(BN254.G1Point memory a, BN254.G2Point memory b, BN254.G1Point memory c, BN254.G2Point memory d, uint256) internal returns (bool,bool) => NONDET; + function BN254.scalar_mul(BN254.G1Point memory p, uint256 s) internal returns (BN254.G1Point memory) => CVL_randomPoint(); + + function BN254.expMod(uint256 b, uint256 e, uint256 m) internal returns (uint256) => CVL_expMod(b,e,m); + function BN254.hashToG1(bytes32 _x) internal returns (BN254.G1Point memory) => CVL_randomPoint(); +} + +function CVL_plus(BN254.G1Point a, BN254.G1Point b) returns BN254.G1Point { + BN254.G1Point res; + return res; +} + +function CVL_randomPoint() returns BN254.G1Point { + BN254.G1Point res; + return res; +} + +function CVL_expMod(uint256 b, uint256 e, uint256 m) returns uint256 { + return require_uint256((b^e) % m); +} \ No newline at end of file diff --git a/certora/specs/multichain/BN254CertificateVerifier.spec b/certora/specs/multichain/BN254CertificateVerifier.spec new file mode 100644 index 0000000000..480fb70f07 --- /dev/null +++ b/certora/specs/multichain/BN254CertificateVerifier.spec @@ -0,0 +1,117 @@ +import "../libraries/BN254-nondet.spec"; +using OperatorSetHelper as OperatorSetHelper; + +use builtin rule sanity filtered { f -> f.contract == currentContract } + +methods{ + function OperatorSetHelper.getOperatorSetKey(BN254CertificateVerifier.OperatorSet os) external returns (bytes32) envfree; +} + +/* + * msg.sender != address(operatorTableUpdater) => revert + * referenceTimestamp == 0 => revert + * + * What it means: Only the designated operatorTableUpdater address can call this function, all other callers must be rejected + * + * Why it should hold: The contract has a specific modifier 'onlyTableUpdater' and the function is critical for updating operator information. Unauthorized access could corrupt the operator registry + * + * Possible consequences: Unauthorized operator table manipulation, state corruption, denial of service by malicious actors updating operator information + */ +rule updateOperatorTable_revert_conditions(env e) { + BN254CertificateVerifier.OperatorSet operatorSet; + uint32 referenceTimestamp; + IOperatorTableCalculatorTypes.BN254OperatorSetInfo operatorSetInfo; + ICrossChainRegistryTypes.OperatorSetConfig operatorSetConfig; + + bool zeroRefTS = referenceTimestamp == 0; + // call function under test + updateOperatorTable@withrevert(e, operatorSet, referenceTimestamp, operatorSetInfo, operatorSetConfig); + bool updateOperatorTable_reverted = lastReverted; + + // verify integrity + assert ((e.msg.sender != currentContract.operatorTableUpdater || zeroRefTS) => updateOperatorTable_reverted), "msg.sender != address(operatorTableUpdater) => revert"; +} + + + + +rule updateOperatorTable_updates_latest_for_set_and_frames(env e) { + BN254CertificateVerifier.OperatorSet os; + uint32 ts; + IOperatorTableCalculatorTypes.BN254OperatorSetInfo info; + ICrossChainRegistryTypes.OperatorSetConfig cfg; + + // keys + bytes32 k = OperatorSetHelper.getOperatorSetKey(os); + BN254CertificateVerifier.OperatorSet otherOs; + bytes32 ok = OperatorSetHelper.getOperatorSetKey(otherOs); + + // snapshots + uint32 latest_before = currentContract._latestReferenceTimestamps[k]; + uint32 other_before = currentContract._latestReferenceTimestamps[ok]; + + // require minimal success preconditions you know the code enforces: + require e.msg.sender == currentContract.operatorTableUpdater; + require ts != 0; + // (If the implementation also checks ts <= block.timestamp, keep it below instead.) + + updateOperatorTable(e, os, ts, info, cfg); + + // effect on this set + assert currentContract._latestReferenceTimestamps[k] == ts; + assert currentContract._latestReferenceTimestamps[k] > latest_before; + + // frame: unrelated sets unchanged + assert (ok == k) || (currentContract._latestReferenceTimestamps[ok] == other_before); +} + + + + +/* + * !operatorTableUpdater.isRootValidByTimestamp(cert.referenceTimestamp) => revert + * + * What it means: The function must revert if the operator table updater indicates that the root corresponding to the reference timestamp is disabled or invalid + * + * Why it should hold: The contract explicitly checks this condition in _validateCertificateTimestamp() with 'require(operatorTableUpdater.isRootValidByTimestamp(referenceTimestamp), RootDisabled())'. This ensures certificates are only verified against valid, non-disabled operator sets. + * + * Possible consequences: Accepting certificates based on outdated or compromised operator sets, potential for replay attacks using disabled roots + */ +rule verifyCertificate_disabled_root(env e) { + BN254CertificateVerifier.OperatorSet operatorSet; + IBN254CertificateVerifierTypes.BN254Certificate cert; + uint256[] signedStakes; + + // call function under test + verifyCertificate@withrevert(e, operatorSet, cert); + bool verifyCertificate_reverted = lastReverted; + + // verify integrity + assert (!currentContract.operatorTableUpdater.isRootValidByTimestamp(e, cert.referenceTimestamp) => verifyCertificate_reverted), "!operatorTableUpdater.isRootValidByTimestamp(cert.referenceTimestamp) => revert"; +} + +/* + * !operatorTableUpdater.isRootValidByTimestamp(cert.referenceTimestamp) => revert + * * totalStakeNominalThresholds.length > 100 => revert + * What it means: The function must revert when the operator table updater indicates that the root for the given reference timestamp is disabled or invalid + * + * Why it should hold: This is a critical security check that ensures only valid, non-revoked operator sets can be used for verification. Disabled roots indicate compromised or outdated operator information + * + * Possible consequences: Security bypass allowing verification against compromised or revoked operator sets, potential fund loss or unauthorized operations + */ +rule verifyCertificateNominal_revert_conditions(env e) { + BN254CertificateVerifier.OperatorSet operatorSet; + IBN254CertificateVerifierTypes.BN254Certificate cert; + uint256[] totalStakeNominalThresholds; + bool result; + + bool disabledRoot = !currentContract.operatorTableUpdater.isRootValidByTimestamp(e, cert.referenceTimestamp); + bool maxThresholdPassed = totalStakeNominalThresholds.length > 100; + + // call function under test + verifyCertificateNominal@withrevert(e, operatorSet, cert, totalStakeNominalThresholds); + bool verifyCertificateNominal_reverted = lastReverted; + + // verify integrity + assert ((disabledRoot || maxThresholdPassed) => verifyCertificateNominal_reverted), "!operatorTableUpdater.isRootValidByTimestamp(cert.referenceTimestamp) => revert"; +} diff --git a/certora/specs/multichain/CrossChainRegistry.spec b/certora/specs/multichain/CrossChainRegistry.spec new file mode 100644 index 0000000000..53b10744bf --- /dev/null +++ b/certora/specs/multichain/CrossChainRegistry.spec @@ -0,0 +1,502 @@ +import "./EnumerableSet.spec"; +using OperatorSetHelper as OperatorSetHelper; + +use builtin rule sanity filtered { f -> f.contract == currentContract } + +use invariant _activeGenerationReservationsInvariant; + +methods { + function _.calculateOperatorTableBytes(CrossChainRegistry.OperatorSet) external => DISPATCHER(true); + function OperatorSetHelper.getOperatorSetKey(CrossChainRegistry.OperatorSet os) external returns (bytes32) envfree; +} + +// // There must not be two active reservations for the same OperatorSet.key() +invariant activeGenerationReservationUniqueness(bytes32 key1, bytes32 key2, uint256 i1, uint256 i2) + (key1 != key2 && ghostIndexes_activeGenerationReservations[key1] != 0 && ghostIndexes_activeGenerationReservations[key2] != 0) => + (ghostIndexes_activeGenerationReservations[key1] != ghostIndexes_activeGenerationReservations[key2] + && ghostValues_activeGenerationReservations[ghostIndexes_activeGenerationReservations[key1]-1] != ghostValues_activeGenerationReservations[ghostIndexes_activeGenerationReservations[key2]-1]) + { + preserved{ + requireInvariant _activeGenerationReservationsInvariant(); + } + } + +// valid state changes +rule onlyValidSenderCanChangeState(env e, method f, calldataarg args) +filtered{f -> !f.isView} { + CrossChainRegistry.OperatorSet os; + bytes32 key = OperatorSetHelper.getOperatorSetKey(os); + requireInvariant _activeGenerationReservationsInvariant(); + uint256 i; + + mathint _activeGenerationReservationsIndexPre = ghostIndexes_activeGenerationReservations[key]; + bytes32 _activeGenerationReservationsValuePre = ghostValues_activeGenerationReservations[i]; + uint256 _activeGenerationReservationsLengthPre = ghostLength_activeGenerationReservations; + + address configPreOwner = currentContract._operatorSetConfigs[key].owner; + uint32 configPreMaxStalenessPeriod = currentContract._operatorSetConfigs[key].maxStalenessPeriod; + address tableCalculatorPre = currentContract._operatorTableCalculators[key]; + + bool canCall = canCall(e, os.avs, e.msg.sender, f.selector); + + if(f.selector == sig:createGenerationReservation(CrossChainRegistry.OperatorSet, address, ICrossChainRegistryTypes.OperatorSetConfig).selector){ + ICrossChainRegistryTypes.OperatorSetConfig config; + createGenerationReservation(e, os, tableCalculatorPre, config); + } else if (f.selector == sig:removeGenerationReservation(CrossChainRegistry.OperatorSet).selector){ + removeGenerationReservation(e, os); + } else { + f(e, args); + } + + // no state change in _activeGenerationReservations + assert ghostValues_activeGenerationReservations[i] == _activeGenerationReservationsValuePre || canCall; + assert ghostIndexes_activeGenerationReservations[key] == _activeGenerationReservationsIndexPre || canCall; + assert ghostLength_activeGenerationReservations == _activeGenerationReservationsLengthPre || canCall; + + // no state change in _operatorSetConfigs + assert configPreOwner == currentContract._operatorSetConfigs[key].owner || canCall; + assert configPreMaxStalenessPeriod == currentContract._operatorSetConfigs[key].maxStalenessPeriod || canCall; + + // no state change in _operatorTableCalculators + assert tableCalculatorPre == currentContract._operatorTableCalculators[key] || canCall; + +} + +/* + * _paused@before == _paused@after + * + * What it means: The function must not modify the pause state stored in the _paused state variable + * + * Why it should hold: createGenerationReservation is not a pause management function and should only affect operator set reservations. Only authorized pausers should be able to modify the pause state + * + * Possible consequences: If this property is violated, an attacker could unpause the contract or change pause states through a function that should only create reservations, bypassing pause controls + */ +rule no_illegal_change_to_paused(env e, method f, calldataarg args) filtered{f -> !f.isView}{ + + // assign all the 'before' variables + uint256 _paused_before = currentContract._paused; + + // call function under test + f(e, args); + + // assign all the 'after' variables + uint256 _paused_after = currentContract._paused; + + // verify integrity + assert (_paused_before == _paused_after || + f.selector == sig:initialize(address, uint32, uint256).selector || + f.selector == sig:pauseAll().selector || + f.selector == sig:pause(uint256).selector || + f.selector == sig:unpause(uint256).selector + ), "_paused@before == _paused@after"; +} + +/* + * _initialized@after == _initialized@before + * + * What it means: The function must not change the initialization state flag + * + * Why it should hold: Only initialization functions should modify this flag, not chain whitelist operations + * + * Possible consequences: Reinitialization vulnerabilities, bypassing initialization checks, state corruption + */ +rule no_illegal_change_initialized(env e, method f, calldataarg args) { + // assign all the 'before' variables + uint8 _initialized_before = currentContract._initialized; + + // call function under test + f(e, args); + + // assign all the 'after' variables + uint8 _initialized_after = currentContract._initialized; + + // verify integrity + assert (_initialized_after == _initialized_before || + f.selector == sig:initialize(address, uint32, uint256).selector + ), "_initialized@after == _initialized@before"; +} + +/* + * _initialized@after == _initialized@before + * + * What it means: The function must not change the initialization state flag + * + * Why it should hold: Only initialization functions should modify this flag, not chain whitelist operations + * + * Possible consequences: Reinitialization vulnerabilities, bypassing initialization checks, state corruption + */ +rule no_illegal_change_initializing(env e, method f, calldataarg args) { + // assign all the 'before' variables + bool _initializing_before = currentContract._initializing; + + // call function under test + f(e, args); + + // assign all the 'after' variables + bool _initializing_after = currentContract._initializing; + + // verify integrity + assert (_initializing_after == _initializing_before), "_initialized@after == _initialized@before"; +} + +/* + * _owner@after == _owner@before + * + * What it means: The contract owner address stored in _owner should remain the same before and after the function execution + * + * Why it should hold: The setOperatorSetConfig function is not designed to change ownership and has no ownership transfer logic. Any change to the owner during this function would indicate unauthorized privilege escalation or a serious bug + * + * Possible consequences: If ownership changes unexpectedly, it could lead to complete loss of administrative control, unauthorized access to owner-only functions, or transfer of control to malicious actors + */ +rule no_illegal_change_to_owner(env e, method f, calldataarg args) { + // assign all the 'before' variables + address _owner_before = currentContract._owner; + + // call function under test + f(e, args); + + // assign all the 'after' variables + address _owner_after = currentContract._owner; + + // verify integrity + assert (_owner_after == _owner_before || + f.selector == sig:initialize(address, uint32, uint256).selector || + f.selector == sig:renounceOwnership().selector || + f.selector == sig:transferOwnership(address).selector + ), "_owner@after == _owner@before"; +} + +/* + * _initialized != 0 => revert + * + * What it means: The initialize function must revert if the contract has already been initialized (when _initialized is not 0) + * + * Why it should hold: This is a critical security property of the Initializable pattern from OpenZeppelin. The initialize function should only be callable once to prevent reinitialization attacks that could reset critical state variables like ownership + * + * Possible consequences: State corruption, ownership takeover, complete contract compromise, fund loss through unauthorized access control changes + */ +rule initialize_already_initialized_reverts(env e) { + address initialOwner; + uint32 initialTableUpdateCadence; + uint256 initialPausedStatus; + + // assign all the 'before' variables + uint8 _initialized_before = currentContract._initialized; + + // call function under test + initialize@withrevert(e, initialOwner, initialTableUpdateCadence, initialPausedStatus); + bool initialize_reverted = lastReverted; + + // verify integrity + assert ((_initialized_before != 0) => initialize_reverted), "_initialized != 0 => revert"; +} + +/* + * initialOwner != address(0) => _owner@after == initialOwner + * _paused@after == initialPausedStatus + * _initialized@after == 1 + * _initialized@before == 0 + * + * What it means: When a valid (non-zero) initialOwner is provided, the _owner storage variable must be set to that address after initialization. The _paused storage variable must be set to the initialPausedStatus parameter value after initialization. The _initialized flag must be set to 1 to mark the contract as initialized + * + * Why it should hold: This ensures proper ownership transfer during initialization. The owner has critical privileges in this contract including managing chain whitelists, so correct ownership assignment is essential for security + * + * Possible consequences: Loss of administrative control, inability to manage protocol parameters, potential for contract to become unmanageable + */ +rule initialize_integrity(env e) { + address initialOwner; + uint32 initialTableUpdateCadence; + uint256 initialPausedStatus; + + // assign all the 'before' variables + uint8 initializedBefore = currentContract._initialized; + + // call function under test + initialize(e, initialOwner, initialTableUpdateCadence, initialPausedStatus); + + // assign all the 'after' variables + address ownerAfter = currentContract._owner; + uint256 pausedAfter = currentContract._paused; + uint32 tableUpdateCadenceAfter = currentContract._tableUpdateCadence; + + // verify integrity + assert (initialOwner != 0 => ownerAfter == initialOwner), "initialOwner != address(0) => _owner@after == initialOwner"; + assert (pausedAfter == initialPausedStatus), "_paused@after == initialPausedStatus"; + assert (initializedBefore == 0 && currentContract._initialized == 1), "_initialized@after == 1"; + assert (tableUpdateCadenceAfter == initialTableUpdateCadence && initialTableUpdateCadence != 0); +} + + + +/* + * _paused != 0 => revert + * + * What it means: The function must revert if the contract is in any paused state (when _paused is non-zero) + * + * Why it should hold: The function has the onlyWhenNotPaused(PAUSED_GENERATION_RESERVATIONS) modifier, which should prevent execution when the contract is paused. This is a critical safety mechanism to halt operations during emergencies or maintenance + * + * Possible consequences: If this property is violated, attackers could continue creating generation reservations even when the contract is paused, potentially bypassing emergency stops, maintenance windows, or security incident responses + */ +rule createGenerationReservation_paused_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + address operatorTableCalculator; + ICrossChainRegistryTypes.OperatorSetConfig config; + + uint256 mask = 1 << 0; // PAUSED_GENERATION_RESERVATIONS == 0 + bool paused = (currentContract._paused & mask) == mask; + + // call function under test + createGenerationReservation@withrevert(e, operatorSet, operatorTableCalculator, config); + bool createGenerationReservation_reverted = lastReverted; + + // verify integrity + assert (paused => createGenerationReservation_reverted), "_paused != 0 => revert"; +} + +/* + * !allocationManager.isOperatorSet(operatorSet) => revert + * + * What it means: The function must revert if the provided operator set is not recognized as valid by the allocation manager + * + * Why it should hold: The function has the isValidOperatorSet modifier that calls allocationManager.isOperatorSet(operatorSet). Only legitimate operator sets registered with the allocation manager should be allowed to create reservations + * + * Possible consequences: If this property is violated, attackers could create reservations for non-existent or unauthorized operator sets, leading to invalid cross-chain configurations and potential system corruption + */ +rule createGenerationReservation_invalid_operator_set_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + address operatorTableCalculator; + ICrossChainRegistryTypes.OperatorSetConfig config; + + // assign all the 'before' variables + bool isOperatorSet = currentContract.allocationManager.isOperatorSet(e, operatorSet); + + // call function under test + createGenerationReservation@withrevert(e, operatorSet, operatorTableCalculator, config); + bool createGenerationReservation_reverted = lastReverted; + + // verify integrity + assert (!isOperatorSet => createGenerationReservation_reverted), "!allocationManager.isOperatorSet(operatorSet) => revert"; +} + +/* + * _paused != 0 => revert + * + * What it means: The function must revert when the contract is in a paused state (when _paused is not zero) + * + * Why it should hold: The function has the onlyWhenNotPaused(PAUSED_GENERATION_RESERVATIONS) modifier which should prevent execution when paused. This is a critical safety mechanism to halt operations during emergencies or maintenance + * + * Possible consequences: Emergency pause mechanisms could be bypassed, allowing operations to continue during critical vulnerabilities or maintenance periods, potentially leading to state corruption or exploitation + */ +rule removeGenerationReservation_paused_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + + // assign all the 'before' variables + uint256 mask = 1 << 0; // PAUSED_GENERATION_RESERVATIONS == 0 + bool paused = (currentContract._paused & mask) == mask; + + // call function under test + removeGenerationReservation@withrevert(e, operatorSet); + bool removeGenerationReservation_reverted = lastReverted; + + // verify integrity + assert (paused => removeGenerationReservation_reverted), "_paused != 0 => revert"; +} + +/* + * !allocationManager.isOperatorSet(operatorSet) => revert + * + * What it means: The function must revert when called with an operator set that is not valid according to the AllocationManager + * + * Why it should hold: The function has the isValidOperatorSet modifier which validates the operator set exists in the AllocationManager. This prevents operations on non-existent or invalid operator sets + * + * Possible consequences: Operations could be performed on invalid operator sets, leading to inconsistent state between the CrossChainRegistry and AllocationManager, potentially causing system-wide inconsistencies + */ +rule removeGenerationReservation_invalid_operator_set_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + + // assign all the 'before' variables + bool isOperatorSet = currentContract.allocationManager.isOperatorSet(e, operatorSet); + + // call function under test + removeGenerationReservation@withrevert(e, operatorSet); + bool removeGenerationReservation_reverted = lastReverted; + + // verify integrity + assert (!isOperatorSet => removeGenerationReservation_reverted), "!allocationManager.isOperatorSet(operatorSet) => revert"; +} + +/* + * _paused & PAUSED_OPERATOR_TABLE_CALCULATOR != 0 => revert + * + * What it means: The function must revert when the PAUSED_OPERATOR_TABLE_CALCULATOR pause flag is set in the _paused bitmap + * + * Why it should hold: The contract implements a pausable mechanism where specific functionality can be disabled during emergencies or maintenance. The onlyWhenNotPaused(PAUSED_OPERATOR_TABLE_CALCULATOR) modifier enforces this check + * + * Possible consequences: Emergency pause mechanisms could be bypassed, allowing critical operations to continue during security incidents or maintenance periods when they should be halted + */ +rule setOperatorTableCalculator_paused_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + address operatorTableCalculator; + + // assign all the 'before' variables + uint256 mask = 1 << 1; // PAUSED_OPERATOR_TABLE_CALCULATOR == 1 + bool paused = (currentContract._paused & mask) == mask; + + // call function under test + setOperatorTableCalculator@withrevert(e, operatorSet, operatorTableCalculator); + bool setOperatorTableCalculator_reverted = lastReverted; + + // verify integrity + assert (paused => setOperatorTableCalculator_reverted), "_paused & PAUSED_OPERATOR_TABLE_CALCULATOR != 0 => revert"; +} + +/* + * !allocationManager.isOperatorSet(operatorSet) => revert + * + * What it means: The function must revert if the provided operatorSet is not recognized as valid by the allocationManager + * + * Why it should hold: The isValidOperatorSet modifier ensures only legitimate operator sets registered in the AllocationManager can have calculators set. This prevents operations on non-existent or unauthorized operator sets + * + * Possible consequences: Unauthorized operator sets could have calculators assigned, leading to invalid cross-chain operations and potential manipulation of operator table calculations + */ +rule setOperatorTableCalculator_invalid_operator_set_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + address operatorTableCalculator; + + // assign all the 'before' variables + bool isOperatorSet = currentContract.allocationManager.isOperatorSet(e, operatorSet); + + // call function under test + setOperatorTableCalculator@withrevert(e, operatorSet, operatorTableCalculator); + bool setOperatorTableCalculator_reverted = lastReverted; + + // verify integrity + assert (!isOperatorSet => setOperatorTableCalculator_reverted), "!allocationManager.isOperatorSet(operatorSet) => revert"; +} + + +/* + * _paused & PAUSED_OPERATOR_SET_CONFIG != 0 => revert + * + * What it means: The function must revert when the PAUSED_OPERATOR_SET_CONFIG flag is set in the _paused bitmap + * + * Why it should hold: The contract implements a pausable mechanism where specific functionality can be disabled during emergencies or maintenance. The onlyWhenNotPaused(PAUSED_OPERATOR_SET_CONFIG) modifier should enforce this by checking the pause status and reverting if the corresponding bit is set + * + * Possible consequences: If this property is violated, critical operator set configuration changes could occur during emergency situations when the system should be frozen, potentially allowing malicious configuration updates during security incidents or system maintenance + */ +rule setOperatorSetConfig_paused_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + ICrossChainRegistryTypes.OperatorSetConfig config; + + // assign all the 'before' variables + uint256 _paused_before = currentContract._paused; + uint256 mask = 1 << 2; // PAUSED_OPERATOR_SET_CONFIG == 2 + bool paused = (currentContract._paused & mask) == mask; + + // call function under test + setOperatorSetConfig@withrevert(e, operatorSet, config); + bool setOperatorSetConfig_reverted = lastReverted; + + // verify integrity + assert (paused => setOperatorSetConfig_reverted), "_paused & PAUSED_OPERATOR_SET_CONFIG != 0 => revert"; +} + +/* + * !allocationManager.isOperatorSet(operatorSet) => revert + * + * What it means: The function must revert when the provided operatorSet is not recognized as valid by the AllocationManager + * + * Why it should hold: The isValidOperatorSet modifier calls allocationManager.isOperatorSet(operatorSet) to ensure only legitimate operator sets can have their configurations modified. This prevents configuration of non-existent or unauthorized operator sets + * + * Possible consequences: If this property is violated, attackers could create configurations for fake or unauthorized operator sets, leading to state corruption, resource waste, and potential manipulation of cross-chain registry operations + */ +rule setOperatorSetConfig_invalid_operator_set_reverts(env e) { + CrossChainRegistry.OperatorSet operatorSet; + ICrossChainRegistryTypes.OperatorSetConfig config; + + // assign all the 'before' variables + bool isOperatorSet = currentContract.allocationManager.isOperatorSet(e, operatorSet); + + // call function under test + setOperatorSetConfig@withrevert(e, operatorSet, config); + bool setOperatorSetConfig_reverted = lastReverted; + + // verify integrity + assert (!isOperatorSet => setOperatorSetConfig_reverted), "!allocationManager.isOperatorSet(operatorSet) => revert"; +} + + + +/* + * Combined revert conditions for addChainIDsToWhitelist + * + * Must revert if: + * 1) Paused bit for whitelist is set + * 2) chainIDs.length != operatorTableUpdaters.length + * 3) Any chainIDs[i] == 0 + * 4) msg sender is not owner + */ +rule addChainIDsToWhitelist_revert_conditions(env e) { + address[] operatorTableUpdaters; + uint256[] chainIDs; + + // --- snapshots / pre-state + uint256 _paused_before = currentContract._paused; + uint256 mask = 1 << 3; // PAUSED_CHAIN_WHITELIST == 3 + bool paused = (_paused_before & mask) == mask; + + uint256 i; + bool zero_present = i < chainIDs.length && chainIDs[i] == 0; + + // --- call function under test + addChainIDsToWhitelist@withrevert(e, chainIDs, operatorTableUpdaters); + bool reverted = lastReverted; + + // --- verify revert conditions + assert (paused + || (e.msg.sender != currentContract._owner) + || (chainIDs.length != operatorTableUpdaters.length) + || zero_present + => reverted); +} + + +/* + * removeChainIDsFromWhitelist revert conditions + * + * Must revert if: + * 1) Paused bit for whitelist is set + * 2) Any chainIDs[i] is not whitelisted in the pre-state + * 3) Any duplicate chain ID appears in the input (i != j && chainIDs[i] == chainIDs[j]) + * + * Empty arrays are allowed and should NOT revert. + */ +rule removeChainIDsFromWhitelist_revert_conditions(env e) { + uint256[] chainIDs; + + // --- pre-state + uint256 paused_before = currentContract._paused; + uint256 mask = 1 << 3; // PAUSED_CHAIN_WHITELIST == 3 + bool paused = (paused_before & mask) == mask; + + uint256 len = chainIDs.length; + + // nondet indices to quantify over the input + uint256 i; + uint256 j; + + bool i_in = (i < len); + bool j_in = (j < len) && (j != i); + uint256 ci = chainIDs[i]; + uint256 cj = chainIDs[j]; + // Any duplicate anywhere in the input will cause the second removal to fail. + bool duplicate_present = i_in && j_in && (ci == cj); + + // --- call function under test + removeChainIDsFromWhitelist@withrevert(e, chainIDs); + bool reverted = lastReverted; + + assert (duplicate_present|| paused || e.msg.sender != currentContract._owner => reverted); + // --- allowed no-op + assert ((!paused && e.msg.sender == currentContract._owner && len == 0 && e.msg.value == 0) => !reverted), "empty input is allowed and should not revert"; +} diff --git a/certora/specs/multichain/ECDSACertificateVerifier.spec b/certora/specs/multichain/ECDSACertificateVerifier.spec new file mode 100644 index 0000000000..51e580b090 --- /dev/null +++ b/certora/specs/multichain/ECDSACertificateVerifier.spec @@ -0,0 +1,101 @@ +using OperatorSetHelper as OperatorSetHelper; + +methods { + function ECDSACertificateVerifier._parseSignatures(bytes32 signableDigest, bytes memory signatures) internal returns (address[] memory) => cvlParseSignatures(signatures); + function OperatorSetHelper.getOperatorSetKey(ECDSACertificateVerifier.OperatorSet os) external returns (bytes32) envfree; +} + +// Needed because the copy loop in _parseSignatures seems to be heavy for the prover. +function cvlParseSignatures(bytes signatures) returns (address[]) { + uint256 signatureCount = require_uint256(signatures.length / 65); + address[] signers; + require signers.length == signatureCount; + return signers; +} + +use builtin rule sanity filtered { f -> f.contract == currentContract } + + +rule ecdsa_updateOperatorTable_revert_conditions(env e) { + ECDSACertificateVerifier.OperatorSet os; + uint32 ts; + IOperatorTableCalculatorTypes.ECDSAOperatorInfo[] operatorInfos; + ICrossChainRegistryTypes.OperatorSetConfig cfg; + + bytes32 k = OperatorSetHelper.getOperatorSetKey(os); + bool notUpdater = e.msg.sender != currentContract.operatorTableUpdater; + bool stale = ts <= currentContract._latestReferenceTimestamps[k]; + + updateOperatorTable@withrevert(e, os, ts, operatorInfos, cfg); + assert ((notUpdater || stale) => lastReverted), + "onlyTableUpdater && ts must be strictly newer"; +} + +rule ecdsa_updateOperatorTable_updates_and_frames(env e) { + ECDSACertificateVerifier.OperatorSet os; + uint32 ts; + IOperatorTableCalculatorTypes.ECDSAOperatorInfo[] operatorInfos; + ICrossChainRegistryTypes.OperatorSetConfig cfg; + + bytes32 k = OperatorSetHelper.getOperatorSetKey(os); + ECDSACertificateVerifier.OperatorSet other; + bytes32 ok = OperatorSetHelper.getOperatorSetKey(other); + + // snapshots + uint32 latest_before = currentContract._latestReferenceTimestamps[k]; + uint32 other_before = currentContract._latestReferenceTimestamps[ok]; + + updateOperatorTable(e, os, ts, operatorInfos, cfg); + + // effects + assert currentContract._latestReferenceTimestamps[k] == ts; + assert currentContract._latestReferenceTimestamps[k] > latest_before; + assert currentContract._numOperators[k][ts] == operatorInfos.length; + assert currentContract._operatorSetOwners[k] == cfg.owner; + assert currentContract._maxStalenessPeriods[k] == cfg.maxStalenessPeriod; + + // frame: other sets unchanged + assert (ok == k) || (currentContract._latestReferenceTimestamps[ok] == other_before); +} + +rule ecdsa_verifyCertificate_disabled_root_reverts(env e) { + ECDSACertificateVerifier.OperatorSet os; + IECDSACertificateVerifierTypes.ECDSACertificate cert; + + bool disabled = !currentContract.operatorTableUpdater.isRootValidByTimestamp(e, cert.referenceTimestamp); + + verifyCertificate@withrevert(e, os, cert); + assert (disabled => lastReverted), "disabled root => revert"; +} + +rule ecdsa_verifyCertificate_staleness_window_reverts(env e) { + ECDSACertificateVerifier.OperatorSet os; + IECDSACertificateVerifierTypes.ECDSACertificate cert; + + bytes32 k = OperatorSetHelper.getOperatorSetKey(os); + bool stale = currentContract._maxStalenessPeriods[k] != 0 && e.block.timestamp > cert.referenceTimestamp + currentContract._maxStalenessPeriods[k]; + + verifyCertificate@withrevert(e, os, cert); + assert (stale => lastReverted), "cert beyond staleness window => revert"; +} + + +rule ecdsa_verify_paths_do_not_mutate_state(env e) { + ECDSACertificateVerifier.OperatorSet os; + IECDSACertificateVerifierTypes.ECDSACertificate cert; + uint16[] p; uint256[] n; + + bytes32 k = OperatorSetHelper.getOperatorSetKey(os); + + uint32 latest_before = currentContract._latestReferenceTimestamps[k]; + uint32 maxStale_before = currentContract._maxStalenessPeriods[k]; + address owner_before = currentContract._operatorSetOwners[k]; + + verifyCertificate(e, os, cert); + verifyCertificateProportion(e, os, cert, p); + verifyCertificateNominal(e, os, cert, n); + + assert currentContract._latestReferenceTimestamps[k] == latest_before; + assert currentContract._maxStalenessPeriods[k] == maxStale_before; + assert currentContract._operatorSetOwners[k] == owner_before; +} \ No newline at end of file diff --git a/certora/specs/multichain/EnumerableSet.spec b/certora/specs/multichain/EnumerableSet.spec new file mode 100644 index 0000000000..8c069afad5 --- /dev/null +++ b/certora/specs/multichain/EnumerableSet.spec @@ -0,0 +1,54 @@ +// GHOST COPIES: +// For every storage variable we add a ghost field that is kept synchronized by hooks. +// The ghost fields can be accessed by the spec, even inside quantifiers. + +// ghost field for the values array +ghost mapping(mathint => bytes32) ghostValues_activeGenerationReservations { + init_state axiom forall mathint x. ghostValues_activeGenerationReservations[x] == to_bytes32(0); +} +// ghost field for the indexes map +ghost mapping(bytes32 => uint256) ghostIndexes_activeGenerationReservations { + init_state axiom forall bytes32 x. ghostIndexes_activeGenerationReservations[x] == 0; +} +// ghost field for the length of the values array (stored in offset 0) +ghost uint256 ghostLength_activeGenerationReservations { + init_state axiom ghostLength_activeGenerationReservations == 0; + // assumption: it's infeasible to grow the list to these many elements. + axiom ghostLength_activeGenerationReservations < max_uint256; +} + +// HOOKS +// Store hook to synchronize ghostLength_activeGenerationReservations with the length of the _activeGenerationReservations._inner._values array. +hook Sstore currentContract._activeGenerationReservations._inner._values.length uint256 newLength { + ghostLength_activeGenerationReservations = newLength; +} +// Store hook to synchronize ghostValues_activeGenerationReservations array with _activeGenerationReservations._inner._values. +hook Sstore currentContract._activeGenerationReservations._inner._values[INDEX uint256 index] bytes32 newValue { + ghostValues_activeGenerationReservations[index] = newValue; +} +// Store hook to synchronize ghostIndexes_activeGenerationReservations array with _activeGenerationReservations._inner._indexes. +hook Sstore currentContract._activeGenerationReservations._inner._indexes[KEY bytes32 value] uint256 newIndex { + ghostIndexes_activeGenerationReservations[value] = newIndex; +} + +// Load hook to synchronize ghostLength_activeGenerationReservations with the length of the _activeGenerationReservations._inner._values array. +hook Sload uint256 length currentContract._activeGenerationReservations._inner._values.length { + require ghostLength_activeGenerationReservations == length; +} +hook Sload bytes32 value currentContract._activeGenerationReservations._inner._values[INDEX uint256 index] { + require ghostValues_activeGenerationReservations[index] == value; +} +hook Sload uint256 index currentContract._activeGenerationReservations._inner._indexes[KEY bytes32 value] { + require ghostIndexes_activeGenerationReservations[value] == index; +} + +// INVARIANTS +// This is the main invariant stating that the indexes and values always match: +// values[indexes[v] - 1] = v for all values v in the _activeGenerationReservations +// and indexes[values[i]] = i+1 for all valid indexes i. + +invariant _activeGenerationReservationsInvariant() + (forall uint256 index. 0 <= index && index < ghostLength_activeGenerationReservations => to_mathint(ghostIndexes_activeGenerationReservations[ghostValues_activeGenerationReservations[index]]) == index + 1) + && (forall bytes32 value. ghostIndexes_activeGenerationReservations[value] == 0 || + (ghostValues_activeGenerationReservations[ghostIndexes_activeGenerationReservations[value] - 1] == value && ghostIndexes_activeGenerationReservations[value] >= 1 && ghostIndexes_activeGenerationReservations[value] <= ghostLength_activeGenerationReservations)); + diff --git a/certora/specs/multichain/OperatorTableUpdater.spec b/certora/specs/multichain/OperatorTableUpdater.spec new file mode 100644 index 0000000000..04176bef40 --- /dev/null +++ b/certora/specs/multichain/OperatorTableUpdater.spec @@ -0,0 +1,224 @@ +import "../libraries/BN254-nondet.spec"; + +methods { +} + +use builtin rule sanity filtered { f -> f.contract == currentContract } + + +// A tiny “frame” helper for maps: if key != touchedKey then unchanged. +function unchangedMappingUint32(uint32 before, uint32 after, bool keysEqual) returns (bool) { + return keysEqual || (after == before); +} + +// A tiny “frame” helper for maps: if key != touchedKey then unchanged. +function unchangedMappingBytes32(bytes32 before, bytes32 after, bool keysEqual) returns (bool) { + return keysEqual || (after == before); +} + +rule confirmGlobalTableRoot_reverts_conditions(env e) { + IBN254CertificateVerifierTypes.BN254Certificate cert; + bytes32 root; + uint32 ts; + uint32 blk; + + bool futureTS = ts > e.block.timestamp; + bool staleTS = ts <= currentContract._latestReferenceTimestamp; + bool zeroTS = ts == 0; + bool invalidMsgHash = currentContract.getGlobalTableUpdateMessageHash(e, root, ts, blk) != cert.messageHash; + // PAUSED_GLOBAL_ROOT_UPDATE = 0 + uint256 mask = 1 << 0; + bool paused = (currentContract._paused & mask) == mask; + + confirmGlobalTableRoot@withrevert(e, cert, root, ts, blk); + bool reverted = lastReverted; + + assert ((futureTS || staleTS || invalidMsgHash || zeroTS || paused) => reverted), + "future || stale || bad messageHash => revert"; +} + +rule confirmGlobalTableRoot_success_updates_and_frames(env e) { + IBN254CertificateVerifierTypes.BN254Certificate cert; + bytes32 root; uint32 ts; uint32 blk; + + // Snapshots + uint32 latest_before = currentContract._latestReferenceTimestamp; + + // Other keys for frame checks + uint32 otherTs; + uint32 otherBlk; + bytes32 otherRoot; + + bytes32 roots_other_before = currentContract._globalTableRoots[otherTs]; + uint32 blks_other_before = currentContract._referenceBlockNumbers[otherTs]; + uint32 ts_other_before = currentContract._referenceTimestamps[otherBlk]; + bool valid_other_before = currentContract._isRootValid[otherRoot]; + + address _owner_before = currentContract._owner; + uint16 threshold_before = currentContract.globalRootConfirmationThreshold; + uint256 paused_before = currentContract._paused; + + + // Call + confirmGlobalTableRoot(e, cert, root, ts, blk); + + // Post + assert ( + currentContract._latestReferenceTimestamp == ts + && currentContract._referenceBlockNumbers[ts] == blk + && currentContract._referenceTimestamps[blk] == ts + && currentContract._globalTableRoots[ts] == root + && currentContract._isRootValid[root] == true + ); + + // Frame: no unintended writes + assert (unchangedMappingBytes32(roots_other_before, + currentContract._globalTableRoots[otherTs], + otherTs == ts)); + assert (unchangedMappingUint32(blks_other_before, + currentContract._referenceBlockNumbers[otherTs], + otherTs == ts)); + assert (unchangedMappingUint32(ts_other_before, + currentContract._referenceTimestamps[otherBlk], + otherBlk == blk)); + assert ( (otherRoot == root) || (currentContract._isRootValid[otherRoot] == valid_other_before) ); + + // Governance params don’t change here + assert currentContract.globalRootConfirmationThreshold == threshold_before; + assert currentContract._owner == _owner_before; + assert currentContract._paused == paused_before; +} + +rule confirmGlobalTableRoot_strictly_monotonic(env e) { + IBN254CertificateVerifierTypes.BN254Certificate cert; + bytes32 root; uint32 ts; uint32 blk; + + uint32 latest_before = currentContract._latestReferenceTimestamp; + confirmGlobalTableRoot(e, cert, root, ts, blk); + assert currentContract._latestReferenceTimestamp > latest_before; +} + + +rule updateOperatorTable_revert_conditions(env e) { + uint32 referenceTimestamp; + bytes32 root; + uint32 idx; + bytes proof; + bytes operatorTable; + + // Snapshots to read pre-state in asserts + bool rootValid_before = currentContract._isRootValid[root]; + bool emptyTable = operatorTable.length == 0; + + // an unset reference timestamp does not cause a revert but noop + bool referenceTimestampSet = isReferenceTimestampSet(e, operatorTable, referenceTimestamp); + + // the following revert cases only trigger if referenceTimestampSet == true + bool staleTS = referenceTimestamp <= latestTsForOperatorTableBytes(e, operatorTable); + bool mismatchedRoot = root != currentContract._globalTableRoots[referenceTimestamp]; + bool invalidCurvetype = !validCurvetype(e, operatorTable); + + uint256 _paused_before = currentContract._paused; + uint256 mask = 1 << 1; // PAUSED_OPERATOR_TABLE_UPDATE == 1 + bool paused = (currentContract._paused & mask) == mask; + + updateOperatorTable@withrevert(e, referenceTimestamp, root, idx, proof, operatorTable); + bool reverted = lastReverted; + + assert ((!rootValid_before || paused || emptyTable ) => reverted), + "!_isRootValid[root] || _globalTableRoots[ts] != root || paused => revert"; + assert !referenceTimestampSet => ((mismatchedRoot || staleTS || invalidCurvetype) => reverted); +} + +rule updateOperatorTable_frame_conditions(env e) { + uint32 ts; bytes32 root; uint32 idx; bytes proof; bytes table; + + // Snapshots + uint32 latest_before = currentContract._latestReferenceTimestamp; + bytes32 mapped_before = currentContract._globalTableRoots[ts]; + uint16 thresh_before = currentContract.globalRootConfirmationThreshold; + address owner_before = currentContract._owner; + uint256 paused_before = currentContract._paused; + bool rootValid_before_state = currentContract._isRootValid[root]; + + updateOperatorTable(e, ts, root, idx, proof, table); + + // No writes to these in implementation + assert currentContract._latestReferenceTimestamp == latest_before; + assert currentContract._globalTableRoots[ts] == mapped_before; + assert currentContract.globalRootConfirmationThreshold == thresh_before; + assert currentContract._owner == owner_before; + assert currentContract._paused == paused_before; + assert currentContract._isRootValid[root] == rootValid_before_state; +} + +rule disableRoot_then_updateOperatorTable_must_revert(env e) { + bytes32 root; uint32 ts; uint32 idx; bytes proof; bytes table; + + // Disable + disableRoot(e, root); + assert !currentContract._isRootValid[root]; + + // Now any attempt to use it must revert (independent of other args) + updateOperatorTable@withrevert(e, ts, root, idx, proof, table); + assert lastReverted; +} + + +rule setGlobalRootConfirmationThreshold_revert_conditions(env e) { + uint16 bps; + + // onlyOwner + setGlobalRootConfirmationThreshold@withrevert(e, bps); + bool reverted = lastReverted; + + assert ((e.msg.sender != currentContract._owner || bps > currentContract.MAX_BPS(e)) => reverted), "onlyOwner"; +} + +rule setGlobalRootConfirmationThreshold_success_and_frame_conditions(env e) { + uint16 bps; + uint32 someTs; + uint32 someBlk; + + address owner = currentContract._owner; + uint32 referenceTimestamp = currentContract._latestReferenceTimestamp; + uint32 refBlockNum_before = currentContract._referenceBlockNumbers[someTs]; + uint32 refTimestamp_before = currentContract._referenceTimestamps[someBlk]; + + // success updates + setGlobalRootConfirmationThreshold(e, bps); + + // integrity check + assert (currentContract.globalRootConfirmationThreshold == bps); + + // frame on unrelated state + assert currentContract._latestReferenceTimestamp == referenceTimestamp; + assert currentContract._owner == owner; + assert currentContract._referenceBlockNumbers[someTs] == refBlockNum_before; + assert currentContract._referenceTimestamps[someBlk] == refTimestamp_before; +} + + +rule disableRoot_revert_conditions(env e){ + bytes32 root; + + bool valid_before = currentContract._isRootValid[root]; + bool pauser = currentContract.pauserRegistry.isPauser(e, e.msg.sender); + + disableRoot@withrevert(e, root); + + assert ((!pauser || !valid_before) => lastReverted), "valid root || onlyPauser"; +} + +rule disableRoot_success_and_frame_conditions(env e) { + bytes32 root; + bytes32 other; + + bool other_before = currentContract._isRootValid[other]; + + // success effect + disableRoot(e, root); + + assert (currentContract._isRootValid[root] == false); + assert ( (other == root) || (currentContract._isRootValid[other] == other_before) ); +} \ No newline at end of file diff --git a/certora/specs/permissions/KeyRegistrar.spec b/certora/specs/permissions/KeyRegistrar.spec new file mode 100644 index 0000000000..2c309aca90 --- /dev/null +++ b/certora/specs/permissions/KeyRegistrar.spec @@ -0,0 +1,328 @@ +import "../libraries/BN254-nondet.spec"; +using AllocationManager as AllocationManager; +using PermissionController as PermissionController; + +methods { + function _.canCall(address, address, address, bytes4) external => DISPATCHER(true); + function _.isValidERC1271SignatureNow(address, bytes32, bytes memory) internal => NONDET; + + function isRegistered(KeyRegistrar.OperatorSet, address) external returns (bool) envfree; + + function getOperatorSetKey(KeyRegistrar.OperatorSet) external returns (bytes32) envfree; + function getOperatorKeyDataHash(bytes32, address) external returns (bytes32) envfree; + + // external calls to AVSRegistrar. Note that the source does not have a proper implementation, the one available always reverts + function _.registerOperator(address,address,uint32[],bytes) external => DISPATCHER(true); + function _.deregisterOperator(address,address,uint32[]) external => DISPATCHER(true); + function _.supportsAVS(address) external => DISPATCHER(true); +} + +use builtin rule sanity filtered { f -> f.contract == currentContract } + + +rule global_registry_monotonic(method f, env e, calldataarg args) filtered { f -> !f.isView } { + bytes32 keyHash; + + // snapshot + bool _globalKeyRegistry_before = currentContract._globalKeyRegistry[keyHash]; + + // execute arbitrary non-view function + f(e, args); + + // check monotonicity + assert _globalKeyRegistry_before => currentContract._globalKeyRegistry[keyHash], "_globalKeyRegistry must never flip from true to false"; +} + +/* + * curveType == 0 => revert + * + * What it means: The function must revert when curveType is 0 (NONE), preventing configuration with an invalid curve type + * + * Why it should hold: CurveType.NONE (value 0) represents an unconfigured state, not a valid curve type for cryptographic operations. Allowing configuration with NONE would create an inconsistent state where an operator set appears configured but has no valid cryptographic curve + * + * Possible consequences: State corruption where operator sets appear configured but cannot perform cryptographic operations, leading to system-wide failures in key registration and verification + */ +rule configureOperatorSet_invalidCurveTypeReverts(env e) { + KeyRegistrar.OperatorSet os; + IKeyRegistrarTypes.CurveType curveType; + bytes32 key = getOperatorSetKey(os); + + // assign all the 'before' variables + IKeyRegistrarTypes.CurveType curveTypeBefore = currentContract._operatorSetCurveTypes[key]; + + // call function under test + configureOperatorSet@withrevert(e, os, curveType); + bool configureOperatorSet_reverted = lastReverted; + + // assign all the 'after' variables + IKeyRegistrarTypes.CurveType curveTypeAfter = currentContract._operatorSetCurveTypes[key]; + + // verify integrity + assert (curveType == IKeyRegistrarTypes.CurveType.NONE) => configureOperatorSet_reverted, "curveType == NONE => revert"; + assert (curveTypeBefore != IKeyRegistrarTypes.CurveType.NONE => configureOperatorSet_reverted), "curveTypeBefore must be empty"; + assert (curveTypeAfter == curveType && (curveType == IKeyRegistrarTypes.CurveType.ECDSA || curveType == IKeyRegistrarTypes.CurveType.BN254)) || configureOperatorSet_reverted, "curveType must be valid after successful configuration"; +} + +/* + * operatorSetNotConfigured || keyAlreadyRegistered => revert + * + * What it means: + * `registerKey` must revert if either (a) the operator‑set has **not** been + * configured with a valid curve type (`_operatorSetCurveTypes == NONE`), or + * (b) the operator already has a key registered in that set, (c) keyData cannot be empty, + * (d) keyData must be exactly 20 bytes for ECDSA keys or 192 bytes for BN254 keys - any other length should cause registration to fail + * + * Why it should hold: + * Registering under an unconfigured curve type would leave the system in an + * unusable state, while allowing duplicate registrations would violate the + * one‑key‑per‑operator invariant and undermine key‑uniqueness guarantees. + * + * Possible consequences: + * If the check is bypassed, keys could be registered under invalid cryptographic + * parameters, or operators could overwrite/accumulate multiple keys. Either case + * leads to inconsistent state, signature‑verification failures, and potential + * security breaches. + */ +rule registerKey_revertConditions(env e) { + KeyRegistrar.OperatorSet os; + address operator; + bytes keyData; + bytes signature; + bytes32 key = getOperatorSetKey(os); + + // Ensure the operatorSet has been configured with a valid curve + bool operatorSetNotConfigured = currentContract._operatorSetCurveTypes[key] == IKeyRegistrarTypes.CurveType.NONE; + bool keyAlreadyRegistered = currentContract._operatorKeyInfo[key][operator].isRegistered == true; + bool emptyKeyData = keyData.length == 0; + bool validKeyDataLength = (currentContract._operatorSetCurveTypes[key] == IKeyRegistrarTypes.CurveType.ECDSA && keyData.length == 20) || (currentContract._operatorSetCurveTypes[key] == IKeyRegistrarTypes.CurveType.BN254 && keyData.length == 192); + bool callAuthorized = PermissionController.canCall(e, operator, e.msg.sender, currentContract, to_bytes4(sig:registerKey(address, KeyRegistrar.OperatorSet, bytes, bytes).selector)); + + // Then the call to registerKey should proceed + registerKey@withrevert(e, operator, os, keyData, signature); + bool registerKeyReverted = lastReverted; + + assert operatorSetNotConfigured => registerKeyReverted; + assert keyAlreadyRegistered => registerKeyReverted; + assert emptyKeyData => registerKeyReverted; + assert !validKeyDataLength => registerKeyReverted; + assert !callAuthorized => registerKeyReverted; +} + +/* + * (_operatorKeyInfo[operatorSetKey][operator] or keyData) changed + * => f.selector == registerKey || deregisterKey + * + * What it means: + * Any state change that touches an operator’s key‑registration record—either + * the `isRegistered` flag or the stored key‑data hash—**must** originate + * exclusively from the `registerKey` or `deregisterKey` functions. All other + * non‑view methods are forbidden to modify this storage. + * + * Why it should hold: + * Centralising mutations in the dedicated registration functions preserves + * invariant boundaries, simplifies auditing, and prevents accidental or + * malicious corruption of key‑management data by unrelated contract logic. + * + * Possible consequences: + * If another function can alter these fields, it might silently register, + * deregister, or tamper with keys without passing the intended access‑control + * and validation pathways—resulting in lost keys, unauthorised operators, + * denial‑of‑service, or broken cryptographic assumptions across the system. + */ +rule onlyRegisterAndDeregisterKeyModifyOperatorKeyInfo(method f, env e, calldataarg args) filtered { f -> !f.isView } + { + address operator; + KeyRegistrar.OperatorSet os; + bytes32 key = getOperatorSetKey(os); + + // Snapshot old state + bool isRegistered = currentContract._operatorKeyInfo[key][operator].isRegistered; + bytes32 keyData = getOperatorKeyDataHash(key, operator); + + // Run any non-view function + f(e, args); + + // Assert state only changed by register or deregister key + assert (getOperatorKeyDataHash(key, operator) != keyData || + currentContract._operatorKeyInfo[key][operator].isRegistered != isRegistered) + => (f.selector == sig:registerKey(address, KeyRegistrar.OperatorSet, bytes, bytes).selector || + f.selector == sig:deregisterKey(address, KeyRegistrar.OperatorSet).selector); +} + + +/* + * a call to `registerKey` must turn `isRegistered` `false → true`; a call to `deregisterKey` must turn it `true → false`. + */ +rule registrationFlagFlipsCorrectly(method f, env e, calldataarg args) filtered { f -> !f.isView } { + address operator; + KeyRegistrar.OperatorSet os; + bytes32 k = getOperatorSetKey(os); + bool before = currentContract._operatorKeyInfo[k][operator].isRegistered; + + f(e,args); + + bool after = currentContract._operatorKeyInfo[k][operator].isRegistered; + + assert (f.selector == sig:registerKey(address, KeyRegistrar.OperatorSet, bytes, bytes).selector) => + ((before == false) => after || before == after); //can stay the same if the registered key is different from k + assert (f.selector == sig:deregisterKey(address, KeyRegistrar.OperatorSet).selector) => + ((before == true) => !after || before == after); //can stay the same if the deregistered key is different from k + assert (f.selector != sig:registerKey(address, KeyRegistrar.OperatorSet, bytes, bytes).selector && f.selector != sig:deregisterKey(address, KeyRegistrar.OperatorSet).selector) => before == after; +} + + +rule onlyConfigureOperatorSetMayWriteCurveType(method f, env e, calldataarg args) + filtered { f -> !f.isView } { + bytes32 setKey; + + IKeyRegistrarTypes.CurveType before = currentContract._operatorSetCurveTypes[setKey]; + f(e, args); + IKeyRegistrarTypes.CurveType after = currentContract._operatorSetCurveTypes[setKey]; + + assert (before != after) => + (f.selector == sig:configureOperatorSet(KeyRegistrar.OperatorSet, IKeyRegistrarTypes.CurveType).selector); +} + + + +/* + * otherOperator != operator => _operatorKeyInfo[operatorSetKey][otherOperator].isRegistered@after == _operatorKeyInfo[operatorSetKey][otherOperator].isRegistered@before + * + * What it means: When one operator deregisters their key, the registration status of all other operators in the same operator set must remain unchanged + * + * Why it should hold: Key deregistration should be isolated to the specific operator performing the action. Other operators' keys are independent and should not be affected by unrelated deregistration operations. + * + * Possible consequences: If other operators' registrations are affected, it could lead to widespread service disruption, unauthorized deregistration of valid keys, and breaking the isolation principle between different operators' key management. + */ +rule deregisterKey_other_operators_unchanged(env e) { + address operator; + KeyRegistrar.OperatorSet operatorSet; + bytes32 operatorSetKey; + address otherOperator; + + // assign all the 'before' variables + bool _operatorKeyInfo_operatorSetKey__otherOperator__isRegistered_before = currentContract._operatorKeyInfo[operatorSetKey][otherOperator].isRegistered; + + // call function under test + deregisterKey(e, operator, operatorSet); + + // assign all the 'after' variables + bool _operatorKeyInfo_operatorSetKey__otherOperator__isRegistered_after = currentContract._operatorKeyInfo[operatorSetKey][otherOperator].isRegistered; + + // verify integrity + assert ((otherOperator != operator) => (_operatorKeyInfo_operatorSetKey__otherOperator__isRegistered_after == _operatorKeyInfo_operatorSetKey__otherOperator__isRegistered_before)), "otherOperator != operator => _operatorKeyInfo[operatorSetKey][otherOperator].isRegistered@after == _operatorKeyInfo[operatorSetKey][otherOperator].isRegistered@before"; +} + + +/* + * (!keyRegistered) ∨ (operatorSetNotConfigured) ∨ (isOperatorSlashable) ⇒ revert + * + * What it means — `deregisterKey` must **fail** in any of the following + * pre‑conditions: + * 1. **Key not registered**  The operator has no key recorded in the requested + * operator‑set (`_operatorKeyInfo[setKey][operator].isRegistered == false`). + * 2. **Operator‑set not configured**  The set’s curve type is + * `CurveType.NONE`, signalling it has never been initialised for use. + * 3. **Operator is slashable**  `AllocationManager.isOperatorSlashable` + * reports the operator is currently subject to slashing and therefore + * must not be allowed to opt‑out. + * + * Why it should hold: + * • Prevents meaningless state transitions on non‑existent keys. + * • Guards against interacting with an uninitialised cryptographic domain. + * • Ensures slashable operators cannot escape penalties by deregistering. + * + * Possible consequences if violated: + * • Deregistering a non‑existent key breaks invariants and confuses callers. + * • Operating on an unconfigured set may leave the system in an unusable or + * inconsistent state. + * • Allowing slashable operators to deregister could let them evade economic + * punishment and undermine security assumptions. + */ +rule deregisterKey_revertConditions(env e) { + address operator; + KeyRegistrar.OperatorSet operatorSet; + bytes32 operatorSetKey = getOperatorSetKey(operatorSet); + + // assign all the 'before' variables + bool keyRegistered = currentContract._operatorKeyInfo[operatorSetKey][operator].isRegistered; + bool operatorSetNotConfigured = currentContract._operatorSetCurveTypes[operatorSetKey] == IKeyRegistrarTypes.CurveType.NONE; + bool isOperatorSlashable = AllocationManager.isOperatorSlashable(e, operator, operatorSet); + bool callAuthorized = PermissionController.canCall(e, operator, e.msg.sender, currentContract, to_bytes4(sig:deregisterKey(address, KeyRegistrar.OperatorSet).selector)); + // call function under test + deregisterKey@withrevert(e, operator, operatorSet); + bool deregisterKey_reverted = lastReverted; + + // verify integrity + assert (!keyRegistered => deregisterKey_reverted), "!_operatorKeyInfo[operatorSetKey][operator].isRegistered => revert"; + assert (operatorSetNotConfigured => deregisterKey_reverted), "curveType is 0 => revert"; + assert (isOperatorSlashable => deregisterKey_reverted), "operator that is slashable cannot be deregistered"; + assert (!callAuthorized => deregisterKey_reverted), "unauthorized operator"; +} + +/***************************************************************** + * 1. configureOperatorSet — unauthorised caller must revert + *****************************************************************/ +rule configureOperatorSet_unauthorisedCallerReverts(env e) { + KeyRegistrar.OperatorSet os; + IKeyRegistrarTypes.CurveType curveType; + + // Permission check performed by the modifier in Solidity + bool callAuthorised = + PermissionController.canCall( + e, + os.avs, // account + e.msg.sender, // caller + currentContract, // target + to_bytes4(sig:configureOperatorSet(KeyRegistrar.OperatorSet, IKeyRegistrarTypes.CurveType).selector) + ); + + configureOperatorSet@withrevert(e, os, curveType); + bool reverted = lastReverted; + + // If not authorised, the call **must** revert + assert (!callAuthorised) => reverted, "configureOperatorSet: unauthorised caller should revert"; +} + + + +/***************************************************************** + * 2. Only registerKey may set a new entry in _globalKeyRegistry + *****************************************************************/ +rule onlyRegisterKeyMayWriteGlobalRegistry(method f, env e, calldataarg args) + filtered { f -> !f.isView } { + bytes32 keyHash; + + bool before = currentContract._globalKeyRegistry[keyHash]; + f(e, args); + bool after = currentContract._globalKeyRegistry[keyHash]; + + /* A transition false → true is allowed **only** via registerKey */ + assert ((after && !before) => + (f.selector == sig:registerKey(address, KeyRegistrar.OperatorSet, bytes, bytes).selector)), + "_globalKeyRegistry can be set only in registerKey"; +} + + + +/***************************************************************** + * 3. registerKey must not touch other operators’ records + *****************************************************************/ +rule registerKey_otherOperatorsUnchanged(env e) { + address operator; + address otherOperator; + KeyRegistrar.OperatorSet os; + bytes keyData; + bytes signature; + bytes32 setKey = getOperatorSetKey(os); + + /* Snapshot another operator’s registration status */ + bool before = currentContract._operatorKeyInfo[setKey][otherOperator].isRegistered; + + registerKey@withrevert(e, operator, os, keyData, signature); + + bool after = currentContract._operatorKeyInfo[setKey][otherOperator].isRegistered; + + assert ((otherOperator != operator) => (after == before)), + "registerKey must not modify registrations of other operators"; +}