From 43b0df35fa7fffd20a9a35b93cd624c47145b508 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 17 Aug 2023 15:29:30 +0200 Subject: [PATCH 1/3] feat: more thorough verification of the transfer lib --- certora/harness/TransferHarness.sol | 11 ++++++- certora/specs/BlueTransfer.spec | 49 +++++++++++++++++++++++++---- 2 files changed, 53 insertions(+), 7 deletions(-) diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol index e4f0d4f3c..1129191ef 100644 --- a/certora/harness/TransferHarness.sol +++ b/certora/harness/TransferHarness.sol @@ -6,20 +6,29 @@ import "../../src/interfaces/IERC20.sol"; interface IERC20Extended is IERC20 { function balanceOf(address) external view returns (uint256); + function allowance(address, 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 { + function doTransferFrom(address token, address from, address to, uint256 value) public { IERC20(token).safeTransferFrom(from, to, value); } + function doTransfer(address token, address to, uint256 value) public { + IERC20(token).safeTransfer(to, value); + } + function getBalance(address token, address user) public view returns (uint256) { return IERC20Extended(token).balanceOf(user); } + function getAllowance(address token, address owner, address spender) public view returns (uint256) { + return IERC20Extended(token).allowance(owner, spender); + } + function getTotalSupply(address token) public view returns (uint256) { return IERC20Extended(token).totalSupply(); } diff --git a/certora/specs/BlueTransfer.spec b/certora/specs/BlueTransfer.spec index 8c435e88d..79babb208 100644 --- a/certora/specs/BlueTransfer.spec +++ b/certora/specs/BlueTransfer.spec @@ -1,10 +1,14 @@ methods { - function doTransfer(address, address, address, uint256) external envfree; + function doTransfer(address, address, uint256) external envfree; + function doTransferFrom(address, address, address, uint256) external envfree; function getBalance(address, address) external returns (uint256) envfree; + function getAllowance(address, address, address) external returns (uint256) envfree; function getTotalSupply(address) external returns (uint256) envfree; + function _.transfer(address, uint256) external => DISPATCHER(true); function _.transferFrom(address, address, uint256) external => DISPATCHER(true); function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address, address) external => DISPATCHER(true); function _.totalSupply() external => DISPATCHER(true); } @@ -22,16 +26,49 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 } } -rule checkTransfer(address token, address from, address to, uint256 amount) { - require from == currentContract || to == currentContract; +rule checkTransferFromSummary(address token, address from, uint256 amount) { + mathint initialBalance = getBalance(token, currentContract); + require from != currentContract => initialBalance + getBalance(token, from) <= to_mathint(getTotalSupply(token)); + + doTransferFrom(token, from, currentContract, amount); + mathint finalBalance = getBalance(token, currentContract); - require from != to => getBalance(token, from) + getBalance(token, to) <= to_mathint(getTotalSupply(token)); + require myBalances[token] == initialBalance; + summarySafeTransferFrom(token, from, currentContract, amount); + assert myBalances[token] == finalBalance; +} +rule checkTransferSummary(address token, address to, uint256 amount) { mathint initialBalance = getBalance(token, currentContract); - doTransfer(token, from, to, amount); + require to != currentContract => initialBalance + getBalance(token, to) <= to_mathint(getTotalSupply(token)); + + doTransfer(token, to, amount); mathint finalBalance = getBalance(token, currentContract); require myBalances[token] == initialBalance; - summarySafeTransferFrom(token, from, to, amount); + summarySafeTransferFrom(token, currentContract, to, amount); assert myBalances[token] == finalBalance; } + +rule transferRevertCondition(address token, address to, uint256 amount) { + uint256 initialBalance = getBalance(token, currentContract); + uint256 toInitialBalance = getBalance(token, to); + require to != currentContract => initialBalance + toInitialBalance <= to_mathint(getTotalSupply(token)); + require currentContract != 0 && to != 0; + + doTransfer@withrevert(token, to, amount); + + assert lastReverted == (initialBalance < amount); +} + +rule transferFromRevertCondition(address token, address from, address to, uint256 amount) { + uint256 initialBalance = getBalance(token, from); + uint256 toInitialBalance = getBalance(token, to); + uint256 allowance = getAllowance(token, from, currentContract); + require to != from => initialBalance + toInitialBalance <= to_mathint(getTotalSupply(token)); + require from != 0 && to != 0; + + doTransferFrom@withrevert(token, from, to, amount); + + assert lastReverted == (initialBalance < amount) || allowance < amount; +} From e52b3ce574b0a282c89f0b810b865d99004b6aa2 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 17 Aug 2023 16:48:25 +0200 Subject: [PATCH 2/3] Add missing totalSupply function. --- certora/dispatch/ERC20NoRevert.sol | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol index ff93b0862..93690e715 100644 --- a/certora/dispatch/ERC20NoRevert.sol +++ b/certora/dispatch/ERC20NoRevert.sol @@ -6,6 +6,7 @@ contract ERC20NoRevert { string public symbol; uint256 public decimals; address owner; + uint256 public totalSupply; mapping(address => uint256) public balanceOf; mapping(address => mapping(address => uint256)) public allowed; @@ -35,6 +36,9 @@ contract ERC20NoRevert { } function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + if (allowed[_from][msg.sender] < _amount) { + return false; + } allowed[_from][msg.sender] -= _amount; return _transfer(_from, _to, _amount); } @@ -51,5 +55,6 @@ contract ERC20NoRevert { function mint(address _receiver, uint256 _amount) public onlyOwner { balanceOf[_receiver] += _amount; + totalSupply += _amount; } } From c6f4614514eda540e226956255ebd97b9efc13f7 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 17 Aug 2023 17:28:58 +0200 Subject: [PATCH 3/3] Add totalSupply to USDT, some linting. --- certora/dispatch/ERC20NoRevert.sol | 2 +- certora/dispatch/ERC20USDT.sol | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol index 93690e715..8904f782c 100644 --- a/certora/dispatch/ERC20NoRevert.sol +++ b/certora/dispatch/ERC20NoRevert.sol @@ -5,7 +5,7 @@ contract ERC20NoRevert { string public name; string public symbol; uint256 public decimals; - address owner; + address public owner; uint256 public totalSupply; mapping(address => uint256) public balanceOf; mapping(address => mapping(address => uint256)) public allowed; diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol index a0400794d..95615e56e 100644 --- a/certora/dispatch/ERC20USDT.sol +++ b/certora/dispatch/ERC20USDT.sol @@ -7,7 +7,8 @@ contract ERC20USDT { string public name; string public symbol; uint256 public decimals; - address owner; + uint256 public totalSupply; + address public owner; mapping(address => uint256) public balanceOf; mapping(address => mapping(address => uint256)) public allowed; @@ -23,7 +24,7 @@ contract ERC20USDT { _; } - function _transfer(address _from, address _to, uint256 _amount) public { + function _transfer(address _from, address _to, uint256 _amount) internal { balanceOf[_from] -= _amount; balanceOf[_to] += _amount; } @@ -51,5 +52,6 @@ contract ERC20USDT { function mint(address _receiver, uint256 _amount) public onlyOwner { balanceOf[_receiver] += _amount; + totalSupply += _amount; } }