Feat/phase 3

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

@@ -0,0 +1,56 @@
+name: certora-review-controller
+
+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==4.13.1
+
+      - 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: |
+          cd security/certora
+          touch applyHarness.patch
+          make munged
+          cd ../..
+          certoraRun security/certora/confs/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyCrossChainControllerWithEmergency.conf #to move to the new prover version, wait for ticket 6284
+
+

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

@@ -28,7 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==4.13.1
+        run: pip3 install certora-cli==7.6.3
 
       - name: Install solc
         run: |
@@ -55,4 +55,6 @@ jobs:
           - verifyCrossChainForwarder-invariants.conf
           - verifyCrossChainForwarder-newEnvelope.conf
           - verifyCrossChainForwarder-sanity.conf
-          - verifyCrossChainForwarder-simpleRules.conf
+          - verifyCrossChainForwarder-simpleRules.conf
+          - verifyCrossChainForwarder-encode-decode-correct.conf --rule encode_decode_well_formed_TX
+          - verifyCrossChainForwarder-shuffle.conf

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

@@ -28,7 +28,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip3 install certora-cli==4.13.1
+        run: pip3 install certora-cli==7.6.3
 
       - name: Install solc
         run: |
@@ -51,18 +51,6 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyCrossChainControllerWithEmergency.conf
-          #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_2 # TODO: uncomment when moving to cli 5.0.2 or higher
-          #- verifyCrossChainReceiver.conf --rule receive_more_than__requiredConfirmations_diff_3 # TODO: uncomment when moving to cli 5.0.2 or higher
-          - verifyCrossChainReceiver.conf --rule transaction_received_only_from_authorized_bridge_adapter only_owner_can_change_bridge_adapters only_owner_can_change_bridge_adapters_witness_consequent only_owner_can_change_required_confirmations only_owner_can_change_required_confirmations_witness_consequent cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice cannot_call_IBaseReceiverPortal_receiveCrossChainMessage_twice_witness_tight_bound state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called
-          - verifyCrossChainReceiver.conf --rule state_transition_to_deliver_iff_IBaseReceiverPortal_receiveCrossChainMessage_called_witness_antecedent call_deliverEnvelope_once_witness_antecedent anyone_can_call_deliverEnvelope invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp_witness_antecedent receiveCrossChainMessage_cannot_change_state_if_requiredConfirmation_is_zero envelope_state envelope_state_witness_none_to_delivered only_single_bridge_adapter_added only_single_bridge_adapter_removed
-          - verifyCrossChainReceiver.conf --rule envelope_state_witness_confirmed_to_delivered envelope_state_witness_none_to_confirmed envelope_state_witness_none_none_confirmed envelope_state_witness_none_confirmed_confirmed envelope_state_witness_confirmed_confirmed_confirmed confirmations_increments_if_received_from_msg_sender confirmations_increments_if_received_from_msg_sender_witness allowReceiverBridgeAdapters_cannot_disallow allowReceiverBridgeAdapters_cannot_disallow_witness
-          - verifyCrossChainReceiver.conf --rule disallowReceiverBridgeAdapters_cannot_allow disallowReceiverBridgeAdapters_cannot_allow_witness_antecedent disallowReceiverBridgeAdapters_cannot_allow_witness_consequent requiredConfirmation_is_positive_after_updateConfirmations receive_increments_confirmations     
-          - verifyCrossChainReceiver.conf --rule reachability encodeDecodeWorks encodeDecodeWorks_witness encodeDecodeWorks_witness_2 
-          - verifyCrossChainReceiver.conf --rule firstBridgedAt_happened_in_the_past  
-          - verifyCrossChainReceiver.conf --rule no_deliverEnvelope_after_receiveCrossChainMessage 
-          #- verifyCrossChainReceiver.conf --rule call_deliverEnvelope_once # TODO: uncomment when moving to cli 5.0.2 or higher
-          #- verifyCrossChainReceiver.conf --rule invalidate_previous_unconfirmed_envelopes_after_updateMessagesValidityTimestamp # TODO: uncomment when moving to cli 5.0.2 or higher
-          #- verifyCrossChainReceiver.conf --rule addressSetInvariant # TODO: uncomment when moving to cli 5.0.2 or higher
-          #- verifyCrossChainReceiver.conf --rule cannot_call_BaseReceiverPortal_receiveCrossChainMessage_twice # TODO: uncomment when moving to cli 5.0.2 or higher
-          - verifyCrossChainReceiver.conf --rule zero_firstBridgedAt_iff_not_received_from_msg_sender
+          - verifyCrossChainReceiver.conf 
+
+

