From cbb5efe6a6a6a8f15e004ac2e9762829640d4836 Mon Sep 17 00:00:00 2001 From: DhairyaSethi <55102840+DhairyaSethi@users.noreply.github.com> Date: Sat, 2 Nov 2024 12:23:43 +0530 Subject: [PATCH] feat: migrate certora formal verification conf --- certora/Makefile | 24 +++++++ certora/confs/ccip.conf | 21 ++++++ certora/harness/SimpleERC20.sol | 58 ++++++++++++++++ certora/munged/.gitignore | 2 + certora/specs/ccip.spec | 119 ++++++++++++++++++++++++++++++++ 5 files changed, 224 insertions(+) create mode 100644 certora/Makefile create mode 100644 certora/confs/ccip.conf create mode 100644 certora/harness/SimpleERC20.sol create mode 100644 certora/munged/.gitignore create mode 100644 certora/specs/ccip.spec diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 0000000000..0e33459cab --- /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/confs/ccip.conf b/certora/confs/ccip.conf new file mode 100644 index 0000000000..6df7e32e37 --- /dev/null +++ b/certora/confs/ccip.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "contracts/src/v0.8/ccip/pools/GHO/UpgradeableLockReleaseTokenPool.sol", + "certora/harness/SimpleERC20.sol" + ], + "packages": [ + "solidity-utils/=contracts/foundry-lib/solidity-utils/src/" + ], + "link": [ + "UpgradeableLockReleaseTokenPool:i_token=SimpleERC20" + ], + "optimistic_loop": true, + "process": "emv", + "prover_args": ["-depth 10","-mediumTimeout 700"], + "smt_timeout": "600", + "solc": "solc8.19", + "verify": "UpgradeableLockReleaseTokenPool:certora/specs/ccip.spec", + "rule_sanity": "basic", + "msg": "CCIP" +} + diff --git a/certora/harness/SimpleERC20.sol b/certora/harness/SimpleERC20.sol new file mode 100644 index 0000000000..f9d14a7ff6 --- /dev/null +++ b/certora/harness/SimpleERC20.sol @@ -0,0 +1,58 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +import {IERC20} from "../../contracts/src/v0.8/vendor/openzeppelin-solidity/v4.8.3/contracts/token/ERC20/IERC20.sol"; + +/** +A simple ERC implementation used as the underlying_asset for the verification process. + */ +contract SimpleERC20 is IERC20 { + uint256 t; + mapping(address => uint256) b; + mapping(address => mapping(address => uint256)) a; + + 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 override returns (uint256) { + return t; + } + + function balanceOf(address account) external view override returns (uint256) { + return b[account]; + } + + function transfer(address recipient, uint256 amount) external override 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 override returns (uint256) { + return a[owner][spender]; + } + + function approve(address spender, uint256 amount) external override returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external override 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; + } +} diff --git a/certora/munged/.gitignore b/certora/munged/.gitignore new file mode 100644 index 0000000000..d6b7ef32c8 --- /dev/null +++ b/certora/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore diff --git a/certora/specs/ccip.spec b/certora/specs/ccip.spec new file mode 100644 index 0000000000..e88cb8dab6 --- /dev/null +++ b/certora/specs/ccip.spec @@ -0,0 +1,119 @@ +/* + This is a Specification File for Smart Contract Verification with the Certora Prover. + Contract name: UpgradeableLockReleaseTokenPool +*/ + +using SimpleERC20 as erc20; + +methods { + function getCurrentBridgedAmount() external returns (uint256) envfree; + function getBridgeLimit() external returns (uint256) envfree; + function owner() external returns (address) envfree; +} + + +rule sanity { + env e; + calldataarg arg; + method f; + f(e, arg); + satisfy true; +} + + + +/* ============================================================================== + invariant: currentBridge_LEQ_bridgeLimit. + Description: The value of s_currentBridged is LEQ than the value of s_bridgeLimit. + Note: this may be violated if one calls to setBridgeLimit(newBridgeLimit) with + newBridgeLimit < s_currentBridged. + ============================================================================*/ +invariant currentBridge_LEQ_bridgeLimit() + getCurrentBridgedAmount() <= getBridgeLimit() + filtered { f -> + !f.isView && + f.selector != sig:setBridgeLimit(uint256).selector} + { + preserved initialize(address owner, address[] allowlist, address router, uint256 bridgeLimit) with (env e2) { + require getCurrentBridgedAmount()==0; + } + } + + +/* ============================================================================== + rule: withdrawLiquidity_correctness + description: The rule checks that the balance of the contract is as expected. + ============================================================================*/ +rule withdrawLiquidity_correctness(env e) { + uint256 amount; + + require e.msg.sender != currentContract; + uint256 bal_before = erc20.balanceOf(e, currentContract); + withdrawLiquidity(e, amount); + uint256 bal_after = erc20.balanceOf(e, currentContract); + + assert (to_mathint(bal_after) == bal_before - amount); +} + + +/* ============================================================================== + rule: provideLiquidity_correctness + description: The rule checks that the balance of the contract is as expected. + ============================================================================*/ +rule provideLiquidity_correctness(env e) { + uint256 amount; + + require e.msg.sender != currentContract; + uint256 bal_before = erc20.balanceOf(e, currentContract); + provideLiquidity(e, amount); + uint256 bal_after = erc20.balanceOf(e, currentContract); + + assert (to_mathint(bal_after) == bal_before + amount); +} + + +/* ============================================================================== + rule: only_lockOrBurn_can_increase_currentBridged + ============================================================================*/ +rule only_lockOrBurn_can_increase_currentBridged(env e) { + method f; + calldataarg args; + + uint256 curr_bridge_before = getCurrentBridgedAmount(); + f (e,args); + uint256 curr_bridge_after = getCurrentBridgedAmount(); + + assert + curr_bridge_after > curr_bridge_before => + f.selector==sig:lockOrBurn(address,bytes calldata,uint256,uint64,bytes calldata).selector; +} + + +/* ============================================================================== + rule: only_releaseOrMint_can_deccrease_currentBridged + ============================================================================*/ +rule only_releaseOrMint_can_decrease_currentBridged(env e) { + method f; + calldataarg args; + + uint256 curr_bridge_before = getCurrentBridgedAmount(); + f (e,args); + uint256 curr_bridge_after = getCurrentBridgedAmount(); + + assert + curr_bridge_after < curr_bridge_before => + f.selector==sig:releaseOrMint(bytes memory,address,uint256,uint64,bytes memory).selector; +} + + +/* ============================================================================== + rule: only_bridgeLimitAdmin_or_owner_can_call_setBridgeLimit + ============================================================================*/ +rule only_bridgeLimitAdmin_or_owner_can_call_setBridgeLimit(env e) { + uint256 newBridgeLimit; + + setBridgeLimit(e, newBridgeLimit); + + assert e.msg.sender==getBridgeLimitAdmin(e) || e.msg.sender==owner(); +} +