diff --git a/.github/workflows/certora-arbitrum.yaml b/.github/workflows/certora-arbitrum.yaml new file mode 100644 index 0000000..1860f4a --- /dev/null +++ b/.github/workflows/certora-arbitrum.yaml @@ -0,0 +1,74 @@ +name: certora-arbitrum + +on: + push: + branches: + - main + - l2-bridges-audit + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Check key + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + run: echo "key length" ${#CERTORAKEY} + + - 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: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.10 + + - name: Verify rule ${{ matrix.rule }} + run: | + cd certora + touch applyHarness.patch + make munged + cd .. + echo "key length" ${#CERTORAKEY} + sh certora/scripts/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifyArbitrum.sh executedValidTransition2 + - verifyArbitrum.sh onlyCancelCanCancel + - verifyArbitrum.sh onlyQueuedAreExecuted + - verifyArbitrum.sh expiredForever + - verifyArbitrum.sh actionNotCanceledAndExecuted + - verifyArbitrum.sh properDelay + - verifyArbitrum.sh notCanceledNotExecuted + - verifyArbitrum.sh minDelayLtMaxDelay + - verifyArbitrum.sh whoChangedStateVariables + - verifyArbitrum.sh executeCannotCancel + - verifyArbitrum.sh whoChangesActionsSetState + - verifyArbitrum.sh canceledForever + - verifyArbitrum.sh executedForever + - verifyArbitrum.sh executeRevertsBeforeDelay + - verifyArbitrum.sh noIncarnations1 noIncarnations2 noIncarnations3 + - verifyArbitrum.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued queue2Reachability cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive diff --git a/.github/workflows/certora-optimism.yaml b/.github/workflows/certora-optimism.yaml new file mode 100644 index 0000000..b3cc2fe --- /dev/null +++ b/.github/workflows/certora-optimism.yaml @@ -0,0 +1,74 @@ +name: certora-optimism + +on: + push: + branches: + - main + - l2-bridges-audit + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Check key + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + run: echo "key length" ${#CERTORAKEY} + + - 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: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.10 + + - name: Verify rule ${{ matrix.rule }} + run: | + cd certora + touch applyHarness.patch + make munged + cd .. + echo "key length" ${#CERTORAKEY} + sh certora/scripts/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifyOptimism.sh executedValidTransition2 + - verifyOptimism.sh onlyCancelCanCancel + - verifyOptimism.sh onlyQueuedAreExecuted + - verifyOptimism.sh expiredForever + - verifyOptimism.sh actionNotCanceledAndExecuted + - verifyOptimism.sh properDelay + - verifyOptimism.sh notCanceledNotExecuted + - verifyOptimism.sh minDelayLtMaxDelay + - verifyOptimism.sh whoChangedStateVariables + - verifyOptimism.sh executeCannotCancel + - verifyOptimism.sh whoChangesActionsSetState + - verifyOptimism.sh canceledForever + - verifyOptimism.sh executedForever + - verifyOptimism.sh executeRevertsBeforeDelay + - verifyOptimism.sh noIncarnations1 noIncarnations2 noIncarnations3 + - verifyOptimism.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued queue2Reachability cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive diff --git a/.github/workflows/certora-polygon.yaml b/.github/workflows/certora-polygon.yaml new file mode 100644 index 0000000..b5f20a6 --- /dev/null +++ b/.github/workflows/certora-polygon.yaml @@ -0,0 +1,74 @@ +name: certora-polygon + +on: + push: + branches: + - main + - l2-bridges-audit + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Check key + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + run: echo "key length" ${#CERTORAKEY} + + - 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: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.10 + + - name: Verify rule ${{ matrix.rule }} + run: | + cd certora + touch applyHarness.patch + make munged + cd .. + echo "key length" ${#CERTORAKEY} + sh certora/scripts/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifyPolygon.sh executedValidTransition2 + - verifyPolygon.sh onlyCancelCanCancel + - verifyPolygon.sh onlyQueuedAreExecuted + - verifyPolygon.sh expiredForever + - verifyPolygon.sh actionNotCanceledAndExecuted + - verifyPolygon.sh properDelay + - verifyPolygon.sh notCanceledNotExecuted + - verifyPolygon.sh minDelayLtMaxDelay + - verifyPolygon.sh whoChangedStateVariables + - verifyPolygon.sh executeCannotCancel + - verifyPolygon.sh whoChangesActionsSetState + - verifyPolygon.sh canceledForever + - verifyPolygon.sh executedForever + - verifyPolygon.sh executeRevertsBeforeDelay + - verifyPolygon.sh noIncarnations1 noIncarnations2 noIncarnations3 + - verifyPolygon.sh actionDuplicate holdYourHorses executeFailsIfExpired executedValidTransition1 queuePriviliged afterQueueHashQueued cancelPriviliged independentQueuedActions queueCannotCancel queueDoesntModifyStateVariables queuedStateConsistency queuedChangedCounter sameExecutionTimesReverts cancelExclusive diff --git a/.gitignore b/.gitignore index dca277a..8dac275 100644 --- a/.gitignore +++ b/.gitignore @@ -22,4 +22,9 @@ coverage.json .DS_Store -deployments/ \ No newline at end of file +deployments/ + +# Certora +.certora* +.last_confs +certora_* diff --git a/README.md b/README.md index 4466eb2..f558e05 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,8 @@ The `L2BridgeExecutor` abstract contract extends `BridgeExecutorBase` in order t ## Audits -- [MixBytes (12/08/21)](./audits/12-08-2021_MixBytes_AaveGovernanceCrosschainBridges.pdf) +- [MixBytes - Bridge contracts for Polygon (12/08/21)](./audits/12-08-2021_MixBytes_AaveGovernanceCrosschainBridges.pdf) +- [ChainSecurity - Bridge contracts for Optimism and Arbitrum (26/07/22)](./audits/26-07-2022_ChainSecurity_AaveL2BridgeExecutors.pdf) ## Getting Started diff --git a/audits/26-07-2022_ChainSecurity_AaveL2BridgeExecutors.pdf b/audits/26-07-2022_ChainSecurity_AaveL2BridgeExecutors.pdf new file mode 100644 index 0000000..a3afd36 Binary files /dev/null and b/audits/26-07-2022_ChainSecurity_AaveL2BridgeExecutors.pdf differ diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 0000000..e47c83b --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1,5 @@ +# certora +.certora* +.certora*.json +**.last_conf* +certora-logs diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 0000000..0e33459 --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,24 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../contracts +MUNGED_DIR = munged + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + cp -r $(CONTRACTS_DIR) $@ + patch -p0 -d $@ < $(PATCH) + +record: + diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./contracts/++g' | sed 's+munged/++g' > $(PATCH) + +clean: + git clean -fdX + touch $(PATCH) + diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..99a7860 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,28 @@ +## Verification Overview +The current directory contains Certora's formal verification of AAVE's L2 bridge protocol. +In this directory you will find three subdirectories: + +1. specs - Contains all the specification files that were written by Certora for the bridge protocol. We have created two spec files, `Optimism_ArbitrumBridge.spec`, `PolygonBridge.spec`, the first is used to verify Optimism and Arbitrum executors and the second for Polygon. The choice for this separation relies on the contracts inhertiance of these three bridges protocols. +We emphasize that essentially the rules in both specs are the same (by context, name and logical idea), but the implementation might be a bit different due to implementation differences (for example the name given to the 'external queue' function.) + +2. scripts - Contains all the necessary run scripts to execute the spec files on the Certora Prover. These scripts composed of a run command of Certora Prover, contracts to take into account in the verification context, declaration of the compiler and a set of additional settings. Each script is named after the bridge type it verifies. Note that the Optimism and Arbitrum bridges are verified by the same spec file, but have separate scripts. + +3. harness - Contains all the inheriting contracts that add/simplify functionalities to the original contract. You will also find a set of symbolic and dummy implementations of external contracts on which the executors rely. +These harnesses, i.e. extensions/simplifications, are necessary to run the verifications. Assumptions and under-approximations are also done in a few places, in order to supply partial coverage where full coverage is not achievable. +One harness worth explaining is the mockTarget and mockTargetPoly contracts that were created in order to simualte the low-level calls of the executed transactions. + +
+ +--- + +## Running Instructions +To run a verification job: + +1. Open terminal and `cd` your way to the main AAVE L2 repository. + +2. Run the script you'd like to get results for: + ``` + sh certora/scripts/verifyOptimism.sh + ``` + +
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch new file mode 100644 index 0000000..932ffe5 --- /dev/null +++ b/certora/applyHarness.patch @@ -0,0 +1,136 @@ +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00.000000000 +0200 ++++ .gitignore 2022-08-03 12:50:10.000000000 +0300 +@@ -0,0 +1,2 @@ ++* ++!.gitignore +diff -ruN bridges/BridgeExecutorBase.sol bridges/BridgeExecutorBase.sol +--- bridges/BridgeExecutorBase.sol 2022-07-31 16:38:17.000000000 +0300 ++++ bridges/BridgeExecutorBase.sol 2022-07-31 16:35:45.000000000 +0300 +@@ -15,7 +15,7 @@ + uint256 constant MINIMUM_GRACE_PERIOD = 10 minutes; + + // Time between queuing and execution +- uint256 private _delay; ++ uint256 internal _delay; // harness: private -> internal + // Time after the execution time during which the actions set can be executed + uint256 private _gracePeriod; + // Minimum allowed delay +@@ -24,13 +24,12 @@ + uint256 private _maximumDelay; + // Address with the ability of canceling actions sets + address private _guardian; +- + // Number of actions sets +- uint256 private _actionsSetCounter; ++ uint256 internal _actionsSetCounter; // harness: private -> internal + // Map of registered actions sets (id => ActionsSet) +- mapping(uint256 => ActionsSet) private _actionsSets; +- // Map of queued actions (actionHash => isQueued) +- mapping(bytes32 => bool) private _queuedActions; ++ mapping(uint256 => ActionsSet) internal _actionsSets; // harness: private -> internal ++ // Map of queued actions sets (actionHash => isQueued) ++ mapping(bytes32 => bool) internal _queuedActions; // harness: private -> internal + + /** + * @dev Only guardian can call functions marked by this modifier. +@@ -162,11 +161,13 @@ + _validateDelay(_delay); + } + ++ // Certora : added virtual + /// @inheritdoc IExecutorBase + function executeDelegateCall(address target, bytes calldata data) + external + payable + override ++ virtual + onlyThis + returns (bool, bytes memory) + { +@@ -312,7 +313,7 @@ + unchecked { + ++i; + } +- } ++ } + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + actionsSet.targets = targets; +@@ -333,6 +334,7 @@ + ); + } + ++ // harness : added virtual + function _executeTransaction( + address target, + uint256 value, +@@ -340,7 +342,7 @@ + bytes memory data, + uint256 executionTime, + bool withDelegatecall +- ) internal returns (bytes memory) { ++ ) internal virtual returns (bytes memory) { + if (address(this).balance < value) revert InsufficientBalance(); + + bytes32 actionHash = keccak256( +@@ -385,8 +387,9 @@ + if (delay > _maximumDelay) revert DelayLongerThanMax(); + } + ++ // harness: private to internal + function _verifyCallResult(bool success, bytes memory returnData) +- private ++ internal + pure + returns (bytes memory) + { +diff -ruN bridges/L2BridgeExecutor.sol bridges/L2BridgeExecutor.sol +--- bridges/L2BridgeExecutor.sol 2022-05-25 20:17:05.000000000 +0300 ++++ bridges/L2BridgeExecutor.sol 2022-07-31 16:35:45.000000000 +0300 +@@ -42,6 +42,7 @@ + } + + /// @inheritdoc IL2BridgeExecutor ++ // Certora harness : removed _queue() + function queue( + address[] memory targets, + uint256[] memory values, +@@ -49,7 +50,7 @@ + bytes[] memory calldatas, + bool[] memory withDelegatecalls + ) external onlyEthereumGovernanceExecutor { +- _queue(targets, values, signatures, calldatas, withDelegatecalls); ++ //_queue(targets, values, signatures, calldatas, withDelegatecalls); + } + + /// @inheritdoc IL2BridgeExecutor +diff -ruN bridges/PolygonBridgeExecutor.sol bridges/PolygonBridgeExecutor.sol +--- bridges/PolygonBridgeExecutor.sol 2022-05-25 20:17:05.000000000 +0300 ++++ bridges/PolygonBridgeExecutor.sol 2022-07-31 16:35:45.000000000 +0300 +@@ -30,9 +30,9 @@ + event FxChildUpdate(address oldFxChild, address newFxChild); + + // Address of the FxRoot Sender, sending the cross-chain transaction from Ethereum +- address private _fxRootSender; ++ address internal _fxRootSender; // Certora harness: private -> internal + // Address of the FxChild, in charge of redirecting cross-chain transactions in Polygon +- address private _fxChild; ++ address internal _fxChild; // Certora harness: private -> internal + + /** + * @dev Only FxChild can call functions marked by this modifier. +@@ -67,11 +67,12 @@ + } + + /// @inheritdoc IFxMessageProcessor ++ // Certora harness: added virtual + function processMessageFromRoot( + uint256 stateId, + address rootMessageSender, + bytes calldata data +- ) external override onlyFxChild { ++ ) external override virtual onlyFxChild { + if (rootMessageSender != _fxRootSender) revert UnauthorizedRootOrigin(); + + address[] memory targets; diff --git a/certora/harness/ArbitrumHarness.sol b/certora/harness/ArbitrumHarness.sol new file mode 100644 index 0000000..9f80c24 --- /dev/null +++ b/certora/harness/ArbitrumHarness.sol @@ -0,0 +1,94 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {AddressAliasHelper} from '../../contracts/dependencies/arbitrum/AddressAliasHelper.sol'; +import {L2BridgeExecutorHarness} from './L2BridgeExecutorHarness.sol'; +import {mockTarget} from './mockTarget.sol'; + + +/** + * @title ArbitrumBridgeExecutor + * @author Aave + * @notice Implementation of the Arbitrum Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the L2 Address Alias of the L1 EthereumGovernanceExecutor + */ +contract ArbitrumHarness is L2BridgeExecutorHarness { + // Address of the Optimism L2 Cross Domain Messenger, in charge of redirecting cross-chain transactions in L2 + mockTarget public _mock; + + /// @inheritdoc L2BridgeExecutorHarness + modifier onlyEthereumGovernanceExecutor() override { + if (AddressAliasHelper.undoL1ToL2Alias(msg.sender) != _ethereumGovernanceExecutor) + revert UnauthorizedEthereumExecutor(); + _; + } + + /** + * @dev Constructor + * + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) + L2BridgeExecutorHarness( + ethereumGovernanceExecutor, + delay, + gracePeriod, + minimumDelay, + maximumDelay, + guardian + ) + { + } + + function _executeTransaction( + address target, + uint256 value, + string memory signature, + bytes memory data, + uint256 executionTime, + bool withDelegatecall + ) internal override returns (bytes memory) { + if (address(this).balance < value) revert InsufficientBalance(); + + bytes32 actionHash = keccak256( + abi.encode(target, value, executionTime) + ); + _queuedActions[actionHash] = false; + + bool success; + bytes memory resultData; + if (withDelegatecall) { + (success, resultData) = this.executeDelegateCall{value: value}(target, data); + } else { + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + } + return _verifyCallResult(success, resultData); + } + + function executeDelegateCall(address target, bytes calldata data) + external + payable + override + onlyThis + returns (bool, bytes memory) + { + bool success; + bytes memory resultData; + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + return (success, resultData); + } +} diff --git a/certora/harness/DummyERC20A.sol b/certora/harness/DummyERC20A.sol new file mode 100644 index 0000000..188b926 --- /dev/null +++ b/certora/harness/DummyERC20A.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import "./DummyERC20Impl.sol"; + +contract DummyERC20A is DummyERC20Impl {} \ No newline at end of file diff --git a/certora/harness/DummyERC20B.sol b/certora/harness/DummyERC20B.sol new file mode 100644 index 0000000..0f97f1e --- /dev/null +++ b/certora/harness/DummyERC20B.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import "./DummyERC20Impl.sol"; + +contract DummyERC20B is DummyERC20Impl {} \ No newline at end of file diff --git a/certora/harness/DummyERC20Impl.sol b/certora/harness/DummyERC20Impl.sol new file mode 100644 index 0000000..42e7f23 --- /dev/null +++ b/certora/harness/DummyERC20Impl.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +// with mint +contract DummyERC20Impl { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) external returns (bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return true; + } + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} \ No newline at end of file diff --git a/certora/harness/L2BridgeExecutorHarness.sol b/certora/harness/L2BridgeExecutorHarness.sol new file mode 100644 index 0000000..efca3b6 --- /dev/null +++ b/certora/harness/L2BridgeExecutorHarness.sol @@ -0,0 +1,169 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {L2BridgeExecutor} from '../munged/bridges/L2BridgeExecutor.sol'; + +/** + * @title BridgeExecutorBase + * @author Aave + * @notice Abstract contract that implements basic executor functionality + * @dev It does not implement an external `queue` function. This should instead be done in the inheriting + * contract with proper access control + */ +abstract contract L2BridgeExecutorHarness is L2BridgeExecutor { + modifier onlyEthereumGovernanceExecutor() override virtual; + /** + * @dev Constructor + * + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) L2BridgeExecutor(ethereumGovernanceExecutor, delay, gracePeriod, + minimumDelay, maximumDelay, guardian){} + + /* + * @notice Queue an ActionsSet + * @dev If a signature is empty, calldata is used for the execution, calldata is appended to signature otherwise + * @param targets Array of targets to be called by the actions set + * @param values Array of values to pass in each call by the actions set + * @param signatures Array of function signatures to encode in each call (can be empty) + * @param calldatas Array of calldata to pass in each call (can be empty) + * @param withDelegatecalls Array of whether to delegatecall for each call + **/ + + function queue2( + address[2] memory targets, + uint256[2] memory values, + string[2] memory signatures, + bytes[2] memory calldatas, + bool[2] memory withDelegatecalls + ) external onlyEthereumGovernanceExecutor { + _queue2(targets, values, signatures, calldatas, withDelegatecalls); + } + + function _queue2( + address[2] memory targets, + uint256[2] memory values, + string[2] memory signatures, + bytes[2] memory calldatas, + bool[2] memory withDelegatecalls + ) internal { + if (targets.length == 0) revert EmptyTargets(); + uint256 targetsLength = targets.length; + if ( + targetsLength != values.length || + targetsLength != signatures.length || + targetsLength != calldatas.length || + targetsLength != withDelegatecalls.length + ) revert InconsistentParamsLength(); + + uint256 actionsSetId = _actionsSetCounter; + uint256 executionTime = block.timestamp + _delay; + unchecked { + ++_actionsSetCounter; + } + + for (uint256 i = 0; i < targetsLength; ) { + bytes32 actionHash = keccak256( + abi.encode( + targets[i], + values[i], + executionTime + ) + ); + if (isActionQueued(actionHash)) revert DuplicateAction(); + _queuedActions[actionHash] = true; + unchecked { + ++i; + } + } + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + actionsSet.targets = targets; + actionsSet.values = values; + //actionsSet.signatures = signatures; + //actionsSet.calldatas = calldatas; + //actionsSet.withDelegatecalls = withDelegatecalls; + actionsSet.executionTime = executionTime; + + for (uint256 j = 0; j < targetsLength; ) { + actionsSet.withDelegatecalls[j] = withDelegatecalls[j]; + unchecked { + ++j; + } + } + } + + // Certora : add getters + function getActionsSetLength(uint256 actionsSetId) + public view returns (uint256) + { + return _actionsSets[actionsSetId].targets.length; + } + + function getActionsSetExecutionTime(uint256 actionsSetId) + public view returns (uint256) + { + return _actionsSets[actionsSetId].executionTime; + } + + function getActionsSetTarget(uint256 actionsSetId, uint256 i) + public view returns (address) + { + return _actionsSets[actionsSetId].targets[i]; + } + + function getActionSetWithDelegate(uint256 actionsSetId, uint256 i) + public view returns (bool) + { + return _actionsSets[actionsSetId].withDelegatecalls[i]; + } + + function getActionsSetCalldata(uint256 actionsSetId, uint256 i) + public view returns (bytes memory) + { + return _actionsSets[actionsSetId].calldatas[i]; + } + + function getActionsSetCanceled(uint256 actionsSetId) + public view returns(bool) + { + return _actionsSets[actionsSetId].canceled; + } + + function getActionsSetExecuted(uint256 actionsSetId) + public view returns(bool) + { + return _actionsSets[actionsSetId].executed; + } + + function noDelegateCalls(uint256 actionsSetId) external onlyThis + { + uint256 length = getActionsSetLength(actionsSetId); + for (uint256 i = 0; i < length; ) { + _actionsSets[actionsSetId].withDelegatecalls[i] = false; + unchecked { + ++i; + } + } + } + + function ID2actionHash(uint256 actionsSetId, uint i) public view returns (bytes32) + { + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + return keccak256( + abi.encode(actionsSet.targets[i], actionsSet.values[i], + actionsSet.executionTime)); + } +} diff --git a/certora/harness/OptimismHarness.sol b/certora/harness/OptimismHarness.sol new file mode 100644 index 0000000..9a772d4 --- /dev/null +++ b/certora/harness/OptimismHarness.sol @@ -0,0 +1,104 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {ICrossDomainMessenger} from '../munged/dependencies/optimism/interfaces/ICrossDomainMessenger.sol'; +import {L2BridgeExecutorHarness} from './L2BridgeExecutorHarness.sol'; +import {mockTarget} from './mockTarget.sol'; + + +/** + * @title OptimismBridgeExecutor + * @author Aave + * @notice Implementation of the Optimism Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the Optimism L2 Cross Domain Messenger and having + * the EthereumGovernanceExecutor as xDomainMessageSender + */ +contract OptimismHarness is L2BridgeExecutorHarness { + // Address of the Optimism L2 Cross Domain Messenger, in charge of redirecting cross-chain transactions in L2 + address public immutable OVM_L2_CROSS_DOMAIN_MESSENGER; + // Certora : replace xDomainMessageSender by a known address. + address private _domainMsgSender; + mockTarget public _mock; + + /// @inheritdoc L2BridgeExecutorHarness + // Certora: removed call to domainMessageSender and replaced with address variable. + modifier onlyEthereumGovernanceExecutor() override { + if ( + msg.sender != OVM_L2_CROSS_DOMAIN_MESSENGER || + _domainMsgSender !=_ethereumGovernanceExecutor + ) revert UnauthorizedEthereumExecutor(); + _; + } + + /** + * @dev Constructor + * + * @param ovmL2CrossDomainMessenger The address of the Optimism L2CrossDomainMessenger + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ovmL2CrossDomainMessenger, + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) + L2BridgeExecutorHarness( + ethereumGovernanceExecutor, + delay, + gracePeriod, + minimumDelay, + maximumDelay, + guardian + ) + { + OVM_L2_CROSS_DOMAIN_MESSENGER = ovmL2CrossDomainMessenger; + } + + function _executeTransaction( + address target, + uint256 value, + string memory signature, + bytes memory data, + uint256 executionTime, + bool withDelegatecall + ) internal override returns (bytes memory) { + if (address(this).balance < value) revert InsufficientBalance(); + + bytes32 actionHash = keccak256( + abi.encode(target, value, executionTime) + ); + _queuedActions[actionHash] = false; + + bool success; + bytes memory resultData; + if (withDelegatecall) { + (success, resultData) = this.executeDelegateCall{value: value}(target, data); + } else { + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + } + return _verifyCallResult(success, resultData); + } + + function executeDelegateCall(address target, bytes calldata data) + external + payable + override + onlyThis + returns (bool, bytes memory) + { + bool success; + bytes memory resultData; + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + return (success, resultData); + } +} diff --git a/certora/harness/PolygonHarness.sol b/certora/harness/PolygonHarness.sol new file mode 100644 index 0000000..84e333d --- /dev/null +++ b/certora/harness/PolygonHarness.sol @@ -0,0 +1,215 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {PolygonBridgeExecutor} from '../munged/bridges/PolygonBridgeExecutor.sol'; +import {mockTargetPoly} from './mockTargetPoly.sol'; + +/** + * @title PolygonBridgeExecutor + * @author Aave + * @notice Implementation of the Polygon Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the FxChild and after passing the EthereumGovernanceExecutor check + * as the FxRoot sender + */ +contract PolygonHarness is PolygonBridgeExecutor { + mockTargetPoly public _mock; + /** + * @dev Constructor + * + * @param fxRootSender The address of the transaction sender in FxRoot + * @param fxChild The address of the FxChild + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address fxRootSender, + address fxChild, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) PolygonBridgeExecutor(fxRootSender, fxChild, delay, gracePeriod, minimumDelay, maximumDelay, guardian) { + } + + // Certora harness: limit to 2 actions in set. + function processMessageFromRoot( + uint256 stateId, + address rootMessageSender, + bytes calldata data + ) external override onlyFxChild { + if (rootMessageSender != _fxRootSender) revert UnauthorizedRootOrigin(); + + address[2] memory targets; + uint256[2] memory values; + string[2] memory signatures; + bytes[2] memory calldatas; + bool[2] memory withDelegatecalls; + + (targets, values, signatures, calldatas, withDelegatecalls) = + abi.decode( + data, + (address[2], uint256[2], string[2], bytes[2], bool[2]) + ); + + _queue2(targets, values, signatures, calldatas, withDelegatecalls); + } + + function _executeTransaction( + address target, + uint256 value, + string memory signature, + bytes memory data, + uint256 executionTime, + bool withDelegatecall + ) internal override returns (bytes memory) { + if (address(this).balance < value) revert InsufficientBalance(); + + bytes32 actionHash = keccak256( + abi.encode(target, value, executionTime) + ); + _queuedActions[actionHash] = false; + + bool success; + bytes memory resultData; + if (withDelegatecall) { + (success, resultData) = this.executeDelegateCall{value: value}(target, data); + } else { + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + } + return _verifyCallResult(success, resultData); + } + + function executeDelegateCall(address target, bytes calldata data) + external + payable + override + onlyThis + returns (bool, bytes memory) + { + bool success; + bytes memory resultData; + // solium-disable-next-line security/no-call-value + success = _mock.targetCall(data); + return (success, resultData); + } + + function _queue2( + address[2] memory targets, + uint256[2] memory values, + string[2] memory signatures, + bytes[2] memory calldatas, + bool[2] memory withDelegatecalls + ) internal { + if (targets.length == 0) revert EmptyTargets(); + uint256 targetsLength = targets.length; + if ( + targetsLength != values.length || + targetsLength != signatures.length || + targetsLength != calldatas.length || + targetsLength != withDelegatecalls.length + ) revert InconsistentParamsLength(); + + uint256 actionsSetId = _actionsSetCounter; + uint256 executionTime = block.timestamp + _delay; + unchecked { + ++_actionsSetCounter; + } + + for (uint256 i = 0; i < targetsLength; ) { + bytes32 actionHash = keccak256( + abi.encode( + targets[i], + values[i], + executionTime + ) + ); + if (isActionQueued(actionHash)) revert DuplicateAction(); + _queuedActions[actionHash] = true; + unchecked { + ++i; + } + } + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + actionsSet.targets = targets; + actionsSet.values = values; + //actionsSet.signatures = signatures; + //actionsSet.calldatas = calldatas; + //actionsSet.withDelegatecalls = withDelegatecalls; + actionsSet.executionTime = executionTime; + + for (uint256 j = 0; j < targetsLength; ) { + actionsSet.withDelegatecalls[j] = withDelegatecalls[j]; + unchecked { + ++j; + } + } + } + + // Certora : add getters + function getActionsSetLength(uint256 actionsSetId) + public view returns (uint256) + { + return _actionsSets[actionsSetId].targets.length; + } + + function getActionsSetExecutionTime(uint256 actionsSetId) + public view returns (uint256) + { + return _actionsSets[actionsSetId].executionTime; + } + + function getActionsSetTarget(uint256 actionsSetId, uint256 i) + public view returns (address) + { + return _actionsSets[actionsSetId].targets[i]; + } + + function getActionSetWithDelegate(uint256 actionsSetId, uint256 i) + public view returns (bool) + { + return _actionsSets[actionsSetId].withDelegatecalls[i]; + } + + function getActionsSetCalldata(uint256 actionsSetId, uint256 i) + public view returns (bytes memory) + { + return _actionsSets[actionsSetId].calldatas[i]; + } + + function getActionsSetCanceled(uint256 actionsSetId) + public view returns(bool) + { + return _actionsSets[actionsSetId].canceled; + } + + function getActionsSetExecuted(uint256 actionsSetId) + public view returns(bool) + { + return _actionsSets[actionsSetId].executed; + } + + function noDelegateCalls(uint256 actionsSetId) external onlyThis + { + uint256 length = getActionsSetLength(actionsSetId); + for (uint256 i = 0; i < length; ) { + _actionsSets[actionsSetId].withDelegatecalls[i] = false; + unchecked { + ++i; + } + } + } + + function ID2actionHash(uint256 actionsSetId, uint i) public view returns (bytes32) + { + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + return keccak256( + abi.encode(actionsSet.targets[i], actionsSet.values[i], + actionsSet.executionTime)); + } +} diff --git a/certora/harness/mockTarget.sol b/certora/harness/mockTarget.sol new file mode 100644 index 0000000..3ae848d --- /dev/null +++ b/certora/harness/mockTarget.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import {OptimismHarness} from './OptimismHarness.sol'; +import {DummyERC20Impl} from './DummyERC20Impl.sol'; + +// target call mock target for Optimism bridge +contract mockTarget +{ + OptimismHarness public _executor; + DummyERC20Impl private _tokenA; + DummyERC20Impl private _tokenB; + address private _account1; + address private _account2; + uint256 private _amount1; + uint256 private _amount2; + + function targetCall(bytes memory data) external returns (bool output) + { + uint8 funcId = abi.decode(data, (uint8)); + if (funcId == 1 ){ + _executor.updateMinimumDelay(_amount1); + } + else if (funcId == 2){ + _executor.updateDelay(_amount1); + } + else if (funcId == 3){ + _executor.updateEthereumGovernanceExecutor(_account1); + } + else if (funcId == 4){ + _executor.updateGracePeriod(_amount1); + } + else if (funcId == 5) { + _executor.cancel(_amount2); + } + else if (funcId == 6) { + output = _tokenA.transfer(_account1, _amount1); + return output; + } + else if (funcId == 7) { + output = _tokenB.transfer(_account2, _amount2); + return output; + } + else { + // Reverting path + return false; + } + return true; + } + + function tokenA() public view returns (DummyERC20Impl) + { + return _tokenA; + } + + function tokenB() public view returns (DummyERC20Impl) + { + return _tokenB; + } + + function getTransferArguments() public view + returns(address, address, uint256, uint256) { + return (_account1, _account2, _amount1, _amount2); + } +} \ No newline at end of file diff --git a/certora/harness/mockTargetPoly.sol b/certora/harness/mockTargetPoly.sol new file mode 100644 index 0000000..bf8c35e --- /dev/null +++ b/certora/harness/mockTargetPoly.sol @@ -0,0 +1,67 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import {PolygonHarness} from './PolygonHarness.sol'; +import {DummyERC20Impl} from './DummyERC20Impl.sol'; + +// target call mock target for Polygon bridge +contract mockTargetPoly +{ + PolygonHarness public _executor; + DummyERC20Impl private _tokenA; + DummyERC20Impl private _tokenB; + address private _account1; + address private _account2; + uint256 private _amount1; + uint256 private _amount2; + + function targetCall(bytes memory data) external returns (bool output) + { + uint8 funcId = abi.decode(data, (uint8)); + if (funcId == 1 ){ + _executor.updateMinimumDelay(_amount1); + } + else if (funcId == 2){ + _executor.updateDelay(_amount1); + } + else if (funcId == 3){ + _executor.updateFxRootSender(_account1); + } + else if (funcId == 4){ + _executor.updateGracePeriod(_amount1); + } + else if (funcId == 5) { + _executor.cancel(_amount2); + } + else if (funcId == 6) { + output = _tokenA.transfer(_account1, _amount1); + return output; + } + else if (funcId == 7) { + output = _tokenB.transfer(_account2, _amount2); + return output; + } + else if (funcId == 8) { + _executor.updateFxChild(_account2); + } + else { + // Reverting path + return false; + } + return true; + } + + function tokenA() public view returns (DummyERC20Impl) + { + return _tokenA; + } + + function tokenB() public view returns (DummyERC20Impl) + { + return _tokenB; + } + + function getTransferArguments() public view + returns(address, address, uint256, uint256) { + return (_account1, _account2, _amount1, _amount2); + } +} \ No newline at end of file diff --git a/certora/munged/bridges/ArbitrumBridgeExecutor.sol b/certora/munged/bridges/ArbitrumBridgeExecutor.sol new file mode 100644 index 0000000..09e54ca --- /dev/null +++ b/certora/munged/bridges/ArbitrumBridgeExecutor.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {AddressAliasHelper} from '../dependencies/arbitrum/AddressAliasHelper.sol'; +import {L2BridgeExecutor} from './L2BridgeExecutor.sol'; + +/** + * @title ArbitrumBridgeExecutor + * @author Aave + * @notice Implementation of the Arbitrum Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the L2 Address Alias of the L1 EthereumGovernanceExecutor + */ +contract ArbitrumBridgeExecutor is L2BridgeExecutor { + /// @inheritdoc L2BridgeExecutor + modifier onlyEthereumGovernanceExecutor() override { + if (AddressAliasHelper.undoL1ToL2Alias(msg.sender) != _ethereumGovernanceExecutor) + revert UnauthorizedEthereumExecutor(); + _; + } + + /** + * @dev Constructor + * + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) + L2BridgeExecutor( + ethereumGovernanceExecutor, + delay, + gracePeriod, + minimumDelay, + maximumDelay, + guardian + ) + { + // Intentionally left blank + } +} diff --git a/certora/munged/bridges/BridgeExecutorBase.sol b/certora/munged/bridges/BridgeExecutorBase.sol new file mode 100644 index 0000000..64d9c92 --- /dev/null +++ b/certora/munged/bridges/BridgeExecutorBase.sol @@ -0,0 +1,413 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {IExecutorBase} from '../interfaces/IExecutorBase.sol'; + +/** + * @title BridgeExecutorBase + * @author Aave + * @notice Abstract contract that implements basic executor functionality + * @dev It does not implement an external `queue` function. This should instead be done in the inheriting + * contract with proper access control + */ +abstract contract BridgeExecutorBase is IExecutorBase { + // Minimum allowed grace period, which reduces the risk of having an actions set expire due to network congestion + uint256 constant MINIMUM_GRACE_PERIOD = 10 minutes; + + // Time between queuing and execution + uint256 internal _delay; // harness: private -> internal + // Time after the execution time during which the actions set can be executed + uint256 private _gracePeriod; + // Minimum allowed delay + uint256 private _minimumDelay; + // Maximum allowed delay + uint256 private _maximumDelay; + // Address with the ability of canceling actions sets + address private _guardian; + // Number of actions sets + uint256 internal _actionsSetCounter; // harness: private -> internal + // Map of registered actions sets (id => ActionsSet) + mapping(uint256 => ActionsSet) internal _actionsSets; // harness: private -> internal + // Map of queued actions sets (actionHash => isQueued) + mapping(bytes32 => bool) internal _queuedActions; // harness: private -> internal + + /** + * @dev Only guardian can call functions marked by this modifier. + **/ + modifier onlyGuardian() { + if (msg.sender != _guardian) revert NotGuardian(); + _; + } + + /** + * @dev Only this contract can call functions marked by this modifier. + **/ + modifier onlyThis() { + if (msg.sender != address(this)) revert OnlyCallableByThis(); + _; + } + + /** + * @dev Constructor + * + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) { + if ( + gracePeriod < MINIMUM_GRACE_PERIOD || + minimumDelay >= maximumDelay || + delay < minimumDelay || + delay > maximumDelay + ) revert InvalidInitParams(); + + _updateDelay(delay); + _updateGracePeriod(gracePeriod); + _updateMinimumDelay(minimumDelay); + _updateMaximumDelay(maximumDelay); + _updateGuardian(guardian); + } + + /// @inheritdoc IExecutorBase + function execute(uint256 actionsSetId) external payable override { + if (getCurrentState(actionsSetId) != ActionsSetState.Queued) revert OnlyQueuedActions(); + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + if (block.timestamp < actionsSet.executionTime) revert TimelockNotFinished(); + + actionsSet.executed = true; + uint256 actionCount = actionsSet.targets.length; + + bytes[] memory returnedData = new bytes[](actionCount); + for (uint256 i = 0; i < actionCount; ) { + returnedData[i] = _executeTransaction( + actionsSet.targets[i], + actionsSet.values[i], + actionsSet.signatures[i], + actionsSet.calldatas[i], + actionsSet.executionTime, + actionsSet.withDelegatecalls[i] + ); + unchecked { + ++i; + } + } + + emit ActionsSetExecuted(actionsSetId, msg.sender, returnedData); + } + + /// @inheritdoc IExecutorBase + function cancel(uint256 actionsSetId) external override onlyGuardian { + if (getCurrentState(actionsSetId) != ActionsSetState.Queued) revert OnlyQueuedActions(); + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + actionsSet.canceled = true; + + uint256 targetsLength = actionsSet.targets.length; + for (uint256 i = 0; i < targetsLength; ) { + _cancelTransaction( + actionsSet.targets[i], + actionsSet.values[i], + actionsSet.signatures[i], + actionsSet.calldatas[i], + actionsSet.executionTime, + actionsSet.withDelegatecalls[i] + ); + unchecked { + ++i; + } + } + + emit ActionsSetCanceled(actionsSetId); + } + + /// @inheritdoc IExecutorBase + function updateGuardian(address guardian) external override onlyThis { + _updateGuardian(guardian); + } + + /// @inheritdoc IExecutorBase + function updateDelay(uint256 delay) external override onlyThis { + _validateDelay(delay); + _updateDelay(delay); + } + + /// @inheritdoc IExecutorBase + function updateGracePeriod(uint256 gracePeriod) external override onlyThis { + if (gracePeriod < MINIMUM_GRACE_PERIOD) revert GracePeriodTooShort(); + _updateGracePeriod(gracePeriod); + } + + /// @inheritdoc IExecutorBase + function updateMinimumDelay(uint256 minimumDelay) external override onlyThis { + if (minimumDelay >= _maximumDelay) revert MinimumDelayTooLong(); + _updateMinimumDelay(minimumDelay); + _validateDelay(_delay); + } + + /// @inheritdoc IExecutorBase + function updateMaximumDelay(uint256 maximumDelay) external override onlyThis { + if (maximumDelay <= _minimumDelay) revert MaximumDelayTooShort(); + _updateMaximumDelay(maximumDelay); + _validateDelay(_delay); + } + + // Certora : added virtual + /// @inheritdoc IExecutorBase + function executeDelegateCall(address target, bytes calldata data) + external + payable + override + virtual + onlyThis + returns (bool, bytes memory) + { + bool success; + bytes memory resultData; + // solium-disable-next-line security/no-call-value + (success, resultData) = target.delegatecall(data); + return (success, resultData); + } + + /// @inheritdoc IExecutorBase + function receiveFunds() external payable override {} + + /// @inheritdoc IExecutorBase + function getDelay() external view override returns (uint256) { + return _delay; + } + + /// @inheritdoc IExecutorBase + function getGracePeriod() external view override returns (uint256) { + return _gracePeriod; + } + + /// @inheritdoc IExecutorBase + function getMinimumDelay() external view override returns (uint256) { + return _minimumDelay; + } + + /// @inheritdoc IExecutorBase + function getMaximumDelay() external view override returns (uint256) { + return _maximumDelay; + } + + /// @inheritdoc IExecutorBase + function getGuardian() external view override returns (address) { + return _guardian; + } + + /// @inheritdoc IExecutorBase + function getActionsSetCount() external view override returns (uint256) { + return _actionsSetCounter; + } + + /// @inheritdoc IExecutorBase + function getActionsSetById(uint256 actionsSetId) + external + view + override + returns (ActionsSet memory) + { + return _actionsSets[actionsSetId]; + } + + /// @inheritdoc IExecutorBase + function getCurrentState(uint256 actionsSetId) public view override returns (ActionsSetState) { + if (_actionsSetCounter <= actionsSetId) revert InvalidActionsSetId(); + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + if (actionsSet.canceled) { + return ActionsSetState.Canceled; + } else if (actionsSet.executed) { + return ActionsSetState.Executed; + } else if (block.timestamp > actionsSet.executionTime + _gracePeriod) { + return ActionsSetState.Expired; + } else { + return ActionsSetState.Queued; + } + } + + /// @inheritdoc IExecutorBase + function isActionQueued(bytes32 actionHash) public view override returns (bool) { + return _queuedActions[actionHash]; + } + + function _updateGuardian(address guardian) internal { + emit GuardianUpdate(_guardian, guardian); + _guardian = guardian; + } + + function _updateDelay(uint256 delay) internal { + emit DelayUpdate(_delay, delay); + _delay = delay; + } + + function _updateGracePeriod(uint256 gracePeriod) internal { + emit GracePeriodUpdate(_gracePeriod, gracePeriod); + _gracePeriod = gracePeriod; + } + + function _updateMinimumDelay(uint256 minimumDelay) internal { + emit MinimumDelayUpdate(_minimumDelay, minimumDelay); + _minimumDelay = minimumDelay; + } + + function _updateMaximumDelay(uint256 maximumDelay) internal { + emit MaximumDelayUpdate(_maximumDelay, maximumDelay); + _maximumDelay = maximumDelay; + } + + /** + * @notice Queue an ActionsSet + * @dev If a signature is empty, calldata is used for the execution, calldata is appended to signature otherwise + * @param targets Array of targets to be called by the actions set + * @param values Array of values to pass in each call by the actions set + * @param signatures Array of function signatures to encode in each call (can be empty) + * @param calldatas Array of calldata to pass in each call (can be empty) + * @param withDelegatecalls Array of whether to delegatecall for each call + **/ + function _queue( + address[] memory targets, + uint256[] memory values, + string[] memory signatures, + bytes[] memory calldatas, + bool[] memory withDelegatecalls + ) internal { + if (targets.length == 0) revert EmptyTargets(); + uint256 targetsLength = targets.length; + if ( + targetsLength != values.length || + targetsLength != signatures.length || + targetsLength != calldatas.length || + targetsLength != withDelegatecalls.length + ) revert InconsistentParamsLength(); + + uint256 actionsSetId = _actionsSetCounter; + uint256 executionTime = block.timestamp + _delay; + unchecked { + ++_actionsSetCounter; + } + + for (uint256 i = 0; i < targetsLength; ) { + bytes32 actionHash = keccak256( + abi.encode( + targets[i], + values[i], + signatures[i], + calldatas[i], + executionTime, + withDelegatecalls[i] + ) + ); + if (isActionQueued(actionHash)) revert DuplicateAction(); + _queuedActions[actionHash] = true; + unchecked { + ++i; + } + } + + ActionsSet storage actionsSet = _actionsSets[actionsSetId]; + actionsSet.targets = targets; + actionsSet.values = values; + actionsSet.signatures = signatures; + actionsSet.calldatas = calldatas; + actionsSet.withDelegatecalls = withDelegatecalls; + actionsSet.executionTime = executionTime; + + emit ActionsSetQueued( + actionsSetId, + targets, + values, + signatures, + calldatas, + withDelegatecalls, + executionTime + ); + } + + // harness : added virtual + function _executeTransaction( + address target, + uint256 value, + string memory signature, + bytes memory data, + uint256 executionTime, + bool withDelegatecall + ) internal virtual returns (bytes memory) { + if (address(this).balance < value) revert InsufficientBalance(); + + bytes32 actionHash = keccak256( + abi.encode(target, value, signature, data, executionTime, withDelegatecall) + ); + _queuedActions[actionHash] = false; + + bytes memory callData; + if (bytes(signature).length == 0) { + callData = data; + } else { + callData = abi.encodePacked(bytes4(keccak256(bytes(signature))), data); + } + + bool success; + bytes memory resultData; + if (withDelegatecall) { + (success, resultData) = this.executeDelegateCall{value: value}(target, callData); + } else { + // solium-disable-next-line security/no-call-value + (success, resultData) = target.call{value: value}(callData); + } + return _verifyCallResult(success, resultData); + } + + function _cancelTransaction( + address target, + uint256 value, + string memory signature, + bytes memory data, + uint256 executionTime, + bool withDelegatecall + ) internal { + bytes32 actionHash = keccak256( + abi.encode(target, value, signature, data, executionTime, withDelegatecall) + ); + _queuedActions[actionHash] = false; + } + + function _validateDelay(uint256 delay) internal view { + if (delay < _minimumDelay) revert DelayShorterThanMin(); + if (delay > _maximumDelay) revert DelayLongerThanMax(); + } + + // harness: private to internal + function _verifyCallResult(bool success, bytes memory returnData) + internal + pure + returns (bytes memory) + { + if (success) { + return returnData; + } else { + // Look for revert reason and bubble it up if present + if (returnData.length > 0) { + // The easiest way to bubble the revert reason is using memory via assembly + + // solhint-disable-next-line no-inline-assembly + assembly { + let returndata_size := mload(returnData) + revert(add(32, returnData), returndata_size) + } + } else { + revert FailedActionExecution(); + } + } + } +} diff --git a/certora/munged/bridges/L2BridgeExecutor.sol b/certora/munged/bridges/L2BridgeExecutor.sol new file mode 100644 index 0000000..3dd816e --- /dev/null +++ b/certora/munged/bridges/L2BridgeExecutor.sol @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {IL2BridgeExecutor} from '../interfaces/IL2BridgeExecutor.sol'; +import {BridgeExecutorBase} from './BridgeExecutorBase.sol'; + +/** + * @title L2BridgeExecutor + * @author Aave + * @notice Abstract contract that implements bridge executor functionality for L2 + * @dev It does not implement the `onlyEthereumGovernanceExecutor` modifier. This should instead be done in the inheriting + * contract with proper configuration and adjustments depending on the L2 + */ +abstract contract L2BridgeExecutor is BridgeExecutorBase, IL2BridgeExecutor { + // Address of the Ethereum Governance Executor, which should be able to queue actions sets + address internal _ethereumGovernanceExecutor; + + /** + * @dev Only the Ethereum Governance Executor should be able to call functions marked by this modifier. + **/ + modifier onlyEthereumGovernanceExecutor() virtual; + + /** + * @dev Constructor + * + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) BridgeExecutorBase(delay, gracePeriod, minimumDelay, maximumDelay, guardian) { + _ethereumGovernanceExecutor = ethereumGovernanceExecutor; + } + + /// @inheritdoc IL2BridgeExecutor + // Certora harness : removed _queue() + function queue( + address[] memory targets, + uint256[] memory values, + string[] memory signatures, + bytes[] memory calldatas, + bool[] memory withDelegatecalls + ) external onlyEthereumGovernanceExecutor { + //_queue(targets, values, signatures, calldatas, withDelegatecalls); + } + + /// @inheritdoc IL2BridgeExecutor + function updateEthereumGovernanceExecutor(address ethereumGovernanceExecutor) external onlyThis { + emit EthereumGovernanceExecutorUpdate(_ethereumGovernanceExecutor, ethereumGovernanceExecutor); + _ethereumGovernanceExecutor = ethereumGovernanceExecutor; + } + + /// @inheritdoc IL2BridgeExecutor + function getEthereumGovernanceExecutor() external view returns (address) { + return _ethereumGovernanceExecutor; + } +} diff --git a/certora/munged/bridges/OptimismBridgeExecutor.sol b/certora/munged/bridges/OptimismBridgeExecutor.sol new file mode 100644 index 0000000..3f61173 --- /dev/null +++ b/certora/munged/bridges/OptimismBridgeExecutor.sol @@ -0,0 +1,59 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {ICrossDomainMessenger} from '../dependencies/optimism/interfaces/ICrossDomainMessenger.sol'; +import {L2BridgeExecutor} from './L2BridgeExecutor.sol'; + +/** + * @title OptimismBridgeExecutor + * @author Aave + * @notice Implementation of the Optimism Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the Optimism L2 Cross Domain Messenger and having + * the EthereumGovernanceExecutor as xDomainMessageSender + */ +contract OptimismBridgeExecutor is L2BridgeExecutor { + // Address of the Optimism L2 Cross Domain Messenger, in charge of redirecting cross-chain transactions in L2 + address public immutable OVM_L2_CROSS_DOMAIN_MESSENGER; + + /// @inheritdoc L2BridgeExecutor + modifier onlyEthereumGovernanceExecutor() override { + if ( + msg.sender != OVM_L2_CROSS_DOMAIN_MESSENGER || + ICrossDomainMessenger(OVM_L2_CROSS_DOMAIN_MESSENGER).xDomainMessageSender() != + _ethereumGovernanceExecutor + ) revert UnauthorizedEthereumExecutor(); + _; + } + + /** + * @dev Constructor + * + * @param ovmL2CrossDomainMessenger The address of the Optimism L2CrossDomainMessenger + * @param ethereumGovernanceExecutor The address of the EthereumGovernanceExecutor + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address ovmL2CrossDomainMessenger, + address ethereumGovernanceExecutor, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) + L2BridgeExecutor( + ethereumGovernanceExecutor, + delay, + gracePeriod, + minimumDelay, + maximumDelay, + guardian + ) + { + OVM_L2_CROSS_DOMAIN_MESSENGER = ovmL2CrossDomainMessenger; + } +} diff --git a/certora/munged/bridges/PolygonBridgeExecutor.sol b/certora/munged/bridges/PolygonBridgeExecutor.sol new file mode 100644 index 0000000..1646296 --- /dev/null +++ b/certora/munged/bridges/PolygonBridgeExecutor.sol @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +import {IFxMessageProcessor} from '../dependencies/polygon/fxportal/interfaces/IFxMessageProcessor.sol'; +import {BridgeExecutorBase} from './BridgeExecutorBase.sol'; + +/** + * @title PolygonBridgeExecutor + * @author Aave + * @notice Implementation of the Polygon Bridge Executor, able to receive cross-chain transactions from Ethereum + * @dev Queuing an ActionsSet into this Executor can only be done by the FxChild and after passing the EthereumGovernanceExecutor check + * as the FxRoot sender + */ +contract PolygonBridgeExecutor is BridgeExecutorBase, IFxMessageProcessor { + error UnauthorizedChildOrigin(); + error UnauthorizedRootOrigin(); + + /** + * @dev Emitted when the FxRoot Sender is updated + * @param oldFxRootSender The address of the old FxRootSender + * @param newFxRootSender The address of the new FxRootSender + **/ + event FxRootSenderUpdate(address oldFxRootSender, address newFxRootSender); + + /** + * @dev Emitted when the FxChild is updated + * @param oldFxChild The address of the old FxChild + * @param newFxChild The address of the new FxChild + **/ + event FxChildUpdate(address oldFxChild, address newFxChild); + + // Address of the FxRoot Sender, sending the cross-chain transaction from Ethereum + address internal _fxRootSender; // Certora harness: private -> internal + // Address of the FxChild, in charge of redirecting cross-chain transactions in Polygon + address internal _fxChild; // Certora harness: private -> internal + + /** + * @dev Only FxChild can call functions marked by this modifier. + **/ + modifier onlyFxChild() { + if (msg.sender != _fxChild) revert UnauthorizedChildOrigin(); + _; + } + + /** + * @dev Constructor + * + * @param fxRootSender The address of the transaction sender in FxRoot + * @param fxChild The address of the FxChild + * @param delay The delay before which an actions set can be executed + * @param gracePeriod The time period after a delay during which an actions set can be executed + * @param minimumDelay The minimum bound a delay can be set to + * @param maximumDelay The maximum bound a delay can be set to + * @param guardian The address of the guardian, which can cancel queued proposals (can be zero) + */ + constructor( + address fxRootSender, + address fxChild, + uint256 delay, + uint256 gracePeriod, + uint256 minimumDelay, + uint256 maximumDelay, + address guardian + ) BridgeExecutorBase(delay, gracePeriod, minimumDelay, maximumDelay, guardian) { + _fxRootSender = fxRootSender; + _fxChild = fxChild; + } + + /// @inheritdoc IFxMessageProcessor + // Certora harness: added virtual + function processMessageFromRoot( + uint256 stateId, + address rootMessageSender, + bytes calldata data + ) external override virtual onlyFxChild { + if (rootMessageSender != _fxRootSender) revert UnauthorizedRootOrigin(); + + address[] memory targets; + uint256[] memory values; + string[] memory signatures; + bytes[] memory calldatas; + bool[] memory withDelegatecalls; + + (targets, values, signatures, calldatas, withDelegatecalls) = abi.decode( + data, + (address[], uint256[], string[], bytes[], bool[]) + ); + + _queue(targets, values, signatures, calldatas, withDelegatecalls); + } + + /** + * @notice Update the address of the FxRoot Sender + * @param fxRootSender The address of the new FxRootSender + **/ + function updateFxRootSender(address fxRootSender) external onlyThis { + emit FxRootSenderUpdate(_fxRootSender, fxRootSender); + _fxRootSender = fxRootSender; + } + + /** + * @notice Update the address of the FxChild + * @param fxChild The address of the new FxChild + **/ + function updateFxChild(address fxChild) external onlyThis { + emit FxChildUpdate(_fxChild, fxChild); + _fxChild = fxChild; + } + + /** + * @notice Returns the address of the FxRoot Sender + * @return The address of the FxRootSender + **/ + function getFxRootSender() external view returns (address) { + return _fxRootSender; + } + + /** + * @notice Returns the address of the FxChild + * @return fxChild The address of FxChild + **/ + function getFxChild() external view returns (address) { + return _fxChild; + } +} diff --git a/certora/munged/dependencies/arbitrum/AddressAliasHelper.sol b/certora/munged/dependencies/arbitrum/AddressAliasHelper.sol new file mode 100644 index 0000000..beecdc2 --- /dev/null +++ b/certora/munged/dependencies/arbitrum/AddressAliasHelper.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: Apache-2.0 + +/* + * Copyright 2019-2021, Offchain Labs, Inc. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +pragma solidity >=0.7.5; + +library AddressAliasHelper { + uint160 constant offset = uint160(0x1111000000000000000000000000000000001111); + + /// @notice Utility function that converts the address in the L1 that submitted a tx to + /// the inbox to the msg.sender viewed in the L2 + /// @param l1Address the address in the L1 that triggered the tx to L2 + /// @return l2Address L2 address as viewed in msg.sender + function applyL1ToL2Alias(address l1Address) internal pure returns (address l2Address) { + l2Address = address(uint160(l1Address) + offset); + } + + /// @notice Utility function that converts the msg.sender viewed in the L2 to the + /// address in the L1 that submitted a tx to the inbox + /// @param l2Address L2 address as viewed in msg.sender + /// @return l1Address the address in the L1 that triggered the tx to L2 + function undoL1ToL2Alias(address l2Address) internal pure returns (address l1Address) { + l1Address = address(uint160(l2Address) - offset); + } +} diff --git a/certora/munged/dependencies/arbitrum/interfaces/ArbRetryableTx.sol b/certora/munged/dependencies/arbitrum/interfaces/ArbRetryableTx.sol new file mode 100644 index 0000000..4909b2d --- /dev/null +++ b/certora/munged/dependencies/arbitrum/interfaces/ArbRetryableTx.sol @@ -0,0 +1,72 @@ +pragma solidity >=0.4.21 <0.9.0; + +/** + * @title precompiled contract in every Arbitrum chain for retryable transaction related data retrieval and interactions. Exists at 0x000000000000000000000000000000000000006E + */ +interface ArbRetryableTx { + /** + * @notice Redeem a redeemable tx. + * Revert if called by an L2 contract, or if userTxHash does not exist, or if userTxHash reverts. + * If this returns, userTxHash has been completed and is no longer available for redemption. + * If this reverts, userTxHash is still available for redemption (until it times out or is canceled). + * @param userTxHash unique identifier of retryable message: keccak256(keccak256(ArbchainId, inbox-sequence-number), uint(0) ) + */ + function redeem(bytes32 userTxHash) external; + + /** + * @notice Return the minimum lifetime of redeemable txn. + * @return lifetime in seconds + */ + function getLifetime() external view returns (uint256); + + /** + * @notice Return the timestamp when userTxHash will age out, or zero if userTxHash does not exist. + * The timestamp could be in the past, because aged-out tickets might not be discarded immediately. + * @param userTxHash unique ticket identifier + * @return timestamp for ticket's deadline + */ + function getTimeout(bytes32 userTxHash) external view returns (uint256); + + /** + * @notice Return the price, in wei, of submitting a new retryable tx with a given calldata size. + * @param calldataSize call data size to get price of (in wei) + * @return (price, nextUpdateTimestamp). Price is guaranteed not to change until nextUpdateTimestamp. + */ + function getSubmissionPrice(uint256 calldataSize) external view returns (uint256, uint256); + + /** + * @notice Return the price, in wei, of extending the lifetime of userTxHash by an additional lifetime period. Revert if userTxHash doesn't exist. + * @param userTxHash unique ticket identifier + * @return (price, nextUpdateTimestamp). Price is guaranteed not to change until nextUpdateTimestamp. + */ + function getKeepalivePrice(bytes32 userTxHash) external view returns (uint256, uint256); + + /** + @notice Deposits callvalue into the sender's L2 account, then adds one lifetime period to the life of userTxHash. + * If successful, emits LifetimeExtended event. + * Revert if userTxHash does not exist, or if the timeout of userTxHash is already at least one lifetime period in the future, or if the sender has insufficient funds (after the deposit). + * @param userTxHash unique ticket identifier + * @return New timeout of userTxHash. + */ + function keepalive(bytes32 userTxHash) external payable returns (uint256); + + /** + * @notice Return the beneficiary of userTxHash. + * Revert if userTxHash doesn't exist. + * @param userTxHash unique ticket identifier + * @return address of beneficiary for ticket + */ + function getBeneficiary(bytes32 userTxHash) external view returns (address); + + /** + * @notice Cancel userTxHash and refund its callvalue to its beneficiary. + * Revert if userTxHash doesn't exist, or if called by anyone other than userTxHash's beneficiary. + * @param userTxHash unique ticket identifier + */ + function cancel(bytes32 userTxHash) external; + + event TicketCreated(bytes32 indexed userTxHash); + event LifetimeExtended(bytes32 indexed userTxHash, uint256 newTimeout); + event Redeemed(bytes32 indexed userTxHash); + event Canceled(bytes32 indexed userTxHash); +} diff --git a/certora/munged/dependencies/arbitrum/interfaces/IInbox.sol b/certora/munged/dependencies/arbitrum/interfaces/IInbox.sol new file mode 100644 index 0000000..a8e836b --- /dev/null +++ b/certora/munged/dependencies/arbitrum/interfaces/IInbox.sol @@ -0,0 +1,50 @@ +pragma solidity >=0.7.0; + +interface IInbox { + function sendL2Message(bytes calldata messageData) external returns (uint256); + + function sendUnsignedTransaction( + uint256 maxGas, + uint256 gasPriceBid, + uint256 nonce, + address destAddr, + uint256 amount, + bytes calldata data + ) external returns (uint256); + + function sendContractTransaction( + uint256 maxGas, + uint256 gasPriceBid, + address destAddr, + uint256 amount, + bytes calldata data + ) external returns (uint256); + + function sendL1FundedUnsignedTransaction( + uint256 maxGas, + uint256 gasPriceBid, + uint256 nonce, + address destAddr, + bytes calldata data + ) external payable returns (uint256); + + function sendL1FundedContractTransaction( + uint256 maxGas, + uint256 gasPriceBid, + address destAddr, + bytes calldata data + ) external payable returns (uint256); + + function createRetryableTicket( + address destAddr, + uint256 arbTxCallValue, + uint256 maxSubmissionCost, + address submissionRefundAddress, + address valueRefundAddress, + uint256 maxGas, + uint256 gasPriceBid, + bytes calldata data + ) external payable returns (uint256); + + function depositEth(uint256 maxSubmissionCost) external payable returns (uint256); +} diff --git a/certora/munged/dependencies/optimism/interfaces/ICrossDomainMessenger.sol b/certora/munged/dependencies/optimism/interfaces/ICrossDomainMessenger.sol new file mode 100644 index 0000000..c7e4362 --- /dev/null +++ b/certora/munged/dependencies/optimism/interfaces/ICrossDomainMessenger.sol @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MIT +pragma solidity >0.5.0 <0.9.0; + +/** + * @title ICrossDomainMessenger + */ +interface ICrossDomainMessenger { + /********** + * Events * + **********/ + + event SentMessage( + address indexed target, + address sender, + bytes message, + uint256 messageNonce, + uint256 gasLimit + ); + event RelayedMessage(bytes32 indexed msgHash); + event FailedRelayedMessage(bytes32 indexed msgHash); + + /************* + * Variables * + *************/ + + function xDomainMessageSender() external view returns (address); + + /******************** + * Public Functions * + ********************/ + + /** + * Sends a cross domain message to the target messenger. + * @param _target Target contract address. + * @param _message Message to send to the target. + * @param _gasLimit Gas limit for the provided message. + */ + function sendMessage( + address _target, + bytes calldata _message, + uint32 _gasLimit + ) external; +} diff --git a/certora/munged/dependencies/polygon/CustomPolygonMapping.sol b/certora/munged/dependencies/polygon/CustomPolygonMapping.sol new file mode 100644 index 0000000..7e7960a --- /dev/null +++ b/certora/munged/dependencies/polygon/CustomPolygonMapping.sol @@ -0,0 +1,179 @@ +/** + *Submitted for verification at Etherscan.io on 2020-05-30 + */ + +/** +Matic network contracts +*/ + +pragma solidity ^0.5.2; + +contract Ownable { + address private _owner; + + event OwnershipTransferred(address indexed previousOwner, address indexed newOwner); + + /** + * @dev The Ownable constructor sets the original `owner` of the contract to the sender + * account. + */ + constructor() internal { + _owner = msg.sender; + emit OwnershipTransferred(address(0), _owner); + } + + /** + * @return the address of the owner. + */ + function owner() public view returns (address) { + return _owner; + } + + /** + * @dev Throws if called by any account other than the owner. + */ + modifier onlyOwner() { + require(isOwner()); + _; + } + + /** + * @return true if `msg.sender` is the owner of the contract. + */ + function isOwner() public view returns (bool) { + return msg.sender == _owner; + } + + /** + * @dev Allows the current owner to relinquish control of the contract. + * It will not be possible to call the functions with the `onlyOwner` + * modifier anymore. + * @notice Renouncing ownership will leave the contract without an owner, + * thereby removing any functionality that is only available to the owner. + */ + function renounceOwnership() public onlyOwner { + emit OwnershipTransferred(_owner, address(0)); + _owner = address(0); + } + + /** + * @dev Allows the current owner to transfer control of the contract to a newOwner. + * @param newOwner The address to transfer ownership to. + */ + function transferOwnership(address newOwner) public onlyOwner { + _transferOwnership(newOwner); + } + + /** + * @dev Transfers control of the contract to a newOwner. + * @param newOwner The address to transfer ownership to. + */ + function _transferOwnership(address newOwner) internal { + require(newOwner != address(0)); + emit OwnershipTransferred(_owner, newOwner); + _owner = newOwner; + } +} + +library SafeMath { + /** + * @dev Multiplies two unsigned integers, reverts on overflow. + */ + function mul(uint256 a, uint256 b) internal pure returns (uint256) { + // Gas optimization: this is cheaper than requiring 'a' not being zero, but the + // benefit is lost if 'b' is also tested. + // See: https://github.com/OpenZeppelin/openzeppelin-solidity/pull/522 + if (a == 0) { + return 0; + } + + uint256 c = a * b; + require(c / a == b); + + return c; + } + + /** + * @dev Integer division of two unsigned integers truncating the quotient, reverts on division by zero. + */ + function div(uint256 a, uint256 b) internal pure returns (uint256) { + // Solidity only automatically asserts when dividing by 0 + require(b > 0); + uint256 c = a / b; + // assert(a == b * c + a % b); // There is no case in which this doesn't hold + + return c; + } + + /** + * @dev Subtracts two unsigned integers, reverts on overflow (i.e. if subtrahend is greater than minuend). + */ + function sub(uint256 a, uint256 b) internal pure returns (uint256) { + require(b <= a); + uint256 c = a - b; + + return c; + } + + /** + * @dev Adds two unsigned integers, reverts on overflow. + */ + function add(uint256 a, uint256 b) internal pure returns (uint256) { + uint256 c = a + b; + require(c >= a); + + return c; + } + + /** + * @dev Divides two unsigned integers and returns the remainder (unsigned integer modulo), + * reverts when dividing by zero. + */ + function mod(uint256 a, uint256 b) internal pure returns (uint256) { + require(b != 0); + return a % b; + } +} + +contract CustomPolygonMapping is Ownable { + using SafeMath for uint256; + + uint256 public counter; + mapping(address => address) public registrations; + + event NewRegistration(address indexed user, address indexed sender, address indexed receiver); + event RegistrationUpdated(address indexed user, address indexed sender, address indexed receiver); + event StateSynced(uint256 indexed id, address indexed contractAddress, bytes data); + + modifier onlyRegistered(address receiver) { + require(registrations[receiver] == msg.sender, 'Invalid sender'); + _; + } + + function syncState(address receiver, bytes calldata data) external onlyRegistered(receiver) { + counter = counter.add(1); + emit StateSynced(counter, receiver, data); + // THIS IS THE ONLY CUSTOM PART + bool success; + bytes memory resultData; + (success, resultData) = receiver.call( + abi.encodeWithSignature('onStateReceive(uint256,bytes)', counter, data) + ); + require(success, 'FAILED_ACTION_EXECUTION_CUSTOM_MAPPING'); + // END THE CUSTOM PART + } + + // register new contract for state sync + function register(address sender, address receiver) public { + require( + isOwner() || registrations[receiver] == msg.sender, + 'StateSender.register: Not authorized to register' + ); + registrations[receiver] = sender; + if (registrations[receiver] == address(0)) { + emit NewRegistration(msg.sender, sender, receiver); + } else { + emit RegistrationUpdated(msg.sender, sender, receiver); + } + } +} diff --git a/certora/munged/dependencies/polygon/fxportal/FxChild.sol b/certora/munged/dependencies/polygon/fxportal/FxChild.sol new file mode 100644 index 0000000..52ba147 --- /dev/null +++ b/certora/munged/dependencies/polygon/fxportal/FxChild.sol @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.7.3; + +// IStateReceiver represents interface to receive state +interface IStateReceiver { + function onStateReceive(uint256 stateId, bytes calldata data) external; +} + +// IFxMessageProcessor represents interface to process message +interface IFxMessageProcessor { + function processMessageFromRoot( + uint256 stateId, + address rootMessageSender, + bytes calldata data + ) external; +} + +/** + * @title FxChild child contract for state receiver + */ +contract FxChild is IStateReceiver { + address public fxRoot; + + event NewFxMessage(address rootMessageSender, address receiver, bytes data); + + function setFxRoot(address _fxRoot) public { + require(fxRoot == address(0x0)); + fxRoot = _fxRoot; + } + + function onStateReceive(uint256 stateId, bytes calldata _data) external override { + // require(msg.sender == address(0x0000000000000000000000000000000000001001), 'Invalid sender'); + (address rootMessageSender, address receiver, bytes memory data) = abi.decode( + _data, + (address, address, bytes) + ); + emit NewFxMessage(rootMessageSender, receiver, data); + IFxMessageProcessor(receiver).processMessageFromRoot(stateId, rootMessageSender, data); + } +} diff --git a/certora/munged/dependencies/polygon/fxportal/FxRoot.sol b/certora/munged/dependencies/polygon/fxportal/FxRoot.sol new file mode 100644 index 0000000..3c9749d --- /dev/null +++ b/certora/munged/dependencies/polygon/fxportal/FxRoot.sol @@ -0,0 +1,36 @@ +/** + *Submitted for verification at Etherscan.io on 2021-01-17 + */ + +// SPDX-License-Identifier: MIT +pragma solidity 0.7.3; + +interface IStateSender { + function syncState(address receiver, bytes calldata data) external; +} + +interface IFxStateSender { + function sendMessageToChild(address _receiver, bytes calldata _data) external; +} + +/** + * @title FxRoot root contract for fx-portal + */ +contract FxRoot is IFxStateSender { + IStateSender public stateSender; + address public fxChild; + + constructor(address _stateSender) { + stateSender = IStateSender(_stateSender); + } + + function setFxChild(address _fxChild) public { + require(fxChild == address(0x0)); + fxChild = _fxChild; + } + + function sendMessageToChild(address _receiver, bytes calldata _data) public override { + bytes memory data = abi.encode(msg.sender, _receiver, _data); + stateSender.syncState(fxChild, data); + } +} diff --git a/certora/munged/dependencies/polygon/fxportal/interfaces/IFxMessageProcessor.sol b/certora/munged/dependencies/polygon/fxportal/interfaces/IFxMessageProcessor.sol new file mode 100644 index 0000000..cf2556a --- /dev/null +++ b/certora/munged/dependencies/polygon/fxportal/interfaces/IFxMessageProcessor.sol @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.10; + +/** + * @title IFxMessageProcessor + * @notice Defines the interface to process message + */ +interface IFxMessageProcessor { + /** + * @notice Process the cross-chain message from a FxChild contract through the Ethereum/Polygon StateSender + * @param stateId The id of the cross-chain message created in the Ethereum/Polygon StateSender + * @param rootMessageSender The address that initially sent this message on Ethereum + * @param data The data from the abi-encoded cross-chain message + **/ + function processMessageFromRoot( + uint256 stateId, + address rootMessageSender, + bytes calldata data + ) external; +} diff --git a/certora/munged/interfaces/IExecutorBase.sol b/certora/munged/interfaces/IExecutorBase.sol new file mode 100644 index 0000000..33f6714 --- /dev/null +++ b/certora/munged/interfaces/IExecutorBase.sol @@ -0,0 +1,250 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +/** + * @title IExecutorBase + * @author Aave + * @notice Defines the basic interface for the ExecutorBase abstract contract + */ +interface IExecutorBase { + error InvalidInitParams(); + error NotGuardian(); + error OnlyCallableByThis(); + error MinimumDelayTooLong(); + error MaximumDelayTooShort(); + error GracePeriodTooShort(); + error DelayShorterThanMin(); + error DelayLongerThanMax(); + error OnlyQueuedActions(); + error TimelockNotFinished(); + error InvalidActionsSetId(); + error EmptyTargets(); + error InconsistentParamsLength(); + error DuplicateAction(); + error InsufficientBalance(); + error FailedActionExecution(); + + /** + * @notice This enum contains all possible actions set states + */ + enum ActionsSetState { + Queued, + Executed, + Canceled, + Expired + } + + /** + * @notice This struct contains the data needed to execute a specified set of actions + * @param targets Array of targets to call + * @param values Array of values to pass in each call + * @param signatures Array of function signatures to encode in each call (can be empty) + * @param calldatas Array of calldatas to pass in each call, appended to the signature at the same array index if not empty + * @param withDelegateCalls Array of whether to delegatecall for each call + * @param executionTime Timestamp starting from which the actions set can be executed + * @param executed True if the actions set has been executed, false otherwise + * @param canceled True if the actions set has been canceled, false otherwise + */ + struct ActionsSet { + address[] targets; + uint256[] values; + string[] signatures; + bytes[] calldatas; + bool[] withDelegatecalls; + uint256 executionTime; + bool executed; + bool canceled; + } + + /** + * @dev Emitted when an ActionsSet is queued + * @param id Id of the ActionsSet + * @param targets Array of targets to be called by the actions set + * @param values Array of values to pass in each call by the actions set + * @param signatures Array of function signatures to encode in each call by the actions set + * @param calldatas Array of calldata to pass in each call by the actions set + * @param withDelegatecalls Array of whether to delegatecall for each call of the actions set + * @param executionTime The timestamp at which this actions set can be executed + **/ + event ActionsSetQueued( + uint256 indexed id, + address[] targets, + uint256[] values, + string[] signatures, + bytes[] calldatas, + bool[] withDelegatecalls, + uint256 executionTime + ); + + /** + * @dev Emitted when an ActionsSet is successfully executed + * @param id Id of the ActionsSet + * @param initiatorExecution The address that triggered the ActionsSet execution + * @param returnedData The returned data from the ActionsSet execution + **/ + event ActionsSetExecuted( + uint256 indexed id, + address indexed initiatorExecution, + bytes[] returnedData + ); + + /** + * @dev Emitted when an ActionsSet is cancelled by the guardian + * @param id Id of the ActionsSet + **/ + event ActionsSetCanceled(uint256 indexed id); + + /** + * @dev Emitted when a new guardian is set + * @param oldGuardian The address of the old guardian + * @param newGuardian The address of the new guardian + **/ + event GuardianUpdate(address oldGuardian, address newGuardian); + + /** + * @dev Emitted when the delay (between queueing and execution) is updated + * @param oldDelay The value of the old delay + * @param newDelay The value of the new delay + **/ + event DelayUpdate(uint256 oldDelay, uint256 newDelay); + + /** + * @dev Emitted when the grace period (between executionTime and expiration) is updated + * @param oldGracePeriod The value of the old grace period + * @param newGracePeriod The value of the new grace period + **/ + event GracePeriodUpdate(uint256 oldGracePeriod, uint256 newGracePeriod); + + /** + * @dev Emitted when the minimum delay (lower bound of delay) is updated + * @param oldMinimumDelay The value of the old minimum delay + * @param newMinimumDelay The value of the new minimum delay + **/ + event MinimumDelayUpdate(uint256 oldMinimumDelay, uint256 newMinimumDelay); + + /** + * @dev Emitted when the maximum delay (upper bound of delay)is updated + * @param oldMaximumDelay The value of the old maximum delay + * @param newMaximumDelay The value of the new maximum delay + **/ + event MaximumDelayUpdate(uint256 oldMaximumDelay, uint256 newMaximumDelay); + + /** + * @notice Execute the ActionsSet + * @param actionsSetId The id of the ActionsSet to execute + **/ + function execute(uint256 actionsSetId) external payable; + + /** + * @notice Cancel the ActionsSet + * @param actionsSetId The id of the ActionsSet to cancel + **/ + function cancel(uint256 actionsSetId) external; + + /** + * @notice Update guardian + * @param guardian The address of the new guardian + **/ + function updateGuardian(address guardian) external; + + /** + * @notice Update the delay, time between queueing and execution of ActionsSet + * @dev It does not affect to actions set that are already queued + * @param delay The value of the delay (in seconds) + **/ + function updateDelay(uint256 delay) external; + + /** + * @notice Update the grace period, the period after the execution time during which an actions set can be executed + * @param gracePeriod The value of the grace period (in seconds) + **/ + function updateGracePeriod(uint256 gracePeriod) external; + + /** + * @notice Update the minimum allowed delay + * @param minimumDelay The value of the minimum delay (in seconds) + **/ + function updateMinimumDelay(uint256 minimumDelay) external; + + /** + * @notice Update the maximum allowed delay + * @param maximumDelay The maximum delay (in seconds) + **/ + function updateMaximumDelay(uint256 maximumDelay) external; + + /** + * @notice Allows to delegatecall a given target with an specific amount of value + * @dev This function is external so it allows to specify a defined msg.value for the delegate call, reducing + * the risk that a delegatecall gets executed with more value than intended + * @return True if the delegate call was successful, false otherwise + * @return The bytes returned by the delegate call + **/ + function executeDelegateCall(address target, bytes calldata data) + external + payable + returns (bool, bytes memory); + + /** + * @notice Allows to receive funds into the executor + * @dev Useful for actionsSet that needs funds to gets executed + */ + function receiveFunds() external payable; + + /** + * @notice Returns the delay (between queuing and execution) + * @return The value of the delay (in seconds) + **/ + function getDelay() external view returns (uint256); + + /** + * @notice Returns the grace period + * @return The value of the grace period (in seconds) + **/ + function getGracePeriod() external view returns (uint256); + + /** + * @notice Returns the minimum delay + * @return The value of the minimum delay (in seconds) + **/ + function getMinimumDelay() external view returns (uint256); + + /** + * @notice Returns the maximum delay + * @return The value of the maximum delay (in seconds) + **/ + function getMaximumDelay() external view returns (uint256); + + /** + * @notice Returns the address of the guardian + * @return The address of the guardian + **/ + function getGuardian() external view returns (address); + + /** + * @notice Returns the total number of actions sets of the executor + * @return The number of actions sets + **/ + function getActionsSetCount() external view returns (uint256); + + /** + * @notice Returns the data of an actions set + * @param actionsSetId The id of the ActionsSet + * @return The data of the ActionsSet + **/ + function getActionsSetById(uint256 actionsSetId) external view returns (ActionsSet memory); + + /** + * @notice Returns the current state of an actions set + * @param actionsSetId The id of the ActionsSet + * @return The current state of theI ActionsSet + **/ + function getCurrentState(uint256 actionsSetId) external view returns (ActionsSetState); + + /** + * @notice Returns whether an actions set (by actionHash) is queued + * @dev actionHash = keccak256(abi.encode(target, value, signature, data, executionTime, withDelegatecall)) + * @param actionHash hash of the action to be checked + * @return True if the underlying action of actionHash is queued, false otherwise + **/ + function isActionQueued(bytes32 actionHash) external view returns (bool); +} diff --git a/certora/munged/interfaces/IL2BridgeExecutor.sol b/certora/munged/interfaces/IL2BridgeExecutor.sol new file mode 100644 index 0000000..1fb0be6 --- /dev/null +++ b/certora/munged/interfaces/IL2BridgeExecutor.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity 0.8.10; + +/** + * @title IL2BridgeExecutorBase + * @author Aave + * @notice Defines the basic interface for the L2BridgeExecutor abstract contract + */ +interface IL2BridgeExecutor { + error UnauthorizedEthereumExecutor(); + + /** + * @dev Emitted when the Ethereum Governance Executor is updated + * @param oldEthereumGovernanceExecutor The address of the old EthereumGovernanceExecutor + * @param newEthereumGovernanceExecutor The address of the new EthereumGovernanceExecutor + **/ + event EthereumGovernanceExecutorUpdate( + address oldEthereumGovernanceExecutor, + address newEthereumGovernanceExecutor + ); + + /** + * @notice Queue an ActionsSet + * @dev If a signature is empty, calldata is used for the execution, calldata is appended to signature otherwise + * @param targets Array of targets to be called by the actions set + * @param values Array of values to pass in each call by the actions set + * @param signatures Array of function signatures to encode in each call by the actions (can be empty) + * @param calldatas Array of calldata to pass in each call by the actions set + * @param withDelegatecalls Array of whether to delegatecall for each call of the actions set + **/ + function queue( + address[] memory targets, + uint256[] memory values, + string[] memory signatures, + bytes[] memory calldatas, + bool[] memory withDelegatecalls + ) external; + + /** + * @notice Update the address of the Ethereum Governance Executor + * @param ethereumGovernanceExecutor The address of the new EthereumGovernanceExecutor + **/ + function updateEthereumGovernanceExecutor(address ethereumGovernanceExecutor) external; + + /** + * @notice Returns the address of the Ethereum Governance Executor + * @return The address of the EthereumGovernanceExecutor + **/ + function getEthereumGovernanceExecutor() external view returns (address); +} diff --git a/certora/report/Formal Verification Report of AAVE L2 Bridge.pdf b/certora/report/Formal Verification Report of AAVE L2 Bridge.pdf new file mode 100644 index 0000000..e95eda4 Binary files /dev/null and b/certora/report/Formal Verification Report of AAVE L2 Bridge.pdf differ diff --git a/certora/scripts/runComplexity.sh b/certora/scripts/runComplexity.sh new file mode 100755 index 0000000..7cec426 --- /dev/null +++ b/certora/scripts/runComplexity.sh @@ -0,0 +1,13 @@ +certoraRun contracts/bridges/OptimismBridgeExecutor.sol:OptimismBridgeExecutor \ + --verify OptimismBridgeExecutor:certora/specs/complexity.spec \ + --solc solc8.10 \ + --optimistic_loop \ + --staging \ + --msg "OptimismBridgeExecutor complexity check" + +certoraRun contracts/bridges/ArbitrumBridgeExecutor.sol:ArbitrumBridgeExecutor \ + --verify ArbitrumBridgeExecutor:certora/specs/complexity.spec \ + --solc solc8.10 \ + --optimistic_loop \ + --staging \ + --msg "ArbitrumBridgeExecutor complexity check" diff --git a/certora/scripts/verifyArbitrum.sh b/certora/scripts/verifyArbitrum.sh new file mode 100644 index 0000000..20a1f98 --- /dev/null +++ b/certora/scripts/verifyArbitrum.sh @@ -0,0 +1,20 @@ +certoraRun certora/harness/ArbitrumHarness.sol \ + certora/harness/DummyERC20A.sol \ + certora/harness/DummyERC20B.sol \ + certora/harness/mockTarget.sol \ + --verify ArbitrumHarness:certora/specs/Optimism_ArbitrumBridge.spec \ + --link mockTarget:_executor=ArbitrumHarness \ + mockTarget:_tokenA=DummyERC20A \ + mockTarget:_tokenB=DummyERC20B \ + ArbitrumHarness:_mock=mockTarget \ + --solc solc8.10 \ + --optimistic_loop \ + --loop_iter 2 \ + --cloud \ + --rules $1 $2 $3 $4 $5 $6 $7 $8 $9 ${10} ${11} ${12} ${13} ${14} ${15} ${16} \ + --settings -contractRecursionLimit=1 \ + --send_only \ + --msg "Arbitrum all" +# py ../EVMVerifier/scripts/certoraRun.py contracts/bridges/OptimismBridgeExecutor.sol \ +# + diff --git a/certora/scripts/verifyOptimism.sh b/certora/scripts/verifyOptimism.sh new file mode 100644 index 0000000..4327fba --- /dev/null +++ b/certora/scripts/verifyOptimism.sh @@ -0,0 +1,20 @@ +certoraRun certora/harness/OptimismHarness.sol \ + certora/harness/DummyERC20A.sol \ + certora/harness/DummyERC20B.sol \ + certora/harness/mockTarget.sol \ + --verify OptimismHarness:certora/specs/Optimism_ArbitrumBridge.spec \ + --link mockTarget:_executor=OptimismHarness \ + mockTarget:_tokenA=DummyERC20A \ + mockTarget:_tokenB=DummyERC20B \ + OptimismHarness:_mock=mockTarget \ + --solc solc8.10 \ + --optimistic_loop \ + --loop_iter 2 \ + --cloud \ + --rules $1 $2 $3 $4 $5 $6 $7 $8 $9 ${10} ${11} ${12} ${13} ${14} ${15} ${16} \ + --settings -contractRecursionLimit=1 \ + --send_only \ + --msg "Optimisim all" +# py ../EVMVerifier/scripts/certoraRun.py contracts/bridges/OptimismBridgeExecutor.sol \ +# + diff --git a/certora/scripts/verifyPolygon.sh b/certora/scripts/verifyPolygon.sh new file mode 100644 index 0000000..c2e3b4f --- /dev/null +++ b/certora/scripts/verifyPolygon.sh @@ -0,0 +1,18 @@ +certoraRun certora/harness/PolygonHarness.sol \ + certora/harness/DummyERC20A.sol \ + certora/harness/DummyERC20B.sol \ + certora/harness/mockTargetPoly.sol \ + --verify PolygonHarness:certora/specs/PolygonBridge.spec \ + --link mockTargetPoly:_executor=PolygonHarness \ + mockTargetPoly:_tokenA=DummyERC20A \ + mockTargetPoly:_tokenB=DummyERC20B \ + PolygonHarness:_mock=mockTargetPoly \ + --solc solc8.10 \ + --optimistic_loop \ + --loop_iter 2 \ + --cloud \ + --rules $1 $2 $3 $4 $5 $6 $7 $8 $9 ${10} ${11} ${12} ${13} ${14} ${15} ${16} \ + --settings -contractRecursionLimit=1 \ + --send_only \ + --msg "Polygon all" +# py ../EVMVerifier/scripts/certoraRun.py contracts/bridges/OptimismBridgeExecutor.sol \ diff --git a/certora/specs/Optimism_ArbitrumBridge.spec b/certora/specs/Optimism_ArbitrumBridge.spec new file mode 100644 index 0000000..41d29a2 --- /dev/null +++ b/certora/specs/Optimism_ArbitrumBridge.spec @@ -0,0 +1,550 @@ +import "erc20.spec" +using DummyERC20A as erc20_A +using DummyERC20B as erc20_B + +// Verification reports: +// Optimism: +// https://vaas-stg.certora.com/output/41958/aa361a2ea9e170a0f577/?anonymousKey=87cf9a705ef8f93f6d9403b56a447cf67404a2c1 +// Arbitrum: +// https://vaas-stg.certora.com/output/41958/9a0c4f34d04cb0432b39/?anonymousKey=b2e095528d7156b7351ff711e3a888f31c7b1c11 + +//////////////////////////////////////////////////////////////////////////// +// Methods // +//////////////////////////////////////////////////////////////////////////// + +methods { + getDelay() returns (uint256) envfree + getGracePeriod() returns (uint256) envfree + getMinimumDelay() returns (uint256) envfree + getMaximumDelay() returns (uint256) envfree + getGuardian() returns(address) envfree + getActionsSetCount() returns(uint256) envfree + getCurrentState(uint256) returns (uint8) + getEthereumGovernanceExecutor() returns (address) envfree + getActionsSetExecutionTime(uint256) returns (uint256) envfree + ID2actionHash(uint256, uint256) returns (bytes32) envfree + getActionsSetLength(uint256) returns (uint256) envfree + getActionSetWithDelegate(uint256, uint256) returns (bool) envfree + getActionsSetTarget(uint256, uint256) returns (address) envfree + getActionsSetCalldata(uint256, uint256) returns (bytes) envfree + queue(address[], uint256[], string[], bytes[], bool[]) + getActionsSetExecuted(uint256) returns (bool) envfree + getActionsSetCanceled(uint256) returns (bool) envfree + + delegatecall(bytes) => NONDET +} + + // enum ActionsSetState + // Queued, + // Executed, + // Canceled, + // Expired + +//////////////////////////////////////////////////////////////////////////// +// Ghosts and definitions // +//////////////////////////////////////////////////////////////////////////// + +definition stateVariableGetter(method f) + returns bool = ( + f.selector == getDelay().selector || + f.selector == getGracePeriod().selector || + f.selector == getMinimumDelay().selector || + f.selector == getMaximumDelay().selector || + f.selector == getGuardian().selector || + f.selector == getActionsSetCount().selector); + +definition stateVariableUpdate(method f) + returns bool = ( + f.selector == updateDelay(uint256).selector || + f.selector == updateGuardian(address).selector || + f.selector == updateGracePeriod(uint256).selector || + f.selector == updateMinimumDelay(uint256).selector || + f.selector == updateMaximumDelay(uint256).selector); + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// +invariant properDelay() + getMinimumDelay() <= getDelay() && getDelay() <= getMaximumDelay() + +invariant actionNotCanceledAndExecuted(uint256 setID) + ! (getActionsSetCanceled(setID) && getActionsSetExecuted(setID)) + +invariant notCanceledNotExecuted(uint256 id) + ( !getActionsSetCanceled(id) && !getActionsSetExecuted(id) ) + { + preserved{ + require id == getActionsSetCount(); + } + } + +invariant minDelayLtMaxDelay() + getMinimumDelay() <= getMaximumDelay() + +// Only the current contract (executor) can change its variables. +rule whoChangedStateVariables(method f) +{ + env e; + calldataarg args; + // State variables before + uint256 delay1 = getDelay(); + uint256 period1 = getGracePeriod(); + uint256 minDelay1 = getMinimumDelay(); + uint256 maxDelay1 = getMaximumDelay(); + address guardian1 = getGuardian(); + // Call function + f(e, args); + // State variables after + uint256 delay2 = getDelay(); + uint256 period2 = getGracePeriod(); + uint256 minDelay2 = getMinimumDelay(); + uint256 maxDelay2 = getMaximumDelay(); + address guardian2 = getGuardian(); + + bool stateChanged = !( delay1 == delay2 && + period1 == period2 && + minDelay1 == minDelay2 && + maxDelay1 == maxDelay2 && + guardian1 == guardian2); + + assert stateChanged => e.msg.sender == currentContract, + "Someone else changed state variables"; +} + +// Verified: +// https://prover.certora.com/output/41958/72618a1086584b9273ee/?anonymousKey=e8133886ff86eeb1f2d395b3f97460ff37dbc3cc +rule queueDoesntModifyStateVariables() +{ + env e; + calldataarg args; + // State variables before + uint256 delay1 = getDelay(); + uint256 period1 = getGracePeriod(); + uint256 minDelay1 = getMinimumDelay(); + uint256 maxDelay1 = getMaximumDelay(); + address guardian1 = getGuardian(); + + // Call queue with one action in the set. + queue2(e, args); + + // State variables after + uint256 delay2 = getDelay(); + uint256 period2 = getGracePeriod(); + uint256 minDelay2 = getMinimumDelay(); + uint256 maxDelay2 = getMaximumDelay(); + address guardian2 = getGuardian(); + + bool stateIntact = delay1 == delay2 && + period1 == period2 && + minDelay1 == minDelay2 && + maxDelay1 == maxDelay2 && + guardian1 == guardian2; + + assert stateIntact, + "_queue changed state variables unexpectedly"; +} + + +// Queue cannot cancel an action set. +// Verified +// https://prover.certora.com/output/41958/8123508132af65dab125/?anonymousKey=bffc0a16295e7bccdafb2b5eb9bba6a5f90c8968 +rule queueCannotCancel() +{ + env e; + calldataarg args; + uint256 actionsSetId; + + require getCurrentState(e, actionsSetId) != 2; + queue2(e, args); + assert getCurrentState(e, actionsSetId) != 2; +} + +// execute cannot cancel another set. +rule executeCannotCancel() +{ + env e; + calldataarg args; + uint256 calledSet; + uint256 canceledSet; + + require getCurrentState(e, canceledSet) != 2; + require getGuardian() != _mock(e); + + execute(e, calledSet); + + assert getCurrentState(e, canceledSet) != 2; +} + +// A three-part rule to prove that: +// An action set ID is never queued twice, after being executed once. + +// First part: +// Prove that an actions set is marked as 'queued' +// After invoking queue2. +rule noIncarnations1() +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + require actionsSetId < max_uint; + requireInvariant notCanceledNotExecuted(actionsSetId); + queue2(e, args); + assert getCurrentState(e, actionsSetId) == 0 + && actionsSetId < getActionsSetCount(); +} + +// Second part: +// Given the first part, after execute of that set, +// the same set cannot be marked as 'queued'. +rule noIncarnations2(uint256 actionsSetId) +{ + env e; + execute(e, actionsSetId); + assert getCurrentState(e, actionsSetId) != 0; +} + +// Third part: +// Given the second part, while an action set is not marked +// as 'queued', calling queue2 with any arguments +// cannot set the same set to 'queued' again. +rule noIncarnations3(uint256 actionsSetId) +{ + env e; + calldataarg args; + require actionsSetId <= getActionsSetCount(); + require getCurrentState(e, actionsSetId) != 0; + queue2(e, args); + assert getCurrentState(e, actionsSetId) != 0; +} + +// Once executed, an actions set ID remains executed forever. +rule executedForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 1; + f(e, args); + assert getCurrentState(e2, actionsSetId) == 1; +} + +rule canceledForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 2; + f(e, args); + assert getCurrentState(e2, actionsSetId) == 2; +} + +rule expiredForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 3; + require e.block.timestamp <= e2.block.timestamp; + + if (f.selector == updateGracePeriod(uint256).selector) { + uint256 oldPeriod = getGracePeriod(); + updateGracePeriod(e, args); + uint256 newPeriod = getGracePeriod(); + assert newPeriod <= oldPeriod => + getCurrentState(e2, actionsSetId) == 3; + } + else { + f(e, args); + assert getCurrentState(e2, actionsSetId) == 3; + } +} + +// After calling to queue, the new action set +// must be set as 'queued'. +rule queuedStateConsistency() +{ + env e; + calldataarg args; + uint256 id = getActionsSetCount(); + requireInvariant notCanceledNotExecuted(id); + queue2(e, args); + assert getCurrentState(e, id) == 0; +} + +// Queue must increase action set by 1. +rule queuedChangedCounter() +{ + env e; + calldataarg args; + uint256 count1 = getActionsSetCount(); + queue2(e, args); + uint256 count2 = getActionsSetCount(); + + assert count1 < max_uint => count2 == count1+1; +} + +// A set status can be changed from 'queued' to 'canceled' +// via the "cancel" function only. +rule onlyCancelCanCancel(method f, uint actionsSetId) +{ + env e; + calldataarg args; + require getGuardian() != _mock(e); + // Replace by !=2 + require getCurrentState(e, actionsSetId) != 2; + + f(e, args); + + assert getCurrentState(e, actionsSetId) == 2 + => f.selector == cancel(uint256).selector; +} + +// Cancel only cancels one actions set. +rule cancelExclusive(uint actionsSetId1, uint actionsSetId2) +{ + env e; + uint8 stateBefore = getCurrentState(e, actionsSetId2); + cancel(e, actionsSetId1); + uint8 stateAfter = getCurrentState(e, actionsSetId2); + + assert actionsSetId1 != actionsSetId2 => stateBefore == stateAfter; +} + +// Checks which functions change the state of a set. +rule whoChangesActionsSetState(method f, uint actionsSetId) +filtered {f -> !f.isView} +{ + env e; + calldataarg args; + + uint8 state1 = getCurrentState(e, actionsSetId); + f(e, args); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert state1 == state2, "${f} changed the state of an actions set."; +} + +// When delay is defined, No immediate execution after queue. +rule holdYourHorses() +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + + uint256 delay = getDelay(); + queue2(e, args); + execute@withrevert(e, actionsSetId); + assert delay > 0 => lastReverted; +} + +// An action set cannot transform from 'queued' to 'executed' +// by a function different than "execute(uint256)". +rule executedValidTransition1(method f, uint256 actionsSetId) +filtered{f -> !f.isView} +{ + env e; + calldataarg args; + uint8 state1 = getCurrentState(e, actionsSetId); + f(e, args); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert f.selector != execute(uint256).selector => + ! (state1 == 0 && state2 == 1); +} + +// If any action set was executed, then this set (and only it) must change +// from 'queued' to 'executed'. +rule executedValidTransition2(uint256 actionsSetId) +{ + env e; + uint actionsSetId2; + uint8 state1 = getCurrentState(e, actionsSetId); + execute(e, actionsSetId2); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert actionsSetId2 == actionsSetId <=> state1 == 0 && state2 == 1; +} + +// Execute must fail if actions set state is expired. +rule executeFailsIfExpired(uint256 actionsSetId) +{ + env e; + uint8 stateBefore = getCurrentState(e, actionsSetId); + execute@withrevert(e, actionsSetId); + bool executeReverted = lastReverted; + assert stateBefore == 3 => executeReverted; +} + +// Cannot execute before delay passed. +// Execution time must not change in this case. +rule executeRevertsBeforeDelay(method f) +filtered{f -> stateVariableUpdate(f)} +{ + env e; + env e2; + calldataarg args; + calldataarg args2; + uint256 actionsSetId = getActionsSetCount(); + uint256 delay = getDelay(); + queue2(e, args); + + uint256 execTime1 = getActionsSetExecutionTime(actionsSetId); + f(e2, args2); + uint256 execTime2 = getActionsSetExecutionTime(actionsSetId); + + execute@withrevert(e2, actionsSetId); + + assert + (e2.block.timestamp < e.block.timestamp + delay => lastReverted) + && (execTime2 == execTime1); +} + +// Two equal transaction sets in different blocks +// can have the same execution time and therefore same hash. +// This leads to revert. +rule sameExecutionTimesReverts() +{ + env e1; env e2; + calldataarg args; + uint256 delay; + uint256 t1 = e1.block.timestamp; + uint256 t2 = e2.block.timestamp; + + // Assume different blocks (block2 later than block1) + require t1 < t2; + + // queue first set. + queue2(e1, args); + // Change the delay period. + uint256 delay1 = getDelay(); + updateDelay(e1, delay); + uint256 delay2 = getDelay(); + // Try to queue second set, with same arguments. + queue2@withrevert(e2, args); + + assert t1 + delay1 == t2 + delay2 => lastReverted; +} + +// Can two batches with same arguments be queued twice? No: +rule independentQueuedActions(method f) +filtered{f -> stateVariableUpdate(f)} +{ + env e1; env e2; env e3; + calldataarg args; + calldataarg argsUpdate; + + // Assume different blocks (block3 later than block1) + require e1.block.timestamp < e3.block.timestamp; + require e1.msg.sender == e3.msg.sender; + require e3.msg.value == 0; + require e3.block.timestamp + getDelay() < max_uint; + + storage initState = lastStorage; + queue2(e3, args); + + // queue first set. + queue2(e1, args) at initState; + // Update some state variable changing method. + f(e2, argsUpdate); + // Try to queue second set, with same arguments. + queue2@withrevert(e3, args); + + assert !lastReverted; +} + +// After a call to queue, the action hash should +// be marked as 'queued'. +rule afterQueueHashQueued(bytes32 actionHash) +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + + bool queueBefore = isActionQueued(e, actionHash); + queue2(e, args); + bool queuedAfter = isActionQueued(e, actionHash); + + assert (actionHash == ID2actionHash(actionsSetId, 0) || + actionHash == ID2actionHash(actionsSetId, 1)) + <=> !queueBefore && queuedAfter; +} + +// Only queued actions can be executed. +// Assuming it was originally queued by 'queue' +// See rule 'afterQueueHashQueued'. +// Assuming only two actions per set. +rule onlyQueuedAreExecuted(bytes32 actionHash, uint256 actionsSetId) +{ + env e2; env e; + calldataarg args; + + require isActionQueued(e, actionHash); + // This is true in general, guardian is not a contract (is EOA). + require getGuardian() != _mock(e); + execute(e2, actionsSetId); + bool queuedAfter = isActionQueued(e2, actionHash); + + assert (actionHash == ID2actionHash(actionsSetId, 0) || + actionHash == ID2actionHash(actionsSetId, 1)) + <=> !queuedAfter; +} + +// Check if queue cannot be called twice with same arguments. +rule actionDuplicate() +{ + env e; + calldataarg args; + + queue2(e, args); + queue2@withrevert(e, args); + assert lastReverted; +} + +// Reachable. +rule queue2Reachability() +{ + env e; calldataarg args; + + queue2(e, args); + assert false; +} + +rule queuePriviliged() +{ + env e1; + env e2; + calldataarg args1; + calldataarg args2; + queue2(e1, args1); + queue2@withrevert(e2, args2); + assert e1.msg.sender != e2.msg.sender => lastReverted; +} + +rule cancelPriviliged() +{ + env e1; + env e2; + calldataarg args1; + calldataarg args2; + cancel(e1, args1); + cancel@withrevert(e2, args2); + assert e1.msg.sender != e2.msg.sender => lastReverted; +} + +// After updating a grace period, an action set execution reverts +// if and only if it's state is 'expired'. +/* +rule gracePeriodChangedAffectsExecution(uint256 actionsSetId) +{ + env e; env e2; + uint period; + // Assume queued action set. + require getCurrentState(e, actionsSetId) == 0; + + storage initialStorage = lastStorage; + // Allow execution (assume does not revert) + execute(e, actionsSetId); + // Now check whether changing the grace period could lead to revert. + updateGracePeriod(e, period) at initialStorage; + uint8 stateAfterUpdate = getCurrentState(e, actionsSetId); + + execute@withrevert(e, actionsSetId); + assert lastReverted <=> stateAfterUpdate == 3; +}*/ \ No newline at end of file diff --git a/certora/specs/PolygonBridge.spec b/certora/specs/PolygonBridge.spec new file mode 100644 index 0000000..b0e9048 --- /dev/null +++ b/certora/specs/PolygonBridge.spec @@ -0,0 +1,532 @@ +import "erc20.spec" +using DummyERC20A as erc20_A +using DummyERC20B as erc20_B + +//Verification reports: +// https://vaas-stg.certora.com/output/41958/07a16231de45f5a25396/?anonymousKey=d9f85af7ef7c4ebf7cd2de9bfcc31b24f7d1d6d0 + +//////////////////////////////////////////////////////////////////////////// +// Methods // +//////////////////////////////////////////////////////////////////////////// + +methods { + getDelay() returns (uint256) envfree + getGracePeriod() returns (uint256) envfree + getMinimumDelay() returns (uint256) envfree + getMaximumDelay() returns (uint256) envfree + getGuardian() returns(address) envfree + updateFxChild(address) + updateFxRootSender(address) + getFxRootSender() returns(address) + getFxChild() returns(address) + getActionsSetCount() returns(uint256) envfree + getCurrentState(uint256) returns (uint8) + getActionsSetExecutionTime(uint256) returns (uint256) envfree + ID2actionHash(uint256, uint256) returns (bytes32) envfree + getActionsSetLength(uint256) returns (uint256) envfree + getActionSetWithDelegate(uint256, uint256) returns (bool) envfree + getActionsSetTarget(uint256, uint256) returns (address) envfree + getActionsSetCalldata(uint256, uint256) returns (bytes) envfree + getActionsSetExecuted(uint256) returns (bool) envfree + getActionsSetCanceled(uint256) returns (bool) envfree + processMessageFromRoot(uint256, address, bytes) + + delegatecall(bytes) => NONDET +} + + // enum ActionsSetState + // Queued, + // Executed, + // Canceled, + // Expired + +//////////////////////////////////////////////////////////////////////////// +// Ghosts and definitions // +//////////////////////////////////////////////////////////////////////////// + +definition stateVariableGetter(method f) + returns bool = ( + f.selector == getDelay().selector || + f.selector == getGracePeriod().selector || + f.selector == getMinimumDelay().selector || + f.selector == getMaximumDelay().selector || + f.selector == getGuardian().selector || + f.selector == getActionsSetCount().selector); + +definition stateVariableUpdate(method f) + returns bool = ( + f.selector == updateDelay(uint256).selector || + f.selector == updateGuardian(address).selector || + f.selector == updateGracePeriod(uint256).selector || + f.selector == updateMinimumDelay(uint256).selector || + f.selector == updateMaximumDelay(uint256).selector); + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// +invariant properDelay() + getMinimumDelay() <= getDelay() && getDelay() <= getMaximumDelay() + +invariant actionNotCanceledAndExecuted(uint256 setID) + ! (getActionsSetCanceled(setID) && getActionsSetExecuted(setID)) + +invariant notCanceledNotExecuted(uint256 id) + ( !getActionsSetCanceled(id) && !getActionsSetExecuted(id) ) + { + preserved{ + require id == getActionsSetCount(); + } + } + +invariant minDelayLtMaxDelay() + getMinimumDelay() <= getMaximumDelay() + +// Only the current contract (executor) can change its variables. +rule whoChangedStateVariables(method f) +{ + env e; + calldataarg args; + // State variables before + uint256 delay1 = getDelay(); + uint256 period1 = getGracePeriod(); + uint256 minDelay1 = getMinimumDelay(); + uint256 maxDelay1 = getMaximumDelay(); + address guardian1 = getGuardian(); + // Call function + f(e, args); + // State variables after + uint256 delay2 = getDelay(); + uint256 period2 = getGracePeriod(); + uint256 minDelay2 = getMinimumDelay(); + uint256 maxDelay2 = getMaximumDelay(); + address guardian2 = getGuardian(); + + bool stateChanged = !( delay1 == delay2 && + period1 == period2 && + minDelay1 == minDelay2 && + maxDelay1 == maxDelay2 && + guardian1 == guardian2); + + assert stateChanged => e.msg.sender == currentContract, + "Someone else changed state variables"; +} + +// Verified: +// https://prover.certora.com/output/41958/72618a1086584b9273ee/?anonymousKey=e8133886ff86eeb1f2d395b3f97460ff37dbc3cc +rule queueDoesntModifyStateVariables() +{ + env e; + calldataarg args; + // State variables before + uint256 delay1 = getDelay(); + uint256 period1 = getGracePeriod(); + uint256 minDelay1 = getMinimumDelay(); + uint256 maxDelay1 = getMaximumDelay(); + address guardian1 = getGuardian(); + + // Call queue with one action in the set. + processMessageFromRoot(e, args); + + // State variables after + uint256 delay2 = getDelay(); + uint256 period2 = getGracePeriod(); + uint256 minDelay2 = getMinimumDelay(); + uint256 maxDelay2 = getMaximumDelay(); + address guardian2 = getGuardian(); + + bool stateIntact = delay1 == delay2 && + period1 == period2 && + minDelay1 == minDelay2 && + maxDelay1 == maxDelay2 && + guardian1 == guardian2; + + assert stateIntact, + "_queue changed state variables unexpectedly"; +} + +// Queue cannot cancel an action set. +// Verified +// https://prover.certora.com/output/41958/8123508132af65dab125/?anonymousKey=bffc0a16295e7bccdafb2b5eb9bba6a5f90c8968 +rule queueCannotCancel() +{ + env e; + calldataarg args; + uint256 actionsSetId; + + require getCurrentState(e, actionsSetId) != 2; + processMessageFromRoot(e, args); + assert getCurrentState(e, actionsSetId) != 2; +} + +// execute cannot cancel another set. +rule executeCannotCancel() +{ + env e; + calldataarg args; + uint256 calledSet; + uint256 canceledSet; + + require getCurrentState(e, canceledSet) != 2; + require getGuardian() != _mock(e); + + execute(e, calledSet); + + assert getCurrentState(e, canceledSet) != 2; +} + +// A three-part rule to prove that: +// An action set ID is never queued twice, after being executed once. + +// First part: +// Prove that an actions set is marked as 'queued' +// After invoking processMessageFromRoot. +rule noIncarnations1() +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + require actionsSetId < max_uint; + requireInvariant notCanceledNotExecuted(actionsSetId); + processMessageFromRoot(e, args); + assert getCurrentState(e, actionsSetId) == 0 + && actionsSetId < getActionsSetCount(); +} + +// Second part: +// Given the first part, after execute of that set, +// the same set cannot be marked as 'queued'. +rule noIncarnations2(uint256 actionsSetId) +{ + env e; + execute(e, actionsSetId); + assert getCurrentState(e, actionsSetId) != 0; +} + +// Third part: +// Given the second part, while an action set is not marked +// as 'queued', calling processMessageFromRoot with any arguments +// cannot set the same set to 'queued' again. +rule noIncarnations3(uint256 actionsSetId) +{ + env e; + calldataarg args; + require actionsSetId <= getActionsSetCount(); + require getCurrentState(e, actionsSetId) != 0; + processMessageFromRoot(e, args); + assert getCurrentState(e, actionsSetId) != 0; +} + +// Once executed, an actions set ID remains executed forever. +// Verified (execpt delegate): +// https://prover.certora.com/output/41958/82a7a598594f67804b91/?anonymousKey=ebc5b375934595f5c8315460be4fe66db7877d79 +// Verified (for execute): +// https://prover.certora.com/output/41958/8292edd79fdfe44fa0e9/?anonymousKey=fbd57f179fa107431847150f148bd5e0a9911841 +rule executedForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 1; + f(e, args); + assert getCurrentState(e2, actionsSetId) == 1; +} + +rule canceledForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 2; + f(e, args); + assert getCurrentState(e2, actionsSetId) == 2; +} + +rule expiredForever(method f, uint256 actionsSetId) +{ + env e; env e2; + calldataarg args; + require getCurrentState(e, actionsSetId) == 3; + require e.block.timestamp <= e2.block.timestamp; + + if (f.selector == updateGracePeriod(uint256).selector) { + uint256 oldPeriod = getGracePeriod(); + updateGracePeriod(e, args); + uint256 newPeriod = getGracePeriod(); + assert newPeriod <= oldPeriod => + getCurrentState(e2, actionsSetId) == 3; + } + else { + f(e, args); + assert getCurrentState(e2, actionsSetId) == 3; + } +} + +// After calling to queue, the new action set +// must be set as 'queued'. +rule queuedStateConsistency() +{ + env e; + calldataarg args; + uint256 id = getActionsSetCount(); + requireInvariant notCanceledNotExecuted(id); + processMessageFromRoot(e, args); + assert getCurrentState(e, id) == 0; +} + +// Queue must increase action set by 1. +rule queuedChangedCounter() +{ + env e; + calldataarg args; + uint256 count1 = getActionsSetCount(); + processMessageFromRoot(e, args); + uint256 count2 = getActionsSetCount(); + + assert count1 < max_uint => count2 == count1+1; +} + +// A set status can be changed from 'queued' to 'canceled' +// via the "cancel" function only. +rule onlyCancelCanCancel(method f, uint actionsSetId) +{ + env e; + calldataarg args; + require getGuardian() != _mock(e); + // Replace by !=2 + require getCurrentState(e, actionsSetId) != 2; + + f(e, args); + + assert getCurrentState(e, actionsSetId) == 2 + => f.selector == cancel(uint256).selector; +} + +// Cancel only cancels one actions set. +rule cancelExclusive(uint actionsSetId1, uint actionsSetId2) +{ + env e; + uint8 stateBefore = getCurrentState(e, actionsSetId2); + cancel(e, actionsSetId1); + uint8 stateAfter = getCurrentState(e, actionsSetId2); + + assert actionsSetId1 != actionsSetId2 => stateBefore == stateAfter; +} + +// Checks which functions change the state of a set. +rule whoChangesActionsSetState(method f, uint actionsSetId) +filtered {f -> !f.isView} +{ + env e; + calldataarg args; + + uint8 state1 = getCurrentState(e, actionsSetId); + f(e, args); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert state1 == state2, "${f} changed the state of an actions set."; +} + +// When delay is defined, No immediate execution after queue. +rule holdYourHorses() +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + + uint256 delay = getDelay(); + processMessageFromRoot(e, args); + execute@withrevert(e, actionsSetId); + assert delay > 0 => lastReverted; +} + +// An action set cannot transform from 'queued' to 'executed' +// by a function different than "execute(uint256)". +rule executedValidTransition1(method f, uint256 actionsSetId) +filtered{f -> !f.isView} +{ + env e; + calldataarg args; + uint8 state1 = getCurrentState(e, actionsSetId); + f(e, args); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert f.selector != execute(uint256).selector => + ! (state1 == 0 && state2 == 1); +} + +// If any action set was executed, then this set (and only it) must change +// from 'queued' to 'executed'. +rule executedValidTransition2(uint256 actionsSetId) +{ + env e; + uint actionsSetId2; + uint8 state1 = getCurrentState(e, actionsSetId); + execute(e, actionsSetId2); + uint8 state2 = getCurrentState(e, actionsSetId); + + assert actionsSetId2 == actionsSetId <=> state1 == 0 && state2 == 1; +} + +// Execute must fail if actions set state is expired. +rule executeFailsIfExpired(uint256 actionsSetId) +{ + env e; + uint8 stateBefore = getCurrentState(e, actionsSetId); + execute@withrevert(e, actionsSetId); + bool executeReverted = lastReverted; + assert stateBefore == 3 => executeReverted; +} + +// Cannot execute before delay passed. +// Execution time must not change in this case. +rule executeRevertsBeforeDelay(method f) +filtered{f -> stateVariableUpdate(f)} +{ + env e; + env e2; + calldataarg args; + calldataarg args2; + uint256 actionsSetId = getActionsSetCount(); + uint256 delay = getDelay(); + processMessageFromRoot(e, args); + + uint256 execTime1 = getActionsSetExecutionTime(actionsSetId); + f(e2, args2); + uint256 execTime2 = getActionsSetExecutionTime(actionsSetId); + + execute@withrevert(e2, actionsSetId); + + assert + (e2.block.timestamp < e.block.timestamp + delay => lastReverted) + && (execTime2 == execTime1); +} + +// Two equal transaction sets in different blocks +// can have the same execution time and therefore same hash. +// This leads to revert. +rule sameExecutionTimesReverts() +{ + env e1; env e2; + calldataarg args; + uint256 delay; + uint256 t1 = e1.block.timestamp; + uint256 t2 = e2.block.timestamp; + + // Assume different blocks (block2 later than block1) + require t1 < t2; + + // queue first set. + processMessageFromRoot(e1, args); + // Change the delay period. + uint256 delay1 = getDelay(); + updateDelay(e1, delay); + uint256 delay2 = getDelay(); + // Try to queue second set, with same arguments. + processMessageFromRoot@withrevert(e2, args); + + assert t1 + delay1 == t2 + delay2 => lastReverted; +} + +// Can two batches with same arguments be queued twice? No: +rule independentQueuedActions(method f) +filtered{f -> stateVariableUpdate(f)} +{ + env e1; env e2; env e3; + calldataarg args; + calldataarg argsUpdate; + + // Assume different blocks (block3 later than block1) + require e1.block.timestamp < e3.block.timestamp; + require e1.msg.sender == e3.msg.sender; + require e3.msg.value == 0; + require e3.block.timestamp + getDelay() < max_uint; + + storage initState = lastStorage; + processMessageFromRoot(e3, args); + + // queue first set. + processMessageFromRoot(e1, args) at initState; + // Update some state variable changing method. + f(e2, argsUpdate); + // Try to queue second set, with same arguments. + processMessageFromRoot@withrevert(e3, args); + + assert !lastReverted; +} + +// After a call to queue, the action hash should +// be marked as 'queued'. +rule afterQueueHashQueued(bytes32 actionHash) +{ + env e; + calldataarg args; + uint256 actionsSetId = getActionsSetCount(); + + bool queueBefore = isActionQueued(e, actionHash); + processMessageFromRoot(e, args); + bool queuedAfter = isActionQueued(e, actionHash); + + assert (actionHash == ID2actionHash(actionsSetId, 0) || + actionHash == ID2actionHash(actionsSetId, 1)) + <=> !queueBefore && queuedAfter; +} + +// Only queued actions can be executed. +// Assuming it was originally queued by 'queue' +// See rule 'afterQueueHashQueued'. +// Assuming only two actions per set. +rule onlyQueuedAreExecuted(bytes32 actionHash, uint256 actionsSetId) +{ + env e2; env e; + calldataarg args; + + require isActionQueued(e, actionHash); + // This is true in general, guardian is not a contract (is EOA). + require getGuardian() != _mock(e); + execute(e2, actionsSetId); + bool queuedAfter = isActionQueued(e2, actionHash); + + assert (actionHash == ID2actionHash(actionsSetId, 0) || + actionHash == ID2actionHash(actionsSetId, 1)) + <=> !queuedAfter; +} + +// Check if queue cannot be called twice with same arguments. +rule actionDuplicate() +{ + env e; + calldataarg args; + + processMessageFromRoot(e, args); + processMessageFromRoot@withrevert(e, args); + assert lastReverted; +} + +// Reachable. +rule processMessageFromRootReachability() +{ + env e; calldataarg args; + + processMessageFromRoot(e, args); + assert false; +} + +rule queuePriviliged() +{ + env e1; + env e2; + calldataarg args1; + calldataarg args2; + processMessageFromRoot(e1, args1); + processMessageFromRoot@withrevert(e2, args2); + assert e1.msg.sender != e2.msg.sender => lastReverted; +} + +rule cancelPriviliged() +{ + env e1; + env e2; + calldataarg args1; + calldataarg args2; + cancel(e1, args1); + cancel@withrevert(e2, args2); + assert e1.msg.sender != e2.msg.sender => lastReverted; +} diff --git a/certora/specs/complexity.spec b/certora/specs/complexity.spec new file mode 100644 index 0000000..0645e07 --- /dev/null +++ b/certora/specs/complexity.spec @@ -0,0 +1,103 @@ +import "erc20.spec" + +rule sanity(method f) +{ + env e; + calldataarg args; + f(e,args); + assert false; +} + + +/* +This rule find which functions never reverts. + +*/ + + +rule noRevert(method f) +description "$f has reverting paths" +{ + env e; + calldataarg arg; + require e.msg.value == 0; + f@withrevert(e, arg); + assert !lastReverted, "${f.selector} can revert"; +} + + +rule alwaysRevert(method f) +description "$f has reverting paths" +{ + env e; + calldataarg arg; + f@withrevert(e, arg); + assert lastReverted, "${f.selector} succeeds"; +} + + +/* +This rule find which functions that can be called, may fail due to someone else calling a function right before. + +This is n expensive rule - might fail on the demo site on big contracts +*/ + +rule simpleFrontRunning(method f, address privileged) filtered { f-> !f.isView } +description "$f can no longer be called after it had been called by someone else" +{ + env e1; + calldataarg arg; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f(e1, arg); + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != e1.msg.sender; + f(e2, arg2) at initialStorage; + f@withrevert(e1, arg); + bool succeeded = !lastReverted; + + assert succeeded, "${f.selector} can be not be called if was called by someone else"; +} + + +/* +This rule find which functions are privileged. +A function is privileged if there is only one address that can call it. + +The rules finds this by finding which functions can be called by two different users. + +*/ + + +rule privilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + f@withrevert(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} + +rule whoChangedBalanceOf(method f, address u) { + env eB; + env eF; + calldataarg args; + uint256 before = balanceOf(eB, u); + f(eF,args); + assert balanceOf(eB, u) == before, "balanceOf changed"; +} \ No newline at end of file diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec new file mode 100644 index 0000000..9b261b9 --- /dev/null +++ b/certora/specs/erc20.spec @@ -0,0 +1,12 @@ +// erc20 methods +methods { + name() returns (string) => DISPATCHER(true) + symbol() returns (string) => DISPATCHER(true) + decimals() returns (string) => DISPATCHER(true) + totalSupply() returns (uint256) => DISPATCHER(true) + balanceOf(address) returns (uint256) => DISPATCHER(true) + allowance(address,address) returns (uint) => DISPATCHER(true) + approve(address,uint256) returns (bool) => DISPATCHER(true) + transfer(address,uint256) returns (bool) => DISPATCHER(true) + transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) +}