Certora formal verification

.github/workflows/certora-prover.yml

@@ -0,0 +1,35 @@
+on:
+  pull_request:
+    branches:
+      - dev
+  workflow_dispatch:
+
+jobs:
+  certora_run_submission:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v2
+        with:
+          # Add your configurations as lines, each line is separated.
+          # Specify additional options for each configuration by adding them after the configuration.
+          configurations: |-
+            certora/confs/ECDSATableCalculator.conf
+            certora/confs/AVSRegistrarWithAllowlist.conf
+            certora/confs/BN254TableCalculator.conf
+            certora/confs/AVSRegistrarWithSocket.conf
+            certora/confs/AVSRegistrar.conf
+          solc-versions: 0.8.27
+          job-name: "Verified Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

certora/confs/AVSRegistrar.conf

@@ -0,0 +1,23 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarAsIdentifier.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarAsIdentifier:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarAsIdentifier:allocationManager=AllocationManager"
+  ],
+  "msg": "AVSRegistrarAsIdentifier rules",
+  "server": "production",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarAsIdentifier.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarAsIdentifier:certora/specs/AVSRegistrar.spec"
+}

certora/confs/AVSRegistrarWithAllowlist.conf

@@ -0,0 +1,34 @@
+{
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarWithAllowlist.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarWithAllowlist:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarWithAllowlist:allocationManager=AllocationManager"
+  ],
+  "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",
+    "openzeppelin-contracts-upgradeable=lib/openzeppelin-contracts-upgradeable",
+    "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable",
+    "eigenlayer-contracts=lib/eigenlayer-contracts"
+  ],
+
+  "msg": "AVSRegistrarWithAllowlist rules",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarWithAllowlist.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarWithAllowlist:certora/specs/AVSRegistrarWithAllowlist.spec",
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf"
+}

certora/confs/AVSRegistrarWithSocket.conf

@@ -0,0 +1,22 @@
+{
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarWithSocket.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarWithSocket:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarWithSocket:allocationManager=AllocationManager"
+  ],
+  "msg": "AVSRegistrarWithSocket rules",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarWithSocket.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarWithSocket:certora/specs/AVSRegistrarWithSocket.spec",
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf"
+}

certora/confs/BN254TableCalculator.conf

@@ -0,0 +1,17 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/tableCalculator/BN254TableCalculator.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/DelegationManager.sol"
+  ],
+  "link": [
+    "BN254TableCalculator:keyRegistrar=KeyRegistrar",
+    "BN254TableCalculator:allocationManager=AllocationManager",
+    "AllocationManager:delegation=DelegationManager"
+  ],
+  "optimistic_hashing": true,
+  "msg": "sanity_BN254TableCalculator",
+  "verify": "BN254TableCalculator:certora/specs/BN254TableCalculator.spec"
+}

certora/confs/BaseConfForInheritance.conf

@@ -0,0 +1,31 @@
+{
+  "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",
+    "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable",
+    "openzeppelin-contracts-upgradeable=lib/openzeppelin-contracts-upgradeable",
+    "eigenlayer-contracts=lib/eigenlayer-contracts"
+  ],
+  "prover_args": [
+    "-verifyCache",
+    "-verifyTACDumps",
+    "-testMode",
+    "-checkRuleDigest",
+    "-callTraceHardFail on",
+    "-allowArrayLengthUpdates true",
+    "-linearInvariantBound 4"
+  ],
+  "prover_version": "master"
+}

certora/confs/ECDSATableCalculator.conf

@@ -0,0 +1,16 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/tableCalculator/ECDSATableCalculator.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/DelegationManager.sol"
+  ],
+  "link": [
+    "ECDSATableCalculator:keyRegistrar=KeyRegistrar",
+    "ECDSATableCalculator:allocationManager=AllocationManager",
+    "AllocationManager:delegation=DelegationManager"
+  ],
+  "msg": "sanity_ECDSATableCalculator",
+  "verify": "ECDSATableCalculator:certora/specs/ECDSATableCalculator.spec"
+}

certora/specs/AVSRegistrar.spec

@@ -0,0 +1,72 @@
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+
+methods{
+    // function _.getBN254Key(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    // function _.merkleizeKeccak(bytes32[] memory) internal => NONDET;
+    // function _getOperatorWeights(BN254TableCalculator.OperatorSet calldata) internal returns (address[] memory, uint256[][] memory) => returnEmptyWeights();
+
+}
+
+/*
+ * msg.sender != address(allocationManager) => revert
+ *
+ * What it means: 
+ * The registerOperator function can only be called by the AllocationManager contract address, and any call from a different address must revert.
+ * 
+ * Why it should hold: The function has the onlyAllocationManager modifier which enforces this access control. This is a critical security boundary that ensures only the authorized AllocationManager can register operators for the AVS. 
+ *
+ * Possible consequences: Unauthorized operator registration, bypassing of allocation management logic, potential manipulation of operator sets, and violation of the intended protocol governance structure. 
+ */
+rule registerOperatorOnlyAllocationManager(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+    bytes data;
+
+    // call function under test
+    registerOperator@withrevert(e, operator, _, operatorSetIds, data);
+    bool registerOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert ((e.msg.sender != currentContract.allocationManager) => registerOperator_reverted), "msg.sender != address(allocationManager) => revert";
+}
+
+rule registerOperatorOnlyValidKeys(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+    bytes data;
+
+    KeyRegistrar.OperatorSet operatorSet;
+    require operatorSetIds.length > 0, "assume non empty operator set list, an empty list does not cause a revert";
+    require operatorSet.avs == currentContract.avs;
+    require operatorSet.id == operatorSetIds[0];
+
+    bool keyRegistered = currentContract.keyRegistrar.isRegistered(e, operatorSet, operator);
+
+    // call function under test
+    registerOperator@withrevert(e, operator, _, operatorSetIds, data);
+    bool registerOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert (!keyRegistered => registerOperator_reverted), "operator key not valid";
+}
+
+/*
+ * msg.sender != address(allocationManager) => revert
+ *
+ * What it means: Only the allocation manager contract can call the deregisterOperator function, any other caller should cause a revert
+ *
+ * Why it should hold: The function has the onlyAllocationManager modifier which enforces access control. This is a critical security boundary that ensures only the authorized allocation manager can deregister operators. The zero address is not a valid operator address and deregistering it would be a meaningless operation. This prevents invalid input and follows standard Ethereum patterns of rejecting zero addresses
+ *
+ * Possible consequences: Unauthorized deregistration of operators, disruption of AVS operations, potential griefing attacks where malicious actors can remove legitimate operators. Invalid state transitions, confusion in operator tracking, potential issues with downstream systems that assume valid operator addresses
+ */
+rule deregisterOperatorOnlyAllocationManager(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+
+    // call function under test
+    deregisterOperator@withrevert(e, operator, _, operatorSetIds);
+    bool deregisterOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert ((e.msg.sender != currentContract.allocationManager) => deregisterOperator_reverted), "msg.sender != address(allocationManager) => revert";
+}

