Merge pull request #6 from Certora/certora-properties

Certora Review

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

@@ -0,0 +1,66 @@
+name: certora-review-execution-chain
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install certora cli
+        run: pip3 install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          certoraRun security/certora/confs/payloads/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - 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 decode2encode_sanity_check_message_leq_96_pass decode2encode_sanity_check_message_eq_96_satisfy 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
+          - verifyPayloadsController.conf --rule executor_exists
+          - verifyPayloadsController.conf --rule executor_exists_if_action_not_null
+          - verifyPayloadsController.conf --rule executor_exists_only_if_action_not_null
+          - verifyPayloadsController.conf --rule payload_delay_within_range
+          - verifyPayloadsController.conf --rule delay_of_executor_of_max_access_level_within_range
+          - verifyPayloadsController.conf --rule nonempty_actions
+          - verifyPayloadsController.conf --rule executor_exists_iff_action_not_null
+          - verifyPayloadsController.conf --rule null_access_level_iff_state_is_none
+          - verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists
+          - verifyPayloadsController.conf --rule executor_of_maximumAccessLevelRequired_exists_after_createPayload
+          - verifyPayloadsController.conf --rule action_access_level_isnt_null_after_createPayload
+          - verifyPayloadsController.conf --rule executor_exists_after_createPayload
+          - verifyPayloadsController.conf --rule action_callData_immutable
+          - verifyPayloadsController.conf --rule action_signature_immutable
+          - verifyPayloadsController.conf --rule action_immutable_check_only_fixed_size_fields
+

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

@@ -0,0 +1,66 @@
+# Github action for verifying the contracts under src/contracts/voting
+name: certora-review-mainnet
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install certora cli
+        run: pip3 install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          certoraRun security/certora/confs/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyVotingStrategy_unittests.conf
+          - verifyGovernancePowerStrategy.conf
+          - verifyGovernance.conf --rule cancellationFeeZeroForFutureProposals null_state_variable_iff_null_access_level zero_voting_portal_iff_uninitialized_proposal 
+          - verifyGovernance.conf --rule no_self_representative no_representative_is_zero  consecutiveIDs totalCancellationFeeEqualETHBalance zero_address_is_not_a_valid_voting_portal 
+          - verifyGovernance.conf --rule no_representative_is_zero_2 no_representative_of_zero empty_payloads_if_uninitialized_proposal null_state_variable_only_if_uninitialized_proposal 
+          - verifyGovernance.conf --rule post_state state_changing_function_self_check state_variable_changing_function_self_check initialize_sanity sanity userFeeDidntChangeImplyNativeBalanceDidntDecrease
+          - verifyGovernance.conf --rule check_new_representative_set_size_after_updateRepresentatives check_old_representative_set_size_after_updateRepresentatives set_size_leq_max_uint160
+          - verifyGovernance.conf --rule at_least_single_payload_active at_least_single_payload_active_variable creator_is_not_zero creator_is_not_zero_2 empty_payloads_iff_uninitialized_proposal 
+          - verifyGovernance.conf --rule null_state_iff_uninitialized_proposal null_state_variable_iff_uninitialized_proposal null_state_if_uninitialized_proposal null_state_variable_if_uninitialized_proposal
+          - verifyGovernance.conf --rule null_state_only_if_uninitialized_proposal pre_state terminal_state_cannot_change state_changing_function_cannot_be_called_while_in_terminal_state proposal_executes_after_cooldown_period
+          - verifyGovernance.conf --rule only_valid_voting_portal_can_queue_proposal immutable_after_activation immutable_payload_after_creation immutable_after_creation only_guardian_can_cancel guardian_can_cancel 
+          - 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