.github/workflows/main.yml

@@ -10,3 +10,4 @@ on:
 jobs:
   test:
     uses: bgd-labs/github-workflows/.github/workflows/foundry-test.yml@main
+    secrets: inherit

.gitmodules

@@ -1,19 +1,7 @@
-[submodule "lib/solidity-utils"]
-	path = lib/solidity-utils
-	url = https://github.com/bgd-labs/solidity-utils
-[submodule "lib/forge-std"]
-	path = lib/forge-std
-	url = https://github.com/foundry-rs/forge-std
 [submodule "lib/openzeppelin-contracts"]
 	path = lib/openzeppelin-contracts
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts
 	branch = release-v4.9
-[submodule "lib/aave-address-book"]
-	path = lib/aave-address-book
-	url = https://github.com/bgd-labs/aave-address-book
-[submodule "lib/nitro-contracts"]
-	path = lib/nitro-contracts
-	url = https://github.com/OffchainLabs/nitro-contracts
-[submodule "lib/fx-portal"]
-	path = lib/fx-portal
-	url = https://github.com/0xPolygon/fx-portal
+[submodule "lib/aave-helpers"]
+	path = lib/aave-helpers
+	url = https://github.com/bgd-labs/aave-helpers

Makefile

@@ -40,226 +40,6 @@ forge script \
 
 endef
 
-# catapulta
-#define deploy_single_fn
-#npx catapulta@0.3.14 script \
-# scripts/$(1).s.sol:$(if $(3),$(3),$(shell UP=$(if $(PROD),$(2),$(2)_testnet); echo $${UP} | perl -nE 'say ucfirst')) \
-# --network $(2) --slow --skip-git \
-# $(if $(LEDGER),$(BASE_LEDGER),$(BASE_KEY)) \
-# $(custom_$(if $(PROD),$(2),$(2)-testnet))
-#
-#endef
-
 define deploy_fn
  $(foreach network,$(2),$(call deploy_single_fn,$(1),$(network),$(3)))
 endef
