Mutant governance core 13

.github/workflows/certora-review-execution-chain.yml

@@ -6,7 +6,7 @@ on:
       - main
   pull_request:
     branches:
-      - main
+      - certora
 
   workflow_dispatch:
 
@@ -64,4 +64,4 @@ jobs:
           - verifyPayloadsController.conf --rule action_signature_immutable
           - verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields
           - verifyPayloadsController.conf --rule zero_executedAt_if_not_executed
-
+

.github/workflows/certora-review-mainnet.yml

@@ -7,7 +7,7 @@ on:
       - main
   pull_request:
     branches:
-      - main
+      - certora
 
   workflow_dispatch:
 
@@ -63,4 +63,4 @@ jobs:
           - verifyGovernance.conf --rule cannot_queue_when_voting_portal_unapproved only_owner_can_set_voting_config_witness only_owner_can_set_voting_config single_state_transition_per_block_non_creator_witness 
           - verifyGovernance.conf --rule single_state_transition_per_block_non_creator_non_guardian state_cant_decrease no_state_transitions_beyond_3 immutable_voting_portal insufficient_proposition_power_time_elapsed_tight_witness 
           - verifyGovernance.conf --rule insufficient_proposition_power_allow_time_elapse insufficient_proposition_power proposal_after_voting_portal_invalidate
-
+

.github/workflows/certora-review-voting-chain.yml

@@ -7,7 +7,7 @@ on:
       - main
   pull_request:
     branches:
-      - main
+      - certora
 
   workflow_dispatch:
 

security/certora/confs/verifyVotingStrategy_unittests.conf

@@ -21,6 +21,8 @@
     "verify": "VotingStrategy:security/certora/specs/VotingStrategy_unittests.spec",
     "optimistic_loop": true,
     "loop_iter": "3",  // Needs 2 for isTokenSlotAccepted (A_AAVE uses 2 slots)
+    //"parametric_contracts":["VotingStrategy"
+    //],
     "solc": "solc8.19",
     "msg": "VotingStrategy tests"
 }

security/certora/scripts/verifyPayloadsController.sh

@@ -0,0 +1,80 @@
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule payload_maximal_access_level_gt_action_access_level no_late_cancel state_cant_decrease no_transition_beyond_state_gt_3 no_transition_beyond_state_variable_gt_3 no_queue_after_expiration empty_actions_if_out_of_bound_payload expirationTime_equal_to_createAt_plus_EXPIRATION_DELAY empty_actions_iff_uninitialized null_access_level_if_out_of_bound_payload null_creator_and_zero_expiration_time_if_out_of_bound_payload empty_actions_only_if_uninitialized_payload executor_access_level_within_range consecutiveIDs empty_actions_if_uninitialized_payload queued_before_expiration_delay payload_grace_period_eq_global_grace_period null_access_level_only_if_out_of_bound_payload null_state_variable_if_out_of_bound_payload created_in_the_past executedAt_is_zero_before_executed queued_after_created executed_after_queue queuedAt_is_zero_before_queued no_early_cancellation guardian_can_cancel executed_when_in_queued_state execute_before_delay__maximumAccessLevelRequired action_immutable_fixed_size_fields initialized_payload_fields_are_immutable payload_fields_immutable_after_createPayload method_reachability \
+           --msg "1: many rules"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_exists_if_action_not_null \
+           --msg "2: executor_exists_if_action_not_null"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_exists_only_if_action_not_null \
+           --msg "3: executor_exists_only_if_action_not_null"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule payload_delay_within_range \
+           --msg "4: payload_delay_within_range"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule delay_of_executor_of_max_access_level_within_range \
+           --msg "5: delay_of_executor_of_max_access_level_within_range"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule nonempty_actions \
+           --msg "6: nonempty_actions"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_exists_iff_action_not_null \
+           --msg "7: executor_exists_iff_action_not_null"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule null_access_level_iff_state_is_none \
+           --msg "8: null_access_level_iff_state_is_none"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_of_maximumAccessLevelRequired_exists \
+           --msg "9: executor_of_maximumAccessLevelRequired_exists"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload \
+           --msg "10: executor_of_maximumAccessLevelRequired_exists_after_createPayload"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule action_access_level_isnt_null_after_createPayload \
+           --msg "11: action_access_level_isnt_null_after_createPayload"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule executor_exists_after_createPayload \
+           --msg "12: executor_exists_after_createPayload"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule action_callData_immutable \
+           --msg "13: action_callData_immutable"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule action_signature_immutable \
+           --msg "14: action_signature_immutable"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule action_immutable_check_only_fixed_size_fields \
+           --msg "15: action_immutable_check_only_fixed_size_fields"
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/payloads/verifyPayloadsController.conf \
+           --rule zero_executedAt_if_not_executed \
+           --msg "16: zero_executedAt_if_not_executed"