certora/specs/AVSRegistrarWithAllowlist.spec

@@ -0,0 +1,105 @@
+import "AVSRegistrar.spec";
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+use rule registerOperatorOnlyAllocationManager; 
+use rule registerOperatorOnlyValidKeys;
+use rule deregisterOperatorOnlyAllocationManager;
+
+
+/*
+ * _initialized > 0 => revert
+ *
+ * What it means: The initialize function must revert if the contract has already been initialized (_initialized > 0)
+ *
+ * Why it should hold: The initializer modifier should prevent re-initialization to maintain contract integrity and prevent ownership takeover after deployment
+ *
+ * Possible consequences: Ownership takeover, allowlist manipulation, complete compromise of access control system
+ */
+rule initialize_already_initialized_reverts(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    uint8 _initialized_before = currentContract._initialized;
+
+    // call function under test
+    initialize@withrevert(e, avs, admin);
+    bool initialize_reverted = lastReverted;
+
+    // verify integrity
+    assert ((_initialized_before > 0) => initialize_reverted), "_initialized > 0 => revert";
+}
+
+/*
+ * _initialized@after > _initialized@before
+ *
+ * What it means: After successful initialization, the _initialized state variable must increase from its previous value
+ *
+ * Why it should hold: The initializer modifier must properly mark the contract as initialized to prevent future re-initialization attempts
+ *
+ * Possible consequences: Re-initialization vulnerability, ownership takeover, state corruption
+ */
+rule initialize_sets_initialized_state(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    uint8 _initialized_before = currentContract._initialized;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    uint8 _initialized_after = currentContract._initialized;
+
+    // verify integrity
+    assert (_initialized_after > _initialized_before), "_initialized@after > _initialized@before";
+}
+
+/*
+ * _owner@after == admin
+ *
+ * What it means: When initialize is called with a  admin address, that address must become the contract owner
+ *
+ * Why it should hold: The purpose of initialization is to establish proper ownership, and the admin parameter should be set as the owner to enable access control
+ *
+ * Possible consequences: Broken access control, inability to manage allowlists, contract becomes non-functional
+ */
+rule initialize_admin_becomes_owner(env e) {
+    address admin;
+    address avs;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    address _owner_after = currentContract._owner;
+
+    // verify integrity
+    assert (_owner_after == admin), "_owner@after == admin";
+}
+
+/*
+ * _initializing@before == false && _initializing@after == false
+ *
+ * What it means: The _initializing flag should be false both before and after the initialize function execution
+ *
+ * Why it should hold: The initializer modifier should properly manage the _initializing flag to prevent reentrancy during initialization and ensure clean state transitions
+ *
+ * Possible consequences: Reentrancy attacks during initialization, inconsistent initialization state, potential for multiple simultaneous initializations
+ */
+rule initialize_initializing_flag_during_execution(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    bool _initializing_before = currentContract._initializing;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    bool _initializing_after = currentContract._initializing;
+
+    // verify integrity
+    assert ((_initializing_before == false) && (_initializing_after == false)), "_initializing@before == false && _initializing@after == false";
+}

certora/specs/AVSRegistrarWithSocket.spec

@@ -0,0 +1,5 @@
+import "AVSRegistrar.spec";
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+use rule registerOperatorOnlyAllocationManager; 
+use rule registerOperatorOnlyValidKeys;
+use rule deregisterOperatorOnlyAllocationManager;

certora/specs/BN254TableCalculator.spec

@@ -0,0 +1,24 @@
+import "Summaries/BN254-nondet.spec";
+import "Summaries/Math.spec";
+
+methods{
+    function _.isRegistered(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    function _.getBN254Key(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    function _.merkleizeKeccak(bytes32[] memory) internal => NONDET;
+    // function _getOperatorWeights(BN254TableCalculator.OperatorSet calldata) internal returns (address[] memory, uint256[][] memory) => returnEmptyWeights();
+
+    unresolved external in _._ => DISPATCH
+    [ 
+        KeyRegistrar.isRegistered(BN254TableCalculator.OperatorSet, address),
+        KeyRegistrar.getBN254Key(BN254TableCalculator.OperatorSet, address),
+    ] default NONDET;
+}
+
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+
+function returnEmptyWeights() returns (address[], uint256[][]) {
+    address[] addresses;
+    uint256[][] weights;
+
+    return (addresses, weights);
+}