@@ -0,0 +1,57 @@
+# Github action for verifying the contracts under src/contracts/voting
+name: certora-review-voting-chain
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install certora cli
+        run: pip3 install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          certoraRun security/certora/confs/voting/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyLegality.conf
+          - verifyMisc.conf
+          - verifyPower_summary.conf
+          - verifyProposal_config.conf
+          - verifyProposal_states.conf
+          - verifyVoting_and_tally.conf

security/certora/confs/payloads/verifyPayloadsController.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "security/certora/harness/PayloadsControllerHarness.sol",
+        "src/contracts/payloads/Executor.sol",
+        "src/contracts/payloads/PayloadsControllerUtils.sol",
+        "security/certora/harness/DummyERC20Impl.sol"
+    ],
+    "packages": [
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "loop_iter": "3",
+    "msg": "All payloadControllers rules",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "prover_args": [
+        " -smt_LIASolvers [z3:def,z3:lia1,z3:lia2] -smt_NIASolvers [z3:def]"
+    ],
+    "smt_timeout": "6000",
+    "solc": "solc8.19",
+    "struct_link": [
+        "PayloadsControllerHarness:executor=Executor"
+    ],
+    "verify": "PayloadsControllerHarness:security/certora/specs/payloads/PayloadsController.spec"
+}

security/certora/confs/verifyGovernance.conf

