From 80458ea2382aadea4bdffe1954f6e53394612106 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 16 Aug 2023 15:15:51 +0200 Subject: [PATCH 1/9] feat: add dispatch for tokens --- certora/dispatch/ERC20Bad.sol | 12 ++++++++ certora/dispatch/ERC20Good.sol | 8 +++++ certora/dispatch/ERC20USDT.sol | 54 ++++++++++++++++++++++++++++++++++ 3 files changed, 74 insertions(+) create mode 100644 certora/dispatch/ERC20Bad.sol create mode 100644 certora/dispatch/ERC20Good.sol create mode 100644 certora/dispatch/ERC20USDT.sol diff --git a/certora/dispatch/ERC20Bad.sol b/certora/dispatch/ERC20Bad.sol new file mode 100644 index 000000000..96c8e5a48 --- /dev/null +++ b/certora/dispatch/ERC20Bad.sol @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.0; + +import {ERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol"; + +contract ERC20Bad is ERC20 { + constructor(string memory name, string memory symbol) ERC20(name, symbol) {} + + function _beforeTokenTransfer(address from, address to, uint256 amount) internal override { + _mint(to, amount); + } +} diff --git a/certora/dispatch/ERC20Good.sol b/certora/dispatch/ERC20Good.sol new file mode 100644 index 000000000..38fcc8e6c --- /dev/null +++ b/certora/dispatch/ERC20Good.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.0; + +import {ERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol"; + +contract ERC20Good is ERC20 { + constructor(string memory name, string memory symbol) ERC20(name, symbol) {} +} diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol new file mode 100644 index 000000000..f81240124 --- /dev/null +++ b/certora/dispatch/ERC20USDT.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.0; + +contract ERC20USDT { + uint256 public constant MAX_UINT = 2 ** 256 - 1; + + string public name; + string public symbol; + uint256 public decimals; + address owner; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowed; + + constructor(string _name, string _symbol, uint256 _decimals) { + name = _name; + symbol = _symbol; + decimals = _decimals; + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function transfer(address _to, uint256 _value) public { + balanceOf[msg.sender] -= _value; + balanceOf[_to] += _value; + Transfer(msg.sender, _to, _value); + } + + function transferFrom(address _from, address _to, uint256 _value) public { + if (allowed[_from][msg.sender] < MAX_UINT) { + allowed[_from][msg.sender] -= value; + } + balanceOf[_from] -= _value; + balanceOf[_to] -= _value; + } + + function approve(address _spender, uint256 _value) public { + require(!((_value != 0) && (allowed[msg.sender][_spender] != 0))); + + allowed[msg.sender][_spender] = _value; + } + + function allowance(address _owner, address _spender) public view returns (uint256 remaining) { + return allowed[_owner][_spender]; + } + + function mint(address _receiver, uint256 amount) public onlyOwner { + balanceOf[owner] += amount; + _totalSupply += amount; + } +} From e5021098012b91402a04f48ea6948fc1973dc8e9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 16 Aug 2023 22:34:14 +0200 Subject: [PATCH 2/9] feat: add verification of summary for transfers --- certora/dispatch/ERC20USDT.sol | 8 ++-- certora/harness/TransferHarness.sol | 24 ++++++++++++ certora/scripts/verifyBlueTransferSummary.sh | 14 +++++++ certora/specs/BlueTransferSummary.spec | 39 ++++++++++++++++++++ 4 files changed, 80 insertions(+), 5 deletions(-) create mode 100644 certora/harness/TransferHarness.sol create mode 100755 certora/scripts/verifyBlueTransferSummary.sh create mode 100644 certora/specs/BlueTransferSummary.spec diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol index f81240124..9df9378ff 100644 --- a/certora/dispatch/ERC20USDT.sol +++ b/certora/dispatch/ERC20USDT.sol @@ -11,7 +11,7 @@ contract ERC20USDT { mapping(address => uint256) public balanceOf; mapping(address => mapping(address => uint256)) public allowed; - constructor(string _name, string _symbol, uint256 _decimals) { + constructor(string memory _name, string memory _symbol, uint256 _decimals) { name = _name; symbol = _symbol; decimals = _decimals; @@ -26,15 +26,14 @@ contract ERC20USDT { function transfer(address _to, uint256 _value) public { balanceOf[msg.sender] -= _value; balanceOf[_to] += _value; - Transfer(msg.sender, _to, _value); } function transferFrom(address _from, address _to, uint256 _value) public { if (allowed[_from][msg.sender] < MAX_UINT) { - allowed[_from][msg.sender] -= value; + allowed[_from][msg.sender] -= _value; } balanceOf[_from] -= _value; - balanceOf[_to] -= _value; + balanceOf[_to] += _value; } function approve(address _spender, uint256 _value) public { @@ -49,6 +48,5 @@ contract ERC20USDT { function mint(address _receiver, uint256 amount) public onlyOwner { balanceOf[owner] += amount; - _totalSupply += amount; } } diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol new file mode 100644 index 000000000..fc435c919 --- /dev/null +++ b/certora/harness/TransferHarness.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.0; + +import "../../src/libraries/SafeTransferLib.sol"; +import "../../src/interfaces/IERC20.sol"; + +interface IERC20Extended is IERC20 { + function balanceOf(address) external returns (uint256); + function totalSupply() external returns (uint256); +} + +contract Transferer { + function doTransfer(address token, address from, address to, uint256 value) public { + IERC20Extended(token).transferFrom(from, to, value); + } + + function getBalance(address token, address user) public returns (uint256) { + return IERC20Extended(token).balanceOf(user); + } + + function getTotalSupply(address token) public returns (uint256) { + return IERC20Extended(token).totalSupply(); + } +} diff --git a/certora/scripts/verifyBlueTransferSummary.sh b/certora/scripts/verifyBlueTransferSummary.sh new file mode 100755 index 000000000..80a3be8da --- /dev/null +++ b/certora/scripts/verifyBlueTransferSummary.sh @@ -0,0 +1,14 @@ +#!/bin/bash + +set -euxo pipefail + +certoraRun \ + certora/harness/TransferHarness.sol \ + certora/dispatch/ERC20Good.sol \ + certora/dispatch/ERC20USDT.sol \ + --verify Transferer:certora/specs/BlueTransferSummary.spec \ + --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \ + --loop_iter 3 \ + --optimistic_loop \ + --msg "Morpho Transfer Summary" \ + "$@" diff --git a/certora/specs/BlueTransferSummary.spec b/certora/specs/BlueTransferSummary.spec new file mode 100644 index 000000000..acbcac4af --- /dev/null +++ b/certora/specs/BlueTransferSummary.spec @@ -0,0 +1,39 @@ +methods { + function doTransfer(address, address, address, uint256) external envfree; + function getBalance(address, address) external returns (uint256) envfree; + function getTotalSupply(address) external returns (uint256) envfree; + + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); +} + +ghost mapping(address => mathint) myBalances +{ + init_state axiom (forall address token. myBalances[token] == 0); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + myBalances[token] = require_uint256(myBalances[token] - amount); + } + if (to == currentContract) { + myBalances[token] = require_uint256(myBalances[token] + amount); + } +} + +rule checkTransferSummary(address token, address from, address to, uint256 amount) { + require from == currentContract || to == currentContract; + + require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token)); + + uint256 initialBalance = getBalance(token, currentContract); + doTransfer(token, from, to, amount); + uint256 finalBalance = getBalance(token, currentContract); + + mathint initialGhostBalance = myBalances[token]; + summarySafeTransferFrom(token, from, to, amount); + mathint finalGhostBalance = myBalances[token]; + + assert finalGhostBalance - initialGhostBalance == finalBalance - initialBalance; +} From 41aca5296f672210d45b71df083f60470a8d4559 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 16 Aug 2023 22:36:44 +0200 Subject: [PATCH 3/9] feat: add transfer summary to the CI --- .github/workflows/certora.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index a7c2cbebd..c3c7b0807 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -44,3 +44,4 @@ jobs: - verifyBlue.sh - verifyBlueRatioMathSummary.sh - verifyBlueExitLiquidity.sh + - verifyBlueTransferSummary.sh From 9229f3c048b48946e763a7523260f78a61592ec8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 16 Aug 2023 22:41:00 +0200 Subject: [PATCH 4/9] fix: install dependencies in CI --- .github/workflows/certora.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index c001e6e25..87c24b282 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -14,6 +14,9 @@ jobs: steps: - uses: actions/checkout@v3 + - name: Install submodules + run: git submodule update --init --recursive + - name: Install python uses: actions/setup-python@v4 with: From ffc7844cd2091b106b25056b974b6bb4b69f94d4 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 16 Aug 2023 22:43:43 +0200 Subject: [PATCH 5/9] fix: change name to TransferHarness --- certora/harness/TransferHarness.sol | 2 +- certora/scripts/verifyBlueTransferSummary.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol index fc435c919..b8382c921 100644 --- a/certora/harness/TransferHarness.sol +++ b/certora/harness/TransferHarness.sol @@ -9,7 +9,7 @@ interface IERC20Extended is IERC20 { function totalSupply() external returns (uint256); } -contract Transferer { +contract TransferHarness { function doTransfer(address token, address from, address to, uint256 value) public { IERC20Extended(token).transferFrom(from, to, value); } diff --git a/certora/scripts/verifyBlueTransferSummary.sh b/certora/scripts/verifyBlueTransferSummary.sh index 80a3be8da..1883d62fc 100755 --- a/certora/scripts/verifyBlueTransferSummary.sh +++ b/certora/scripts/verifyBlueTransferSummary.sh @@ -6,7 +6,7 @@ certoraRun \ certora/harness/TransferHarness.sol \ certora/dispatch/ERC20Good.sol \ certora/dispatch/ERC20USDT.sol \ - --verify Transferer:certora/specs/BlueTransferSummary.spec \ + --verify TransferHarness:certora/specs/BlueTransferSummary.spec \ --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \ --loop_iter 3 \ --optimistic_loop \ From 7125c7d3a85ae413abf846ae533daf4692df05ea Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 17 Aug 2023 09:58:28 +0200 Subject: [PATCH 6/9] refactor: simplify transfer summary check Co-authored-by: Jochen Hoenicke Signed-off-by: Quentin Garchery --- certora/specs/BlueTransferSummary.spec | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/certora/specs/BlueTransferSummary.spec b/certora/specs/BlueTransferSummary.spec index acbcac4af..76a1fe70c 100644 --- a/certora/specs/BlueTransferSummary.spec +++ b/certora/specs/BlueTransferSummary.spec @@ -31,9 +31,7 @@ rule checkTransferSummary(address token, address from, address to, uint256 amoun doTransfer(token, from, to, amount); uint256 finalBalance = getBalance(token, currentContract); - mathint initialGhostBalance = myBalances[token]; + require myBalances[token] == initialBalance; summarySafeTransferFrom(token, from, to, amount); - mathint finalGhostBalance = myBalances[token]; - - assert finalGhostBalance - initialGhostBalance == finalBalance - initialBalance; + assert myBalances[token] == finalBalance; } From 9739986152f578e760771d63a0e3409e429db486 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 17 Aug 2023 10:18:02 +0200 Subject: [PATCH 7/9] fix: cast balance to mathint --- certora/specs/BlueTransferSummary.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/BlueTransferSummary.spec b/certora/specs/BlueTransferSummary.spec index 76a1fe70c..3dc75591b 100644 --- a/certora/specs/BlueTransferSummary.spec +++ b/certora/specs/BlueTransferSummary.spec @@ -27,9 +27,9 @@ rule checkTransferSummary(address token, address from, address to, uint256 amoun require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token)); - uint256 initialBalance = getBalance(token, currentContract); + mathint initialBalance = getBalance(token, currentContract); doTransfer(token, from, to, amount); - uint256 finalBalance = getBalance(token, currentContract); + mathint finalBalance = getBalance(token, currentContract); require myBalances[token] == initialBalance; summarySafeTransferFrom(token, from, to, amount); From 5b9dc6379d1cd8819bf04663fc7ca716eed6e0bb Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 17 Aug 2023 10:19:23 +0200 Subject: [PATCH 8/9] feat: add dispatch token not reverting and returning a boolean --- certora/dispatch/ERC20NoRevert.sol | 55 ++++++++++++++++++++ certora/dispatch/ERC20USDT.sol | 27 +++++----- certora/scripts/verifyBlueTransferSummary.sh | 1 + 3 files changed, 71 insertions(+), 12 deletions(-) create mode 100644 certora/dispatch/ERC20NoRevert.sol diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol new file mode 100644 index 000000000..ff93b0862 --- /dev/null +++ b/certora/dispatch/ERC20NoRevert.sol @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.0; + +contract ERC20NoRevert { + string public name; + string public symbol; + uint256 public decimals; + address owner; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowed; + + constructor(string memory _name, string memory _symbol, uint256 _decimals) { + name = _name; + symbol = _symbol; + decimals = _decimals; + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) { + if (balanceOf[_from] < _amount) { + return false; + } + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + return true; + } + + function transfer(address _to, uint256 _amount) public returns (bool) { + return _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + allowed[_from][msg.sender] -= _amount; + return _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + require(!((_amount != 0) && (allowed[msg.sender][_spender] != 0))); + + allowed[msg.sender][_spender] = _amount; + } + + function allowance(address _owner, address _spender) public view returns (uint256 remaining) { + return allowed[_owner][_spender]; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + } +} diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol index 9df9378ff..a0400794d 100644 --- a/certora/dispatch/ERC20USDT.sol +++ b/certora/dispatch/ERC20USDT.sol @@ -23,30 +23,33 @@ contract ERC20USDT { _; } - function transfer(address _to, uint256 _value) public { - balanceOf[msg.sender] -= _value; - balanceOf[_to] += _value; + function _transfer(address _from, address _to, uint256 _amount) public { + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; } - function transferFrom(address _from, address _to, uint256 _value) public { + function transfer(address _to, uint256 _amount) public { + _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public { if (allowed[_from][msg.sender] < MAX_UINT) { - allowed[_from][msg.sender] -= _value; + allowed[_from][msg.sender] -= _amount; } - balanceOf[_from] -= _value; - balanceOf[_to] += _value; + _transfer(_from, _to, _amount); } - function approve(address _spender, uint256 _value) public { - require(!((_value != 0) && (allowed[msg.sender][_spender] != 0))); + function approve(address _spender, uint256 _amount) public { + require(!((_amount != 0) && (allowed[msg.sender][_spender] != 0))); - allowed[msg.sender][_spender] = _value; + allowed[msg.sender][_spender] = _amount; } function allowance(address _owner, address _spender) public view returns (uint256 remaining) { return allowed[_owner][_spender]; } - function mint(address _receiver, uint256 amount) public onlyOwner { - balanceOf[owner] += amount; + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; } } diff --git a/certora/scripts/verifyBlueTransferSummary.sh b/certora/scripts/verifyBlueTransferSummary.sh index 1883d62fc..e9ae59ddb 100755 --- a/certora/scripts/verifyBlueTransferSummary.sh +++ b/certora/scripts/verifyBlueTransferSummary.sh @@ -6,6 +6,7 @@ certoraRun \ certora/harness/TransferHarness.sol \ certora/dispatch/ERC20Good.sol \ certora/dispatch/ERC20USDT.sol \ + certora/dispatch/ERC20NoRevert.sol \ --verify TransferHarness:certora/specs/BlueTransferSummary.spec \ --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \ --loop_iter 3 \ From e0a9b50a5fe5526a1a4a0f609261b12d764e1038 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 17 Aug 2023 10:33:04 +0200 Subject: [PATCH 9/9] refactor: rename transfer to not only verify summary --- .github/workflows/certora.yml | 2 +- certora/harness/TransferHarness.sol | 12 +++++++----- ...yBlueTransferSummary.sh => verifyBlueTransfer.sh} | 2 +- .../{BlueTransferSummary.spec => BlueTransfer.spec} | 2 +- 4 files changed, 10 insertions(+), 8 deletions(-) rename certora/scripts/{verifyBlueTransferSummary.sh => verifyBlueTransfer.sh} (84%) rename certora/specs/{BlueTransferSummary.spec => BlueTransfer.spec} (94%) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 87c24b282..c1c5523cd 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -47,5 +47,5 @@ jobs: - verifyBlue.sh - verifyBlueRatioMathSummary.sh - verifyBlueExitLiquidity.sh - - verifyBlueTransferSummary.sh + - verifyBlueTransfer.sh - verifyReentrancy.sh diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol index b8382c921..e4f0d4f3c 100644 --- a/certora/harness/TransferHarness.sol +++ b/certora/harness/TransferHarness.sol @@ -5,20 +5,22 @@ import "../../src/libraries/SafeTransferLib.sol"; import "../../src/interfaces/IERC20.sol"; interface IERC20Extended is IERC20 { - function balanceOf(address) external returns (uint256); - function totalSupply() external returns (uint256); + function balanceOf(address) external view returns (uint256); + function totalSupply() external view returns (uint256); } contract TransferHarness { + using SafeTransferLib for IERC20; + function doTransfer(address token, address from, address to, uint256 value) public { - IERC20Extended(token).transferFrom(from, to, value); + IERC20(token).safeTransferFrom(from, to, value); } - function getBalance(address token, address user) public returns (uint256) { + function getBalance(address token, address user) public view returns (uint256) { return IERC20Extended(token).balanceOf(user); } - function getTotalSupply(address token) public returns (uint256) { + function getTotalSupply(address token) public view returns (uint256) { return IERC20Extended(token).totalSupply(); } } diff --git a/certora/scripts/verifyBlueTransferSummary.sh b/certora/scripts/verifyBlueTransfer.sh similarity index 84% rename from certora/scripts/verifyBlueTransferSummary.sh rename to certora/scripts/verifyBlueTransfer.sh index e9ae59ddb..7cddf3f51 100755 --- a/certora/scripts/verifyBlueTransferSummary.sh +++ b/certora/scripts/verifyBlueTransfer.sh @@ -7,7 +7,7 @@ certoraRun \ certora/dispatch/ERC20Good.sol \ certora/dispatch/ERC20USDT.sol \ certora/dispatch/ERC20NoRevert.sol \ - --verify TransferHarness:certora/specs/BlueTransferSummary.spec \ + --verify TransferHarness:certora/specs/BlueTransfer.spec \ --packages openzeppelin-contracts=lib/openzeppelin-contracts/contracts \ --loop_iter 3 \ --optimistic_loop \ diff --git a/certora/specs/BlueTransferSummary.spec b/certora/specs/BlueTransfer.spec similarity index 94% rename from certora/specs/BlueTransferSummary.spec rename to certora/specs/BlueTransfer.spec index 3dc75591b..8c435e88d 100644 --- a/certora/specs/BlueTransferSummary.spec +++ b/certora/specs/BlueTransfer.spec @@ -22,7 +22,7 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 } } -rule checkTransferSummary(address token, address from, address to, uint256 amount) { +rule checkTransfer(address token, address from, address to, uint256 amount) { require from == currentContract || to == currentContract; require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token));