-
-# ----------------------------------------------------------------------------------------------------------------------
-# ----------------------------------------- PRODUCTION DEPLOYMENT SCRIPTS ---------------------------------------------------------
-
-# deploy emergency registry
-deploy-emergency-registry:
-	$(call deploy_fn,Deploy_EmergencyRegistry,ethereum)
-
-# Deploy Proxy Factories on all networks
-deploy-proxy-factory:
-	$(call deploy_fn,InitialDeployments,ethereum avalanche polygon optimism arbitrum metis base binance gnosis zkevm)
-
-# Deploy Cross Chain Infra on all networks
-deploy-cross-chain-infra:
-	$(call deploy_fn,CCC/Deploy_CCC,ethereum avalanche polygon optimism arbitrum metis base binance gnosis zkevm)
-
-## Deploy CCIP bridge adapters on all networks
-deploy-ccip-bridge-adapters:
-	$(call deploy_fn,Adapters/DeployCCIP,ethereum avalanche binance polygon binance gnosis)
-
-## Deploy LayerZero bridge adapters on all networks
-deploy-lz-bridge-adapters:
-	$(call deploy_fn,Adapters/DeployLZ,ethereum avalanche binance polygon binance gnosis)
-
-## Deploy HyperLane bridge adapters on all networks
-deploy-hl-bridge-adapters:
-	$(call deploy_fn,Adapters/DeployHL,ethereum avalanche binance polygon binance gnosis)
-
-## Deploy SameChain adapters on ethereum
-deploy-same-chain-adapters:
-	$(call deploy_fn,Adapters/DeploySameChainAdapter,ethereum)
-
-deploy-optimism-adapters:
-	$(call deploy_fn,Adapters/DeployOpAdapter,ethereum optimism)
-
-deploy-arbitrum-adapters:
-	$(call deploy_fn,Adapters/DeployArbAdapter,ethereum arbitrum)
-
-deploy-metis-adapters:
-	$(call deploy_fn,Adapters/DeployMetisAdapter,ethereum metis)
-
-deploy-polygon-adapters:
-	$(call deploy_fn,Adapters/DeployPolygon,ethereum polygon)
-
-deploy-base-adapters:
-	$(call deploy_fn,Adapters/DeployCBaseAdapter,ethereum base)
-
-deploy-gnosis-adapters:
-	$(call deploy_fn,Adapters/DeployGnosisChain,ethereum gnosis)
-
-deploy-scroll-adapters:
-	$(call deploy_fn,Adapters/DeployScrollAdapter,ethereum scroll)
-
-deploy-zkevm-adapters:
-	$(call deploy_fn,Adapters/DeployZkEVMAdapter,ethereum zkevm)
-
-deploy-wormhole-adapters:
-	$(call deploy_fn,Adapters/DeployWormholeAdapter,ethereum celo)
-
-## Set sender bridge dapters. Only eth pol avax are needed as other networks will only receive
-set-ccf-sender-adapters:
-	$(call deploy_fn,CCC/Set_CCF_Sender_Adapters,ethereum)
-
-# Set the bridge adapters allowed to receive messages
-set-ccr-receiver-adapters:
-	$(call deploy_fn,CCC/Set_CCR_Receivers_Adapters,ethereum polygon avalanche binance arbitrum optimism base metis gnosis zkevm)
-
-# Sets the required confirmations
-set-ccr-confirmations:
-	$(call deploy_fn,CCC/Set_CCR_Confirmations,ethereum polygon avalanche optimism arbitrum metis base binance gnosis zkevm)
-
-# Generate Addresses Json
-write-json-addresses :; forge script scripts/WriteAddresses.s.sol:WriteDeployedAddresses -vvvv
-
-# Funds CCC
-fund-crosschain:
-	$(call deploy_fn,CCC/FundCCC,ethereum polygon avalanche arbitrum)
-
-## Deploy and configure all contracts
-deploy-full:
-		make deploy-proxy-factory
-		make deploy-cross-chain-infra
-		make deploy-ccip-bridge-adapters
-		make deploy-lz-bridge-adapters
-		make deploy-hl-bridge-adapters
-		make deploy-same-chain-adapters
-		make deploy-optimism-adapters
-		make deploy-arbitrum-adapters
-		make deploy-metis-adapters
-		make deploy-polygon-adapters
-		make set-ccf-approved-senders
-		make set-ccf-sender-adapters
-		make set-ccr-receiver-adapters
-		make set-ccr-confirmations
-		make fund-crosschain
-		make write-json-addresses
-
-
-
-# ----------------------------------------------------------------------------------------------------------------------
-# ----------------------------------------- TESTNET DEPLOYMENT SCRIPTS ---------------------------------------------------------
-
-# Deploy Proxy Factories on all networks
-deploy-proxy-factory-test:
-	$(call deploy_fn,InitialDeployments,base)
-
-# Deploy Cross Chain Infra on all networks
-deploy-cross-chain-infra-test:
-	$(call deploy_fn,CCC/Deploy_CCC,ethereum)
-
-## Deploy CCIP bridge adapters on all networks
-deploy-ccip-bridge-adapters-test:
-	$(call deploy_fn,Adapters/DeployCCIP,ethereum)
-
-## Deploy LayerZero bridge adapters on all networks
-deploy-lz-bridge-adapters-test:
-	$(call deploy_fn,Adapters/DeployLZ,ethereum)
-
-## Deploy HyperLane bridge adapters on all networks
-deploy-hl-bridge-adapters-test:
-	$(call deploy_fn,Adapters/DeployHL,ethereum)
-
-## Deploy SameChain adapters on ethereum
-deploy-same-chain-adapters-test:
-	$(call deploy_fn,Adapters/DeploySameChainAdapter,ethereum)
-
-deploy-scroll-adapters-test:
-	$(call deploy_fn,Adapters/DeployScrollAdapter,ethereum)
-
-deploy-wormhole-adapters-test:
-	$(call deploy_fn,Adapters/DeployWormholeAdapter,ethereum)
-
-deploy-polygon-adapters-test:
-	$(call deploy_fn,Adapters/DeployPolygon,ethereum)
-
-deploy-gnosis-adapters-test:
-	$(call deploy_fn,Adapters/DeployGnosisChain,ethereum)
-
-deploy-arbitrum-adapters-test:
-	$(call deploy_fn,Adapters/DeployArbAdapter,ethereum)
-
-deploy-optimism-adapters-test:
-	$(call deploy_fn,Adapters/DeployOpAdapter,ethereum)
-
-deploy-metis-adapters-test:
-	$(call deploy_fn,Adapters/DeployMetisAdapter,ethereum)
-
-deploy-base-adapters-test:
-	$(call deploy_fn,Adapters/DeployCBaseAdapter,ethereum)
-
-## Set sender bridge dapters. Only eth pol avax are needed as other networks will only receive
-set-ccf-sender-adapters-test:
-	$(call deploy_fn,CCC/Set_CCF_Sender_Adapters,avalanche)
-
-# Set the bridge adapters allowed to receive messages
-set-ccr-receiver-adapters-test:
-	$(call deploy_fn,CCC/Set_CCR_Receivers_Adapters,celo)
-
-# Sets the required confirmations
-set-ccr-confirmations-test:
-	$(call deploy_fn,CCC/Set_CCR_Confirmations,ethereum)
-
-# Funds CCC
-fund-crosschain-test:
-	$(call deploy_fn,CCC/FundCCC,ethereum)
-
-## Deploy and configure all contracts
-deploy-full-test:
-		#make deploy-proxy-factory-test
-		make deploy-cross-chain-infra-test
-		make deploy-ccip-bridge-adapters-test
-		make deploy-lz-bridge-adapters-test
-		make deploy-hl-bridge-adapters-test
-		make deploy-same-chain-adapters-test
-		make set-ccf-sender-adapters-test
-		make set-ccr-receiver-adapters-test
-		make set-ccr-confirmations-test
-		make fund-crosschain-test
-		make write-json-addresses
-
-
-
-# ----------------------------------------------------------------------------------------------------------------------
-# ----------------------------------------- HELPER SCRIPTS ---------------------------------------------------------
-remove-bridge-adapters:
-	$(call deploy_fn,helpers/RemoveBridgeAdapters,celo)
-
-send-direct-message:
-	$(call deploy_fn,helpers/Send_Direct_CCMessage,avalanche)
-
-deploy_mock_destination:
-	$(call deploy_fn,helpers/Deploy_Mock_destination,ethereum)
-
-set-approved-ccf-senders:
-	$(call deploy_fn,helpers/Set_Approved_Senders,ethereum)
-
-send-message:
-	@$(call deploy_fn,helpers/Testnet_ForwardMessage,ethereum,Testnet_ForwardMessage)
-
-deploy_mock_ccc:
-	$(call deploy_fn,helpers/mocks/Deploy_Mock_CCC,zkevm)
-
-send-message-via-adapter:
-	$(call deploy_fn,helpers/Send_Message_Via_Adapter,ethereum)
-
-deploy-ccc-revision-and-update:
-	$(call deploy_fn,CCC/UpdateCCC,ethereum)
-
-deploy-ccc-update-payload:
-	$(call deploy_fn,helpers/UpdateCCCImpl_Payload,celo)