@@ -0,0 +1,31 @@
+{
+    "files": [
+        "security/certora/harness/GovernanceHarness.sol",
+        "src/contracts/VotingPortal.sol",
+        "src/contracts/voting/VotingStrategy.sol",
+        "lib/aave-token-v3/src/AaveTokenV3.sol",
+        "src/contracts/GovernancePowerStrategy.sol",
+        "src/contracts/payloads/PayloadsControllerUtils.sol"
+    ],
+    "link": [
+        "GovernanceHarness:_powerStrategy=GovernancePowerStrategy"
+    ],
+    "packages": [
+        "aave-address-book=lib/aave-address-book/src",
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "aave-token-v3=lib/aave-token-v3/src",
+        "openzeppelin-contracts=lib/openzeppelin-contracts",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "verify": "GovernanceHarness:security/certora/specs/Governance.spec",
+    "struct_link": [
+        "GovernanceHarness:votingPortal=VotingPortal"
+    ],
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "prover_args": [
+        " -copyLoopUnroll 8"
+    ],
+    "solc": "solc8.19",
+    "msg": "All Governance rules",
+}

security/certora/confs/verifyGovernancePowerStrategy.conf

@@ -0,0 +1,23 @@
+{
+    "files": [
+        "src/contracts/GovernancePowerStrategy.sol",
+        "security/certora/harness/tokens/AaveTokenV3_DummyA.sol",
+        "security/certora/harness/tokens/AaveTokenV3_DummyB.sol",
+        "security/certora/harness/tokens/AaveTokenV3_DummyC.sol"
+    ],
+    "link": [
+    ],
+    "packages": [
+        "@openzeppelin=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "aave-token-v3=lib/aave-token-v3/src",
+        "forge-std=lib/forge-std/src",
+        "openzeppelin-contracts=lib/openzeppelin-contracts",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "verify": "GovernancePowerStrategy:security/certora/specs/GovernancePowerStrategy.spec",
+    "optimistic_loop": true,
+    "loop_iter": "3",  // Needs 3 for the 3 tokens
+    "solc": "solc8.19",
+    "msg": "GovernancePowerStrategy tests"
+}

security/certora/confs/verifyVotingStrategy_unittests.conf

@@ -0,0 +1,27 @@
+{
+    "files": [
+        "src/contracts/voting/VotingStrategy.sol",
+        "src/contracts/voting/DataWarehouse.sol",
+        "security/certora/harness/voting/DelegationModeHarness.sol"
+    ],
+    "link": [
+        "VotingStrategy:DATA_WAREHOUSE=DataWarehouse"
+    ],
+    "packages": [
+        "@openzeppelin=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
+        "aave-token-v3=lib/aave-token-v3/src",
+        "forge-std=lib/forge-std/src",
+        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
+        "openzeppelin-contracts=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
+        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "verify": "VotingStrategy:security/certora/specs/VotingStrategy_unittests.spec",
+    "optimistic_loop": true,
+    "loop_iter": "2",  // Needs 2 for isTokenSlotAccepted (A_AAVE uses 2 slots)
+    "solc": "solc8.19",
+    "msg": "VotingStrategy tests"
+}
+

security/certora/confs/voting/verifyLegality.conf

@@ -0,0 +1,34 @@
+// conf file for VotingMachine - legality.spec
+{
+    "files": [
+        "security/certora/harness/voting/VotingMachineHarness.sol",
+        "security/certora/harness/voting/VotingStrategyHarness.sol",
+        "src/contracts/voting/DataWarehouse.sol",
+        "src/contracts/voting/libs/StateProofVerifier.sol",
+        "src/contracts/libraries/SlotUtils.sol",
+        "lib/aave-delivery-infrastructure/src/contracts/CrossChainController.sol"
+    ],
+    "link": [
+        "VotingMachineHarness:VOTING_STRATEGY=VotingStrategyHarness",
+        "VotingMachineHarness:CROSS_CHAIN_CONTROLLER=CrossChainController",
+        "VotingMachineHarness:DATA_WAREHOUSE=DataWarehouse",  // NOTE: same as in VotingStrategy
+        "VotingStrategyHarness:DATA_WAREHOUSE=DataWarehouse"
+    ],
+    "packages": [
+        "@openzeppelin=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
+        "aave-token-v3=lib/aave-token-v3/src",
+        "forge-std=lib/forge-std/src",
+        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
+        "openzeppelin-contracts=lib/openzeppelin-contracts",
+        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "verify": "VotingMachineHarness:security/certora/specs/voting/legality.spec",
+    "optimistic_loop": true,
+    "loop_iter": "1",
+    "optimistic_hashing": true,
+    "solc": "solc8.19",
+    "msg": "VotingMachine - legality rules"
+}

security/certora/confs/voting/verifyMisc.conf

@@ -0,0 +1,34 @@
+// conf file for VotingMachine - misc.spec
+{
+    "files": [
+        "security/certora/harness/voting/VotingMachineHarnessTriple.sol",
+        "security/certora/harness/voting/VotingStrategyHarness.sol",
+        "src/contracts/voting/DataWarehouse.sol",
+        "src/contracts/voting/libs/StateProofVerifier.sol",
+        "src/contracts/libraries/SlotUtils.sol",
+        "lib/aave-delivery-infrastructure/src/contracts/CrossChainController.sol"
+    ],
+    "link": [
+        "VotingMachineHarnessTriple:VOTING_STRATEGY=VotingStrategyHarness",
+        "VotingMachineHarnessTriple:CROSS_CHAIN_CONTROLLER=CrossChainController",
+        "VotingMachineHarnessTriple:DATA_WAREHOUSE=DataWarehouse",  // NOTE: same as in VotingStrategy
+        "VotingStrategyHarness:DATA_WAREHOUSE=DataWarehouse"
+    ],
+    "packages": [
+        "@openzeppelin=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
+        "aave-delivery-infrastructure=lib/aave-delivery-infrastructure/src",
+        "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
+        "aave-token-v3=lib/aave-token-v3/src",
+        "forge-std=lib/forge-std/src",
+        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
+        "openzeppelin-contracts=lib/openzeppelin-contracts",
+        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
+        "solidity-utils=lib/solidity-utils/src"
+    ],
+    "verify": "VotingMachineHarnessTriple:security/certora/specs/voting/misc.spec",
+    "optimistic_loop": true,
+    "loop_iter": "3",  // Needs 3 for `submitVoteTripleProof`
+    "optimistic_hashing": true,
+    "solc": "solc8.19",
+    "msg": "VotingMachine - miscellaneous rules"
+}