diff --git a/.github/workflows/CONTRIBUTING.ms b/.github/workflows/CONTRIBUTING.ms new file mode 100644 index 00000000..217718d1 --- /dev/null +++ b/.github/workflows/CONTRIBUTING.ms @@ -0,0 +1,91 @@ +# Contributing + +Thanks for your interest in contributing to the Aave Delivery Infrastructure! Please take a moment to review this document **before submitting a pull request.** + +## Rules + +1. Significant changes to the Protocol must be reviewed before a Pull Request is created. Create a [Feature Request](https://github.com/aave-dao/aave-delivery-infrastructure/issues) first to discuss your ideas. +2. Contributors must be humans, not bots. +3. First time contributions must not contain only spelling or grammatical fixes. + +## Basic guide + +This guide is intended to help you get started with contributing. By following these steps, you will understand the development process and workflow. + +1. [Forking the repository](#forking-the-repository) +2. [Installing Foundry](#installing-foundry) +4. [Installing dependencies](#installing-dependencies) +5. [Running the test suite](#running-the-test-suite) +7. [Submitting a pull request](#submitting-a-pull-request) +8. [Versioning](#versioning) + +--- + +### Forking the repository + +To start contributing to the project, [fork it](https://github.com/aave-dao/aave-delivery-infrastructure/fork) to your private github account. + +Once that is done, you can clone your forked repository to your local machine. +```bash +# https +git clone https://github.com//aave-delivery-infrastructure.git +# ssh +git clone git@github.com:/aave-delivery-infrastructure.git +``` + +To stay up to date with the main repository, you can add it as a remote. +```bash +# https +git remote add upstream https://github.com/aave-dao/aave-delivery-infrastructure.git +# ssh +git remote add upstream git@github.com:aave-dao/aave-delivery-infrastructure.git +``` + +--- + +### Installing foundry + +Aave Delivery Infrastructure is a [Foundry](https://github.com/foundry-rs/foundry) project. + +Install foundry using the following command: + +```bash +curl -L https://foundry.paradigm.xyz | bash +``` + +--- + +### Installing dependencies + +For generating the changelog, linting and testing, we rely on some additional node packages. You can install them by running: + +```bash +npm install +``` + +--- + +### Running the test suite + +For running the default test suite you can use the following command: + +```bash +forge test +``` + +--- + +### Submitting a pull request + +When you're ready to submit a pull request, you can follow these naming conventions: + +- Pull request titles use the [Imperative Mood](https://en.wikipedia.org/wiki/Imperative_mood) (e.g., `Add something`, `Fix something`). +- [Changesets](#versioning) use past tense verbs (e.g., `Added something`, `Fixed something`). + +When you submit a pull request, GitHub will automatically lint, build, and test your changes. If you see an ❌, it's most likely a bug in your code. Please, inspect the logs through the GitHub UI to find the cause. + +- Pull requests must always cover all the changes made with tests. If you're adding a new feature, you must also add a test for it. If you're fixing a bug, you must add a test that reproduces the bug. Pull requests that cause a regression in test coverage will not be accepted. +- Pull requests that touch code functionality should always include updated gas snapshots. Running `forge test` will update the snapshots for you. +- Make sure that your updates are fitting within the existing code margin. You can check by running `forge build --sizes` + +--- diff --git a/.github/workflows/certora-review-controller.yml b/.github/workflows/certora-review-controller.yml deleted file mode 100644 index a6d6e1e6..00000000 --- a/.github/workflows/certora-review-controller.yml +++ /dev/null @@ -1,56 +0,0 @@ -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.20/solc-static-linux - chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc8.20 - - - 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 - - diff --git a/.github/workflows/certora-review-forwarder.yml b/.github/workflows/certora-review-forwarder.yml deleted file mode 100644 index 3ecbf4c5..00000000 --- a/.github/workflows/certora-review-forwarder.yml +++ /dev/null @@ -1,60 +0,0 @@ -name: certora-review-forwarder - -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==7.6.3 - - - name: Install solc - run: | - wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux - chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc8.20 - - - 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: - - verifyCrossChainForwarder-envelopRetry.conf - - verifyCrossChainForwarder-invariants.conf - - verifyCrossChainForwarder-newEnvelope.conf - - verifyCrossChainForwarder-sanity.conf - - verifyCrossChainForwarder-simpleRules.conf - - verifyCrossChainForwarder-encode-decode-correct.conf --rule encode_decode_well_formed_TX - - verifyCrossChainForwarder-shuffle.conf diff --git a/.github/workflows/certora-review-receiver.yml b/.github/workflows/certora-review-receiver.yml deleted file mode 100644 index 0f9ee687..00000000 --- a/.github/workflows/certora-review-receiver.yml +++ /dev/null @@ -1,56 +0,0 @@ -name: certora-review-receiver - -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==7.6.3 - - - name: Install solc - run: | - wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux - chmod +x solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc8.20 - - - 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: - - verifyCrossChainReceiver.conf - - diff --git a/.github/workflows/certora-review.yml b/.github/workflows/certora-review.yml new file mode 100644 index 00000000..dde34689 --- /dev/null +++ b/.github/workflows/certora-review.yml @@ -0,0 +1,60 @@ +name: certora + +concurrency: + group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +on: + pull_request: + branches: + - '*' + push: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + if: + github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' && + github.ref == format('refs/heads/{0}', github.event.repository.default_branch)) + permissions: + contents: read + statuses: write + pull-requests: write + id-token: write + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + + - name: Munged + run: | + cd security/certora + touch applyHarness.patch + make munged + + - uses: Certora/certora-run-action@v2 + with: + cli-version: 7.31.2 + configurations: |- + security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf + security/certora/confs/verifyCrossChainForwarder-invariants.conf + security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf + security/certora/confs/verifyCrossChainForwarder-sanity.conf + security/certora/confs/verifyCrossChainForwarder-simpleRules.conf + security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf --rule encode_decode_well_formed_TX + security/certora/confs/verifyCrossChainForwarder-shuffle.conf + security/certora/confs/verifyCrossChainReceiver.conf + security/certora/confs/verifyCrossChainControllerWithEmergency.conf + solc-versions: 0.8.20 + comment-fail-only: false + solc-remove-version-prefix: "0." + job-name: "Certora Prover Run" + certora-key: ${{ secrets.CERTORAKEY }} + install-java: true + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + diff --git a/.github/workflows/comment.yml b/.github/workflows/comment.yml new file mode 100644 index 00000000..64c960a6 --- /dev/null +++ b/.github/workflows/comment.yml @@ -0,0 +1,23 @@ +name: PR Comment + +on: + workflow_run: + # The workflow generating the artifacts + workflows: [Test] + types: + - completed + +permissions: + actions: read + issues: write + checks: read + statuses: read + pull-requests: write + +jobs: + comment: + uses: bgd-labs/github-workflows/.github/workflows/comment.yml@main + secrets: + # the provided PAT needs write and write permissions on issues and pull requests + # the PAT is only really needed when commenting of prs from forks + READ_ONLY_PAT: ${{ secrets.READ_ONLY_PAT }} \ No newline at end of file diff --git a/README.md b/README.md index 3cd7e2ef..dabaf189 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,7 @@ All the information about setup of the project and deployments can be found [HER | Network | CrossChainController | Forwards to | Receives from | Consensus | |------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------|------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -|
Ethereum