security/certora/scripts/voting-chain.sh

@@ -0,0 +1,89 @@
+
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyLegality.conf \
+           --rule createdVoteHasNonZeroHash \
+           --msg "1: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyLegality.conf \
+           --rule onlyValidProposalCanChangeTally \
+           --msg "2: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyLegality.conf \
+           --rule legalVote \
+           --msg "3: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyLegality.conf \
+           --rule votedPowerIsImmutable method_reachability \
+           --msg "4: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyMisc.conf \
+           --msg "5: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyPower_summary.conf \
+           --msg "6: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_config.conf \
+           --rule createdProposalHasRoots \
+           --msg "7: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_config.conf \
+           --rule startedProposalHasConfig \
+           --msg "8: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_config.conf \
+           --rule proposalHasNonzeroDuration configIsImmutable newProposalUnusedId method_reachability \
+           --msg "9: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule proposalImmutability \
+           --msg "10: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule startsStrictlyBeforeEnds \
+           --msg "11: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule startsBeforeEnds \
+           --msg "12: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule startedProposalHasConfig \
+           --msg "13: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule proposalMethodStateTransitionCompliance \
+           --msg "14: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyProposal_states.conf \
+           --rule proposalIdIsImmutable proposalHasNonzeroDuration proposalTimeStateTransitionCompliance proposalLegalStates method_reachability \
+           --msg "15: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyVoting_and_tally.conf \
+           --rule voteUpdatesTally \
+           --msg "16: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyVoting_and_tally.conf \
+           --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote \
+           --msg "17: "
+
+certoraRun --fe_version latest --send_only --disable_auto_cache_key_gen \
+           security/certora/confs/voting/verifyVoting_and_tally.conf \
+           --rule voteTallyChangedOnlyByVoting onlyVoteCanChangeResult votingTallyCanOnlyIncrease strangerVoteUnchanged otherProposalUnchanged otherVoterUntouched cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote method_reachability \
+           --msg "18: "

security/certora/tests/BaseVotingStrategy-6.sol

