diff --git a/certora/harnesses/ERC20FlashMintHarness.sol b/certora/harnesses/ERC20FlashMintHarness.sol new file mode 100644 index 000000000..aec8c2238 --- /dev/null +++ b/certora/harnesses/ERC20FlashMintHarness.sol @@ -0,0 +1,5 @@ +import "../munged/token/ERC20/extensions/ERC20FlashMint.sol"; + +contract ERC20FlashMintHarness is ERC20FlashMint { + constructor(string memory name, string memory symbol) ERC20(name, symbol) {} +} diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index 23e37df11..b000afde4 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -6,5 +6,12 @@ contract ERC20WrapperHarness is ERC20Wrapper { ERC20Wrapper(underlyingToken) ERC20(_name, _symbol) {} -} + function underlyingTotalSupply() public view returns (uint256) { + return underlying.totalSupply(); + } + + function underlyingBalanceOf(address account) public view returns (uint256) { + return underlying.balanceOf(account); + } +} \ No newline at end of file diff --git a/certora/harnesses/IERC3156FlashBorrowerHarness.sol b/certora/harnesses/IERC3156FlashBorrowerHarness.sol new file mode 100644 index 000000000..097a5c2fd --- /dev/null +++ b/certora/harnesses/IERC3156FlashBorrowerHarness.sol @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (interfaces/IERC3156FlashBorrower.sol) + +import "../munged/interfaces/IERC3156FlashBorrower.sol"; + +pragma solidity ^0.8.0; + +contract IERC3156FlashBorrowerHarness is IERC3156FlashBorrower { + bytes32 somethingToReturn; + + function onFlashLoan( + address initiator, + address token, + uint256 amount, + uint256 fee, + bytes calldata data + ) external override returns (bytes32){ + return somethingToReturn; + } +} diff --git a/certora/helpers/DummyERC20A.sol b/certora/helpers/DummyERC20A.sol new file mode 100644 index 000000000..188b92608 --- /dev/null +++ b/certora/helpers/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/helpers/DummyERC20B.sol b/certora/helpers/DummyERC20B.sol new file mode 100644 index 000000000..0f97f1efc --- /dev/null +++ b/certora/helpers/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/helpers/DummyERC20Impl.sol b/certora/helpers/DummyERC20Impl.sol new file mode 100644 index 000000000..42e7f2302 --- /dev/null +++ b/certora/helpers/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/munged/governance/TimelockController.sol b/certora/munged/governance/TimelockController.sol index da38df8f3..3da7e2170 100644 --- a/certora/munged/governance/TimelockController.sol +++ b/certora/munged/governance/TimelockController.sol @@ -353,4 +353,10 @@ contract TimelockController is AccessControl { emit MinDelayChange(_minDelay, newDelay); _minDelay = newDelay; } + + + + function scheduleCheck1(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) { + require(false); + } } diff --git a/certora/munged/token/ERC20/ERC20.sol b/certora/munged/token/ERC20/ERC20.sol index dc963af88..fec3327ea 100644 --- a/certora/munged/token/ERC20/ERC20.sol +++ b/certora/munged/token/ERC20/ERC20.sol @@ -277,7 +277,7 @@ contract ERC20 is Context, IERC20, IERC20Metadata { * - `account` cannot be the zero address. * - `account` must have at least `amount` tokens. */ - function _burn(address account, uint256 amount) internal virtual { + function _burn(address account, uint256 amount) public virtual returns (bool) { // HARNESS: internal -> public require(account != address(0), "ERC20: burn from the zero address"); _beforeTokenTransfer(account, address(0), amount); @@ -292,6 +292,8 @@ contract ERC20 is Context, IERC20, IERC20Metadata { emit Transfer(account, address(0), amount); _afterTokenTransfer(account, address(0), amount); + + return true; } /** diff --git a/certora/munged/token/ERC20/extensions/ERC20FlashMint.sol b/certora/munged/token/ERC20/extensions/ERC20FlashMint.sol index cbcf3b60f..2a811cacf 100644 --- a/certora/munged/token/ERC20/extensions/ERC20FlashMint.sol +++ b/certora/munged/token/ERC20/extensions/ERC20FlashMint.sol @@ -40,9 +40,11 @@ abstract contract ERC20FlashMint is ERC20, IERC3156FlashLender { require(token == address(this), "ERC20FlashMint: wrong token"); // silence warning about unused variable without the addition of bytecode. amount; - return 0; + return fee; // HARNESS: made "return" nonzero } + uint256 public fee; // HARNESS: added it to simulate random fee amount + /** * @dev Performs a flash loan. New tokens are minted and sent to the * `receiver`, who is required to implement the {IERC3156FlashBorrower} @@ -70,7 +72,7 @@ abstract contract ERC20FlashMint is ERC20, IERC3156FlashLender { uint256 fee = flashFee(token, amount); _mint(address(receiver), amount); require( - receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE, + receiver.onFlashLoan(msg.sender, token, amount, fee, data) == _RETURN_VALUE, // HAVOC_ALL "ERC20FlashMint: invalid return value" ); uint256 currentAllowance = allowance(address(receiver), address(this)); diff --git a/certora/munged/token/ERC20/extensions/ERC20Wrapper.sol b/certora/munged/token/ERC20/extensions/ERC20Wrapper.sol index 32a3b830a..b7027441f 100644 --- a/certora/munged/token/ERC20/extensions/ERC20Wrapper.sol +++ b/certora/munged/token/ERC20/extensions/ERC20Wrapper.sol @@ -44,7 +44,7 @@ abstract contract ERC20Wrapper is ERC20 { * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal * function that can be exposed with access control if desired. */ - function _recover(address account) internal virtual returns (uint256) { + function _recover(address account) public virtual returns (uint256) { // HARNESS: internal -> public uint256 value = underlying.balanceOf(address(this)) - totalSupply(); _mint(account, value); return value; diff --git a/certora/scripts/verifyERC20FlashMint.sh b/certora/scripts/verifyERC20FlashMint.sh new file mode 100644 index 000000000..84ec58eff --- /dev/null +++ b/certora/scripts/verifyERC20FlashMint.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC20FlashMintHarness.sol certora/harnesses/IERC3156FlashBorrowerHarness.sol \ + certora/munged/token/ERC20/ERC20.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --staging \ + --rule_sanity \ + --msg "letsWatchItBurns" + \ No newline at end of file diff --git a/certora/scripts/verifyERC20Wrapper.sh b/certora/scripts/verifyERC20Wrapper.sh new file mode 100644 index 000000000..e4557724f --- /dev/null +++ b/certora/scripts/verifyERC20Wrapper.sh @@ -0,0 +1,10 @@ +certoraRun \ + certora/harnesses/ERC20WrapperHarness.sol \ + certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \ + --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --staging \ + --rule_sanity \ + --msg "all check" + \ No newline at end of file diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh index 696ab2595..718c13c60 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -3,7 +3,8 @@ certoraRun \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ --solc solc8.2 \ --optimistic_loop \ - --cloud alex/uhf-more-precision \ + --staging alex/unify-hash-functions \ --rule_sanity \ - --msg "sanity flag check" + --rule "$1" \ + --msg "$1 false check with hash" \ No newline at end of file diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec new file mode 100644 index 000000000..db8cddcad --- /dev/null +++ b/certora/specs/ERC20FlashMint.spec @@ -0,0 +1,37 @@ +import "erc20.spec" + +methods { + onFlashLoan(address, address, uint256, uint256, bytes) => HAVOC_ALL // HAVOC_ECF + + _burn(address account, uint256 amount) returns(bool) => specBurn(account, amount); +} + +ghost mapping(address => uint256) trackedBurnAmount; + +function specBurn(address account, uint256 amount) returns bool { // retuns needed to overcome current CVL limitations: "could not type expression "specBurn(account,amount)", message: A summary must return a simple type, but specBurn(account,amount) returns 'void'" + trackedBurnAmount[account] = amount; + return true; +} + +// ghost to save args that were passed to burn function +// summarize burn +// assert ghost == amount + fee + + +// STATUS - in progress +// HAVOC_ALL - everything is havoced => violation +// HAVOC_ECF - verified +// https://vaas-stg.certora.com/output/3106/8795450b626f2ca53a2b/?anonymousKey=dd774da10cc595e4e38357af9e4f50bf2c0cb02a +// fee + flashLoan amount is burned +rule letsWatchItBurns(env e){ + address receiver; address token; uint256 amount; bytes data; + require amount > 0; + + uint256 feeBefore = flashFee(e, token, amount); + + flashLoan(e, receiver, token, amount, data); + + uint256 burned = trackedBurnAmount[receiver]; + + assert to_mathint(amount + feeBefore) == burned, "cheater"; +} \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec new file mode 100644 index 000000000..6e40c61d2 --- /dev/null +++ b/certora/specs/ERC20Wrapper.spec @@ -0,0 +1,203 @@ +import "erc20.spec" + +methods { + underlying() returns(address) envfree + underlyingTotalSupply() returns(uint256) envfree + underlyingBalanceOf(address) returns(uint256) envfree + + depositFor(address, uint256) returns(bool) + withdrawTo(address, uint256) returns(bool) + _recover(address) returns(uint256) +} + + +// STATUS - verified +// totalsupply of wrapped should be less than or equal to underlying (assuming no transfer they should be equal) - solvency +invariant whatAboutTotal(env e) + totalSupply(e) <= underlyingTotalSupply() + filtered { f -> f.selector != certorafallback_0().selector } + { + preserved { + require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); + require underlying() != currentContract; + } + preserved depositFor(address account, uint256 amount) with (env e2){ + require underlyingBalanceOf(currentContract) <= underlyingTotalSupply(); + require totalSupply(e) + amount <= underlyingTotalSupply(); + require underlying() != currentContract; + } + } + + +// STATUS - verified +// check correct values update by depositFor() +rule depositForSpecBasic(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 underlyingTotalBefore = underlyingTotalSupply(); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + depositFor(e, account, amount); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 underlyingTotalAfter = underlyingTotalSupply(); + uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); + + assert wrapperTotalBefore == wrapperTotalAfter - amount, "wrapper total wrong update"; + assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; + assert underlyingThisBalanceBefore == underlyingThisBalanceAfter - amount, "underlying this balance wrong update"; +} + + +rule depositForSpecWrapper(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + + depositFor(e, account, amount); + + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount, "wrapper balances wrong update"; + assert account != e.msg.sender => wrapperUserBalanceBefore == wrapperUserBalanceAfter - amount + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; +} + + +rule depositForSpecUnderlying(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account); + + depositFor(e, account, amount); + + uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); + + assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount, "underlying balances wrong update"; + + assert account != e.msg.sender && account == currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update"; + + assert account != e.msg.sender && account != currentContract => underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + amount + && underlyingUserBalanceBefore == underlyingUserBalanceAfter, "underlying balances wrong update"; +} + + +// STATUS - verified +// check correct values update by withdrawTo() +rule withdrawToSpecBasic(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 underlyingTotalBefore = underlyingTotalSupply(); + + withdrawTo(e, account, amount); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 underlyingTotalAfter = underlyingTotalSupply(); + + assert wrapperTotalBefore == wrapperTotalAfter + amount, "wrapper total wrong update"; + assert underlyingTotalBefore == underlyingTotalAfter, "underlying total was updated"; +} + + +rule withdrawToSpecWrapper(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + + withdrawTo(e, account, amount); + + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert account == e.msg.sender => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter + amount, "wrapper user balance wrong update"; + assert account != e.msg.sender => wrapperSenderBalanceBefore == wrapperSenderBalanceAfter + amount + && wrapperUserBalanceBefore == wrapperUserBalanceAfter, "wrapper user balance wrong update"; +} + + +rule withdrawToSpecUnderlying(env e){ + address account; uint256 amount; + + require e.msg.sender != currentContract; + require underlying() != currentContract; + + uint256 underlyingSenderBalanceBefore = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceBefore = underlyingBalanceOf(account); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + withdrawTo(e, account, amount); + + uint256 underlyingSenderBalanceAfter = underlyingBalanceOf(e.msg.sender); + uint256 underlyingUserBalanceAfter = underlyingBalanceOf(account); + uint256 underlyingThisBalanceAfter = underlyingBalanceOf(currentContract); + + assert account == e.msg.sender => underlyingSenderBalanceBefore == underlyingUserBalanceBefore + && underlyingSenderBalanceAfter == underlyingUserBalanceAfter + && underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount, "underlying balances wrong update (acc == sender)"; + + assert account != e.msg.sender && account == currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter, "underlying balances wrong update (acc == contract)"; + assert account != e.msg.sender && account != currentContract => underlyingUserBalanceBefore == underlyingUserBalanceAfter - amount + && underlyingSenderBalanceBefore == underlyingSenderBalanceAfter + && underlyingThisBalanceBefore == underlyingThisBalanceAfter + amount, "underlying balances wrong update (acc != contract)"; +} + + +// STATUS - verified +// check correct values update by _recover() +rule recoverSpec(env e){ + address account; uint256 amount; // e.msg.sender + require underlying() != currentContract; + + require e.msg.sender != currentContract; + + uint256 wrapperTotalBefore = totalSupply(e); + uint256 wrapperUserBalanceBefore = balanceOf(e, account); + uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); + + mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; + + _recover(e, account); + + uint256 wrapperTotalAfter = totalSupply(e); + uint256 wrapperUserBalanceAfter = balanceOf(e, account); + uint256 wrapperSenderBalanceAfter = balanceOf(e, e.msg.sender); + + assert wrapperTotalBefore == wrapperTotalAfter - value, "wrapper total wrong update"; + assert e.msg.sender == account => wrapperUserBalanceBefore == wrapperSenderBalanceBefore + && wrapperUserBalanceAfter == wrapperSenderBalanceAfter + && wrapperUserBalanceBefore == wrapperUserBalanceAfter - value, "wrapper balances wrong update"; + assert e.msg.sender != account => wrapperUserBalanceBefore == wrapperUserBalanceAfter - value + && wrapperSenderBalanceBefore == wrapperSenderBalanceAfter, "wrapper balances wrong update"; +} \ No newline at end of file diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index b8a15cbe3..f7896a1b7 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -40,7 +40,7 @@ definition done(bytes32 id) returns bool = function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ - require data.length < 3; + require data.length < 7; require hashOperation(target, value, data, predecessor, salt) == id; } @@ -241,16 +241,20 @@ rule cannotCallExecute(method f, env e){ } -// STATUS - in progress (need working hash) +// STATUS - in progress // in unset() execute() reverts -rule executeRevertFromUnset(method f, env e){ +rule executeRevertFromUnset(method f, env e, env e2){ address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; bytes32 id; - hashIdCorrelation(id, target, value, data, predecessor, salt); + // hashIdCorrelation(id, target, value, data, predecessor, salt); + require data.length < 4; + require hashOperation(target, value, data, predecessor, salt) == id; require unset(id); - execute@withrevert(e, target, value, data, predecessor, salt); + scheduleCheck1@withrevert(e, id); + + // execute@withrevert(e, target, value, data, predecessor, salt); assert lastReverted, "you go against execution nature"; } @@ -266,6 +270,7 @@ rule executeRevertEffectCheck(method f, env e){ require pending(id) && !ready(id, e); execute@withrevert(e, target, value, data, predecessor, salt); + bool reverted = lastReverted; assert lastReverted => pending(id) && !ready(id, e), "you go against execution nature"; } @@ -286,7 +291,7 @@ rule cancelledNotExecuted(method f, env e){ } -// STATUS - in progress (need working hash) +// STATUS - in progress // Only proposers can schedule an operation rule onlyProposer(method f, env e){ bytes32 id; diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec new file mode 100644 index 000000000..b12fec167 --- /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) +}