Ethereum

| [0xEd42a7D8559a463722Ca4beD50E0Cc05a386b0e1](https://etherscan.io/address/0xEd42a7D8559a463722Ca4beD50E0Cc05a386b0e1) | Polygon Avalanche Arbitrum Optimism Binance Base Metis Gnosis

Scroll

| Avalanche Polygon |

Avalanche

2/3

Polygon

3/4

| +|
Ethereum

Ethereum

| [0xEd42a7D8559a463722Ca4beD50E0Cc05a386b0e1](https://etherscan.io/address/0xEd42a7D8559a463722Ca4beD50E0Cc05a386b0e1) | Polygon Avalanche Arbitrum Optimism Binance Base Metis Gnosis Scroll Celo Linea Sonic SoneiumZkSyncInk

| Avalanche Polygon |

Avalanche

2/3

Polygon

3/4

| |
Polygon

Polygon

| [0xF6B99959F0b5e79E1CC7062E12aF632CEb18eF0d](https://polygonscan.com/address/0xF6B99959F0b5e79E1CC7062E12aF632CEb18eF0d) | Ethereum | Ethereum |
Ethereum

3/4

| |
Avalanche

Avalanche

| [0x27FC7D54C893dA63C0AE6d57e1B2B13A70690928](https://snowtrace.io/address/0x27FC7D54C893dA63C0AE6d57e1B2B13A70690928) | Ethereum | Ethereum |
Ethereum

2/3

| |
Arbitrum

Arbitrum

| [0xCbFB78a3Eeaa611b826E37c80E4126c8787D29f0](https://arbiscan.io/address/0xCbFB78a3Eeaa611b826E37c80E4126c8787D29f0) | - | Ethereum |
Ethereum

1/1

| @@ -39,7 +39,12 @@ All the information about setup of the project and deployments can be found [HER |
Gnosis

Gnosis

| [0x8Dc5310fc9D3D7D1Bb3D1F686899c8F082316c9F](https://gnosisscan.io/address/0x8Dc5310fc9D3D7D1Bb3D1F686899c8F082316c9F) | - | Ethereum |
Ethereum

2/3

| |
Scroll

Scroll

| [0x03073D3F4769f6b6604d616238fD6c636C99AD0A](https://scrollscan.com/address/0x03073D3F4769f6b6604d616238fD6c636C99AD0A) | - | Ethereum |
Ethereum

1/1

| |
ZkEVM

ZkEVM

| [0xed7e0874526B9BB9E36C7e9472ed7ed324CEeE3B](https://zkevm.polygonscan.com/address/0xed7e0874526B9BB9E36C7e9472ed7ed324CEeE3B) | - | Ethereum |
Ethereum

1/1

| -|
Celo

Celo

| [0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79](https://zkevm.polygonscan.com/address/0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79) | - | Ethereum |
Ethereum

1/1

| +|
Celo

Celo

| [0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79](https://celoscan.io/address/0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79) | - | Ethereum |
Ethereum

1/1

| +|
Linea

Linea

| [0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79](https://lineascan.build/address/0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79) | - | Ethereum |
Ethereum

1/1

| +|
Sonic

Sonic

| [0x58e003a3C6f2Aeed6a2a6Bc77B504566523cb15c](https://sonicscan.org/address/0x58e003a3C6f2Aeed6a2a6Bc77B504566523cb15c) | - | Ethereum |
Ethereum

1/1

| +|
Soneium

Soneium

| [0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79](https://soneium.blockscout.com/address/0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79) | - | Ethereum |
Ethereum

1/1

| +|
ZkSync

ZkSync

| [0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79](https://era.zksync.network/address/0x4A5f4b29C0407E5Feb323305e121f563c7bC4d79) | - | Ethereum |
Ethereum

1/1

+|
Ink

Ink

| [0x990B75fD1a2345D905a385dBC6e17BEe0Cb2f505](https://explorer.inkonchain.com/address/0x990B75fD1a2345D905a385dBC6e17BEe0Cb2f505) | - | Ethereum |
Ethereum

1/1

|
@@ -56,7 +61,9 @@ All the information about setup of the project and deployments can be found [HER |
Gnosis

Gnosis

| - | [0xf937ffaea1363e4fa260760bdfa2aa8fc911f84d](https://gnosisscan.io/address/0xf937ffaea1363e4fa260760bdfa2aa8fc911f84d) | |
Scroll

Scroll

| - | - | |
ZkEVM

ZkEVM

| - | - | -|
Celo

Celo

| - | [0x91b21900E91CD302EBeD05E45D8f270ddAED944d](https://gnosisscan.io/address/0x91b21900E91CD302EBeD05E45D8f270ddAED944d) | +|
Celo

Celo

| - | [0x91b21900E91CD302EBeD05E45D8f270ddAED944d](https://gnosisscan.io/address/0x91b21900E91CD302EBeD05E45D8f270ddAED944d) +|
Sonic

Sonic

| - | [0xECB564e91f620fBFb59d0C4A41d7f10aDb0D1934](https://sonicscan.org/address/0xECB564e91f620fBFb59d0C4A41d7f10aDb0D1934) +|
Ink

Ink

| - | - |
diff --git a/docs/networks/ink.svg b/docs/networks/ink.svg new file mode 100644 index 00000000..1b347674 --- /dev/null +++ b/docs/networks/ink.svg @@ -0,0 +1,10 @@ + + + + + + + + + + diff --git a/docs/networks/linea.svg b/docs/networks/linea.svg new file mode 100644 index 00000000..f6d4deb0 --- /dev/null +++ b/docs/networks/linea.svg @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/docs/networks/soneium.svg b/docs/networks/soneium.svg new file mode 100644 index 00000000..52160a06 --- /dev/null +++ b/docs/networks/soneium.svg @@ -0,0 +1,14 @@ + + + + + + + + + + + + + + diff --git a/docs/networks/sonic.svg b/docs/networks/sonic.svg new file mode 100644 index 00000000..53607727 --- /dev/null +++ b/docs/networks/sonic.svg @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/docs/networks/zksync.svg b/docs/networks/zksync.svg new file mode 100644 index 00000000..b5db4015 --- /dev/null +++ b/docs/networks/zksync.svg @@ -0,0 +1,4 @@ + + + + diff --git a/lib/solidity-utils b/lib/solidity-utils index 94b1392e..bf955b86 160000 --- a/lib/solidity-utils +++ b/lib/solidity-utils @@ -1 +1 @@ -Subproject commit 94b1392e43190f998d4af2cb4e604ec0866a6798 +Subproject commit bf955b866b9f6c90b9cc2d099b94fc37ee53c542 diff --git a/security/certora/applyHarness.patch b/security/certora/applyHarness.patch index f0ecc703..bca0640d 100644 --- a/security/certora/applyHarness.patch +++ b/security/certora/applyHarness.patch @@ -1,14 +1,14 @@ diff -ruN .gitignore .gitignore --- .gitignore 1970-01-01 02:00:00.000000000 +0200 -+++ .gitignore 2023-09-14 14:23:45.279003572 +0300 ++++ .gitignore 2025-08-05 18:13:11.368089637 +0300 @@ -0,0 +1,2 @@ +* +!.gitignore \ No newline at end of file diff -ruN src/contracts/CrossChainForwarder.sol src/contracts/CrossChainForwarder.sol ---- src/contracts/CrossChainForwarder.sol 2023-09-14 23:39:12.458049170 +0300 -+++ src/contracts/CrossChainForwarder.sol 2023-09-14 23:23:52.854487614 +0300 -@@ -278,36 +278,36 @@ +--- src/contracts/CrossChainForwarder.sol 2025-08-13 14:51:48.742535847 +0300 ++++ src/contracts/CrossChainForwarder.sol 2025-08-05 18:13:11.368089637 +0300 +@@ -335,36 +335,36 @@ uint256 destinationChainId, uint256 gasLimit, ChainIdBridgeConfig[] memory bridgeAdapters @@ -67,7 +67,7 @@ diff -ruN src/contracts/CrossChainForwarder.sol src/contracts/CrossChainForwarde } return (isForwardedAtLeastOnce); -@@ -361,11 +361,11 @@ +@@ -418,11 +418,11 @@ if (!configFound) { // preparing fees stream diff --git a/security/certora/confs/verifyCrossChainControllerWithEmergency.conf b/security/certora/confs/verifyCrossChainControllerWithEmergency.conf index 0aeb5dd7..908c0b53 100644 --- a/security/certora/confs/verifyCrossChainControllerWithEmergency.conf +++ b/security/certora/confs/verifyCrossChainControllerWithEmergency.conf @@ -2,16 +2,16 @@ "files": [ "security/certora/harness/CrossChainControllerWithEmergencyModeHarness.sol", ], + "packages": [ + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + ], "hashing_length_bound": "288", "loop_iter": "1", "msg": "All CrosschainControllerWithEmergency rules", "optimistic_hashing": true, "optimistic_loop": true, - "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", - ], "process": "emv", "prover_args": [ " -copyLoopUnroll 8" diff --git a/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf b/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf index ae2a6934..329f2b5b 100644 --- a/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf +++ b/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarnessED:security/certora/specs/CrossChainForwarder-encode-decode-correct.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf b/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf index b1ccd3ed..ad2a0539 100644 --- a/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf +++ b/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-envelopRetry.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-invariants.conf b/security/certora/confs/verifyCrossChainForwarder-invariants.conf index bcebfa2b..abed2a1f 100644 --- a/security/certora/confs/verifyCrossChainForwarder-invariants.conf +++ b/security/certora/confs/verifyCrossChainForwarder-invariants.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/invariants.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf b/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf index f8b83a75..06040597 100644 --- a/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf +++ b/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-newEnvelope.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-sanity.conf b/security/certora/confs/verifyCrossChainForwarder-sanity.conf index 461ea773..2776a5d5 100644 --- a/security/certora/confs/verifyCrossChainForwarder-sanity.conf +++ b/security/certora/confs/verifyCrossChainForwarder-sanity.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-sanity.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-shuffle.conf b/security/certora/confs/verifyCrossChainForwarder-shuffle.conf index c797053f..87ed7b82 100644 --- a/security/certora/confs/verifyCrossChainForwarder-shuffle.conf +++ b/security/certora/confs/verifyCrossChainForwarder-shuffle.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-shuffle.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf b/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf index b8fd0323..0a993c38 100644 --- a/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf +++ b/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf @@ -5,9 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/solidity-utils/src", - "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "solidity-utils=lib/solidity-utils/src", + "forge-std=lib/solidity-utils/lib/forge-std/src", + "openzeppelin-contracts=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-simpleRules.spec", "solc": "solc8.20", diff --git a/security/certora/confs/verifyCrossChainReceiver.conf b/security/certora/confs/verifyCrossChainReceiver.conf index 118acb3a..0b55dbdf 100644 --- a/security/certora/confs/verifyCrossChainReceiver.conf +++ b/security/certora/confs/verifyCrossChainReceiver.conf @@ -2,8 +2,8 @@ "files": [ "security/certora/harness/CrossChainReceiverHarness.sol", "security/certora/harness/BaseReceiverPortalDummy.sol", - "src/contracts/libs/EncodingUtils.sol:TransactionUtils", - "src/contracts/libs/EncodingUtils.sol:EnvelopeUtils" + "security/certora/munged/src/contracts/libs/EncodingUtils.sol:TransactionUtils", + "security/certora/munged/src/contracts/libs/EncodingUtils.sol:EnvelopeUtils" ], "hashing_length_bound": "320", "loop_iter": "2", @@ -13,7 +13,7 @@ "packages": [ "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/solidity-utils/lib/forge-std/src", - "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/", + "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", ], "process": "emv", "prover_args": [ diff --git a/security/certora/harness/BaseCrossChainControllerHarness.sol b/security/certora/harness/BaseCrossChainControllerHarness.sol index a94f57ce..16c94335 100644 --- a/security/certora/harness/BaseCrossChainControllerHarness.sol +++ b/security/certora/harness/BaseCrossChainControllerHarness.sol @@ -1,6 +1,6 @@ pragma solidity ^0.8.8; -import {BaseCrossChainController} from '../../../src/contracts/BaseCrossChainController.sol'; +import {BaseCrossChainController} from '../munged/src/contracts/BaseCrossChainController.sol'; import {CrossChainReceiverHarnessAbstract} from './CrossChainReceiverHarnessAbstract.sol'; contract BaseCrossChainControllerHarness is BaseCrossChainController, CrossChainReceiverHarnessAbstract { diff --git a/security/certora/harness/CrossChainControllerWithEmergencyModeHarness.sol b/security/certora/harness/CrossChainControllerWithEmergencyModeHarness.sol index 25e01ae8..813e36eb 100644 --- a/security/certora/harness/CrossChainControllerWithEmergencyModeHarness.sol +++ b/security/certora/harness/CrossChainControllerWithEmergencyModeHarness.sol @@ -1,6 +1,7 @@ pragma solidity ^0.8.8; -import {CrossChainControllerWithEmergencyMode} from '../../../src/contracts/CrossChainControllerWithEmergencyMode.sol'; +//import {CrossChainControllerWithEmergencyMode} from '../../../src/contracts/CrossChainControllerWithEmergencyMode.sol'; +import {CrossChainControllerWithEmergencyMode} from '../munged/src/contracts/CrossChainControllerWithEmergencyMode.sol'; import {BaseCrossChainControllerHarness} from './BaseCrossChainControllerHarness.sol'; contract CrossChainControllerWithEmergencyModeHarness is diff --git a/security/certora/harness/CrossChainReceiverHarness.sol b/security/certora/harness/CrossChainReceiverHarness.sol index 5a31bac8..5168acfb 100644 --- a/security/certora/harness/CrossChainReceiverHarness.sol +++ b/security/certora/harness/CrossChainReceiverHarness.sol @@ -1,7 +1,7 @@ pragma solidity ^0.8.8; import {CrossChainReceiverHarnessAbstract} from './CrossChainReceiverHarnessAbstract.sol'; -import {CrossChainReceiver} from '../../../src/contracts/CrossChainReceiver.sol'; +import {CrossChainReceiver} from '../munged/src/contracts/CrossChainReceiver.sol'; contract CrossChainReceiverHarness is CrossChainReceiverHarnessAbstract { diff --git a/security/certora/harness/CrossChainReceiverHarnessAbstract.sol b/security/certora/harness/CrossChainReceiverHarnessAbstract.sol index 215e67d1..38392504 100644 --- a/security/certora/harness/CrossChainReceiverHarnessAbstract.sol +++ b/security/certora/harness/CrossChainReceiverHarnessAbstract.sol @@ -1,10 +1,10 @@ pragma solidity ^0.8.8; -import {CrossChainReceiver} from '../../../src/contracts/CrossChainReceiver.sol'; -import {Envelope, Transaction, TransactionUtils} from '../../../src/contracts/libs/EncodingUtils.sol'; -import {EnumerableSet} from '../../../src/contracts/interfaces/ICrossChainReceiver.sol'; -import {Errors} from '../../../src/contracts/libs/Errors.sol'; -import {IBaseReceiverPortal} from '../../../src/contracts/interfaces/IBaseReceiverPortal.sol'; +import {CrossChainReceiver} from '../munged/src/contracts/CrossChainReceiver.sol'; +import {Envelope, Transaction, TransactionUtils} from '../munged/src/contracts/libs/EncodingUtils.sol'; +import {EnumerableSet} from '../munged/src/contracts/interfaces/ICrossChainReceiver.sol'; +import {Errors} from '../munged/src/contracts/libs/Errors.sol'; +import {IBaseReceiverPortal} from '../munged/src/contracts/interfaces/IBaseReceiverPortal.sol'; abstract contract CrossChainReceiverHarnessAbstract is CrossChainReceiver { @@ -74,4 +74,4 @@ abstract contract CrossChainReceiverHarnessAbstract is CrossChainReceiver { } - \ No newline at end of file + diff --git a/security/certora/scripts/CrossChainForwarder-encode-decode-correct.sh b/security/certora/scripts/CrossChainForwarder-encode-decode-correct.sh deleted file mode 100644 index f769e360..00000000 --- a/security/certora/scripts/CrossChainForwarder-encode-decode-correct.sh +++ /dev/null @@ -1,26 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg \"$1::$2\"" -fi - -echo "RULE is ==>" $RULE "<==" - -eval \ -certoraRun --send_only \ - --fe_version latest \ - security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf $RULE $MSG - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/CrossChainForwarder-envelopRetry.sh b/security/certora/scripts/CrossChainForwarder-envelopRetry.sh deleted file mode 100644 index 3c457fc3..00000000 --- a/security/certora/scripts/CrossChainForwarder-envelopRetry.sh +++ /dev/null @@ -1,26 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg \"$1:: $2\"" -fi - -echo "RULE is ==>" $RULE "<==" - -eval \ -certoraRun --send_only \ - --fe_version latest \ - certora/confs/CrossChainForwarder-envelopRetry.conf $RULE $MSG - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/CrossChainForwarder-invariants.sh b/security/certora/scripts/CrossChainForwarder-invariants.sh deleted file mode 100644 index f8cd2b32..00000000 --- a/security/certora/scripts/CrossChainForwarder-invariants.sh +++ /dev/null @@ -1,31 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg \"$1:: $2\" " -fi - -echo "RULE is ==>" $RULE "<==" - -eval \ -certoraRun --send_only \ - --fe_version latest \ - certora/confs/CrossChainForwarder-invariants.conf $RULE $MSG - -#echo "CMD is ==>"$CMD"<==" - - -#eval $CMD - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/CrossChainForwarder-newEnvelope.sh b/security/certora/scripts/CrossChainForwarder-newEnvelope.sh deleted file mode 100644 index 09ac7cfb..00000000 --- a/security/certora/scripts/CrossChainForwarder-newEnvelope.sh +++ /dev/null @@ -1,25 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg $1:: $2" -fi - -echo "RULE is ==>" $RULE "<==" - -certoraRun --send_only \ - --fe_version latest \ - security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf $RULE $MSG - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/CrossChainForwarder-run-all.sh b/security/certora/scripts/CrossChainForwarder-run-all.sh deleted file mode 100644 index f2b328a3..00000000 --- a/security/certora/scripts/CrossChainForwarder-run-all.sh +++ /dev/null @@ -1,16 +0,0 @@ - -certoraRun security/certora/confs/verifyCrossChainForwarder-sanity.conf - -certoraRun security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf - -certoraRun security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf - -certoraRun security/certora/confs/verifyCrossChainForwarder-simpleRules.conf - -certoraRun security/certora/confs/verifyCrossChainForwarder-invariants.conf - -certoraRun security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf \ - --rule encode_decode_well_formed_TX - -certoraRun security/certora/confs/verifyCrossChainForwarder-shuffle.conf - diff --git a/security/certora/scripts/CrossChainForwarder-sanity.sh b/security/certora/scripts/CrossChainForwarder-sanity.sh deleted file mode 100644 index b8101db0..00000000 --- a/security/certora/scripts/CrossChainForwarder-sanity.sh +++ /dev/null @@ -1,26 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg \"$1::$2\"" -fi - -echo "RULE is ==>" $RULE "<==" - -eval \ -certoraRun --send_only \ - --fe_version latest \ - security/certora/confs/verifyCrossChainForwarder-sanity.conf $RULE $MSG - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/CrossChainForwarder-simpleRules.sh b/security/certora/scripts/CrossChainForwarder-simpleRules.sh deleted file mode 100644 index 79552425..00000000 --- a/security/certora/scripts/CrossChainForwarder-simpleRules.sh +++ /dev/null @@ -1,26 +0,0 @@ -if [[ "$1" ]] -then - RULE="--rule $1" - MSG="--msg \"$1::$2\"" -fi - -echo "RULE is ==>" $RULE "<==" - -eval \ -certoraRun --send_only \ - --fe_version latest \ - security/certora/confs/verifyCrossChainForwarder-simpleRules.conf $RULE $MSG - - - - -# --server staging \ -# --prover_version jaroslav/UCNotNullFix \ -# --prover_version master \ -# --typecheck_only \ - - -# --method "retryTransaction(bytes,uint256,address[])" \ -# --method "disableBridgeAdapters_single((address,uint256[])[])" \ -# --method "retryEnvelope((uint256,address,address,uint256,uint256,bytes),uint256)" \ - diff --git a/security/certora/scripts/run-all.sh b/security/certora/scripts/run-all.sh new file mode 100644 index 00000000..8f76f131 --- /dev/null +++ b/security/certora/scripts/run-all.sh @@ -0,0 +1,52 @@ +CMN="--compilation_steps_only" + + +echo +echo "******** 1. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-sanity.conf \ + --msg "1. " + +echo +echo "******** 2. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf \ + --msg "2. " + +echo +echo "******** 3. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf \ + --msg "3. " + +echo +echo "******** 4. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-simpleRules.conf \ + --msg "4. " + +echo +echo "******** 5. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-invariants.conf \ + --msg "5. " + +echo +echo "******** 6. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf \ + --rule encode_decode_well_formed_TX \ + --msg "6. " + +echo +echo "******** 7. Running: ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainForwarder-shuffle.conf \ + --msg "7. " + + +echo +echo "******** 8. Running: All Receiver Rules ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainReceiver.conf \ + --msg "8. All Receiver Rules " + + +echo +echo "******** 9. Running: verifyCrossChainControllerWithEmergency.conf ****************" +certoraRun $CMN security/certora/confs/verifyCrossChainControllerWithEmergency.conf \ + --msg "9. verifyCrossChainControllerWithEmergency.conf" + + diff --git a/security/certora/specs/CrossChainControllerWithEmergencyMode.spec b/security/certora/specs/CrossChainControllerWithEmergencyMode.spec index 3619de35..124d9411 100644 --- a/security/certora/specs/CrossChainControllerWithEmergencyMode.spec +++ b/security/certora/specs/CrossChainControllerWithEmergencyMode.spec @@ -6,6 +6,10 @@ methods{ // declared in ICLEmergencyOracle.sol // function _.latestRoundData() external returns (uint80,int256,uint256,uint256,uint80) => NONDET; function _.latestRoundData() external => NONDET; + + // The following should be change to a DISPATCHER. Naftali is working to allow delegatecall to be dispatched. + function _.forwardMessage(address receiver,uint256 executionGasLimit,uint256 destinationChainId,bytes message) + external => NONDET; } definition is_invalidating_function(method f) returns bool = diff --git a/security/certora/specs/CrossChainReceiver.spec b/security/certora/specs/CrossChainReceiver.spec index 3954bd0c..df77a728 100644 --- a/security/certora/specs/CrossChainReceiver.spec +++ b/security/certora/specs/CrossChainReceiver.spec @@ -803,11 +803,11 @@ rule disallowReceiverBridgeAdapters_cannot_allow_witness_consequent // Internal property 11: If there are allowedBridges configured, requiredConfirmation must be configured to a positive value rule requiredConfirmation_is_positive_after_updateConfirmations(uint256 chainId) { - env e; - ICrossChainReceiver.ConfirmationInput[] newConfirmations; - updateConfirmations(e, newConfirmations); - // assuming that newConfirmations is not empty! - assert newConfirmations[0].chainId == chainId => getRequiredConfirmation(chainId) > 0; + env e; + ICrossChainReceiver.ConfirmationInput[] newConfirmations; + updateConfirmations(e, newConfirmations); + // assuming that newConfirmations is not empty! + assert (newConfirmations.length >0 && newConfirmations[0].chainId == chainId) => getRequiredConfirmation(chainId) > 0; } // Internal property #13: @@ -970,20 +970,19 @@ rule only_single_bridge_adapter_removed } -rule checkUpdateMessagesValidityTimestamp{ - - env e; - ICrossChainReceiver.ValidityTimestampInput[] newValidityTimestamp; - - updateMessagesValidityTimestamp(e, newValidityTimestamp); - - uint256 chainId; - uint120 validityTimestamp = getValidityTimestamp(chainId); - - bool no_duplicate_chainId = newValidityTimestamp[0].chainId != newValidityTimestamp[1].chainId && newValidityTimestamp.length <= 2; - - assert newValidityTimestamp[0].chainId == chainId && no_duplicate_chainId => newValidityTimestamp[0].validityTimestamp == validityTimestamp; - assert newValidityTimestamp[1].chainId == chainId && no_duplicate_chainId => newValidityTimestamp[1].validityTimestamp == validityTimestamp; +rule checkUpdateMessagesValidityTimestamp { + env e; + ICrossChainReceiver.ValidityTimestampInput[] newValidityTimestamp; + + updateMessagesValidityTimestamp(e, newValidityTimestamp); + + uint256 chainId; + uint120 validityTimestamp = getValidityTimestamp(chainId); + + bool no_duplicate_chainId = newValidityTimestamp[0].chainId != newValidityTimestamp[1].chainId && newValidityTimestamp.length == 2; + + assert newValidityTimestamp[0].chainId == chainId && no_duplicate_chainId => newValidityTimestamp[0].validityTimestamp == validityTimestamp; + assert newValidityTimestamp[1].chainId == chainId && no_duplicate_chainId => newValidityTimestamp[1].validityTimestamp == validityTimestamp; }