@@ -0,0 +1,116 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity ^0.8.0;
+
+import {IBaseVotingStrategy} from '../interfaces/IBaseVotingStrategy.sol';
+import {Errors} from './libraries/Errors.sol';
+
+//import {AaveV3EthereumAssets} from 'aave-address-book/AaveV3Ethereum.sol';
+
+/**
+ * @title BaseVotingStrategy
+ * @author BGD Labs
+ * @notice This contract contains the base logic of a voting strategy, being on governance chain or voting machine chain.
+ */
+abstract contract BaseVotingStrategy is IBaseVotingStrategy {
+  function AAVE() public pure virtual returns (address) {
+    return 0x7Fc66500c84A76Ad7e9c93437bFc5Ac33E2DDaE9;
+  }
+
+  function STK_AAVE() public pure virtual returns (address) {
+    return 0x4da27a545c0c5B758a6BA100e3a049001de870f5;
+  }
+
+  function A_AAVE() public pure virtual returns (address) {
+    return 0xA700b4eB416Be35b2911fd5Dee80678ff64fF6C9;
+  }
+
+  uint128 public constant BASE_BALANCE_SLOT = 0;
+  uint128 public constant A_AAVE_BASE_BALANCE_SLOT = 52;
+  uint128 public constant A_AAVE_DELEGATED_STATE_SLOT = 64;
+
+  /// @dev on the constructor we get all the voting assets and emit the different asset configurations
+  constructor() {
+    address[] memory votingAssetList = getVotingAssetList();
+
+    // Check that voting strategy at least has one asset
+    require(votingAssetList.length != 0, Errors.NO_VOTING_ASSETS);
+
+    for (uint256 i = 0; i < votingAssetList.length; i++) {
+      for (uint256 j = i + 1; j < votingAssetList.length; j++) {
+        require(
+          votingAssetList[i] != votingAssetList[j],
+          Errors.REPEATED_STRATEGY_ASSET
+        );
+      }
+      VotingAssetConfig memory votingAssetConfig = getVotingAssetConfig(
+        votingAssetList[i]
+      );
+
+      require(
+        votingAssetConfig.storageSlots.length > 0,
+        Errors.EMPTY_ASSET_STORAGE_SLOTS
+      );
+
+      for (uint256 k = 0; k < votingAssetConfig.storageSlots.length; k++) {
+        for (
+          uint256 l = k + 1;
+          l < votingAssetConfig.storageSlots.length;
+          l++
+        ) {
+          require(
+            votingAssetConfig.storageSlots[k] !=
+              votingAssetConfig.storageSlots[l],
+            Errors.REPEATED_STRATEGY_ASSET_SLOT
+          );
+        }
+      }
+
+      emit VotingAssetAdd(votingAssetList[i], votingAssetConfig.storageSlots);
+    }
+  }
+
+  /// @inheritdoc IBaseVotingStrategy
+  function getVotingAssetList() public pure returns (address[] memory) {
+    address[] memory votingAssets = new address[](3);
+
+    votingAssets[0] = AAVE();
+    votingAssets[1] = STK_AAVE();
+    votingAssets[2] = A_AAVE();
+
+    return votingAssets;
+  }
+
+  /// @inheritdoc IBaseVotingStrategy
+  function getVotingAssetConfig(
+    address asset
+  ) public pure returns (VotingAssetConfig memory) {
+    VotingAssetConfig memory votingAssetConfig;
+
+    if (asset == AAVE() || asset == STK_AAVE()) {
+      votingAssetConfig.storageSlots = new uint128[](1);
+      votingAssetConfig.storageSlots[0] = BASE_BALANCE_SLOT;
+    } else if (asset == A_AAVE()) {
+      votingAssetConfig.storageSlots = new uint128[](2);
+      votingAssetConfig.storageSlots[0] = BASE_BALANCE_SLOT;
+      votingAssetConfig.storageSlots[1] = A_AAVE_DELEGATED_STATE_SLOT;
+    } else {
+      return votingAssetConfig;
+    }
+
+    return votingAssetConfig;
+  }
+
+  /// @inheritdoc IBaseVotingStrategy
+  function isTokenSlotAccepted(
+    address token,
+    uint128 slot
+  ) external pure returns (bool) {
+    VotingAssetConfig memory votingAssetConfig = getVotingAssetConfig(token);
+    for (uint256 i = 0; i < votingAssetConfig.storageSlots.length; i++) {
+      if (slot == votingAssetConfig.storageSlots[i]) {
+        return true;
+      }
+    }
+    return false;
+  }
+}

security/certora/tests/REPORT-power-strategy.txt

@@ -23,7 +23,8 @@ Suggestion for rules that can catch it:
 - For every voting token T, and every user U that does not delegate, if the balance of U in T is increased then the power of U increased.
 
 
-2. UNDETECTED
+2. DETECTED 
+By certora-review-mainnet.yml::verifyVotingStrategy_unittests.conf
 Changed file: BaseVotingStrategy.sol ==> BaseVotingStrategy-2.sol
 The change: BaseVotingStrategy.sol:109:
    orig:
@@ -35,18 +36,18 @@ Suggestion for rule that can catch it:
 - We have the rule: invalidTokenRefused(...). We can add its analogue validTokenAccepted(...).
 
 
-3. DETECTED
+3. DETECTED 
+By: certora-review-mainnet.yml::verifyGovernancePowerStrategy.conf
 Changed file: GovernancePowerStrategy.sol ==> GovernancePowerStrategy-3.sol
 The change: GovernancePowerStrategy.sol::25:
    orig:
         "IGovernancePowerDelegationToken.GovernancePowerType.VOTING"
    mutant:
         "IGovernancePowerDelegationToken.GovernancePowerType.PROPOSITION"
 
-Found by: powerlessCompliance
 
 
-4. UNDETECTED
+4. UNDETECTED 
 Changed file: GovernancePowerStrategy.sol ==> GovernancePowerStrategy-4.sol
 The change: GovernancePowerStrategy.sol::53:
     orig:
@@ -71,7 +72,11 @@ Suggestion for rule that can catch it:
 - Same as in #4.
 
 
-6. DETECTED by invalidTokenRefused
+6. DETECTED
+By:
+certora-review-mainnet.yml::verifyVotingStrategy_unittests.conf
+certora-review-mainnet.yml::verifyGovernancePowerStrategy.conf
+
 Changed file: BaseVotingStrategy.sol ==> BaseVotingStrategy-6.sol
 The Change: BaseVotingStrategy.sol::94:
     orig: