diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol new file mode 100644 index 000000000..3ae6e7e8c --- /dev/null +++ b/certora/harnesses/AccessControlHarness.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.5.0) (access/AccessControl.sol) + +pragma solidity ^0.8.0; + +import "../munged/access/AccessControl.sol"; + +contract AccessControlHarness is AccessControl { + +} 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/access/AccessControl.sol b/certora/munged/access/AccessControl.sol index 2ac203867..dec22fe8e 100644 --- a/certora/munged/access/AccessControl.sol +++ b/certora/munged/access/AccessControl.sol @@ -93,7 +93,7 @@ abstract contract AccessControl is Context, IAccessControl, ERC165 { * * _Available since v4.6._ */ - function _checkRole(bytes32 role) internal view virtual { + function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public _checkRole(role, _msgSender()); } diff --git a/certora/munged/governance/TimelockController.sol b/certora/munged/governance/TimelockController.sol index 621ebd87b..c6d30c665 100644 --- a/certora/munged/governance/TimelockController.sol +++ b/certora/munged/governance/TimelockController.sol @@ -24,10 +24,10 @@ contract TimelockController is AccessControl { bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); - uint256 internal constant _DONE_TIMESTAMP = uint256(1); + uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public mapping(bytes32 => uint256) private _timestamps; - uint256 private _minDelay; + uint256 public _minDelay; // HARNESS: private -> public /** * @dev Emitted when a call is scheduled as part of operation `id`. @@ -353,4 +353,11 @@ contract TimelockController is AccessControl { emit MinDelayChange(_minDelay, newDelay); _minDelay = newDelay; } + + + + function scheduleCheck1(bytes32 id) public virtual onlyRole(PROPOSER_ROLE) { + bool tmp = false; + require(tmp); + } } 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 e8ac5548b..718c13c60 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -1,7 +1,10 @@ certoraRun \ - certora/harnesses/TimelockControllerHarness.sol \ + certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ --solc solc8.2 \ --optimistic_loop \ - --cloud \ - --msg "sanity" \ No newline at end of file + --staging alex/unify-hash-functions \ + --rule_sanity \ + --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 9c0b99c5f..b4dc024ce 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,36 +1,328 @@ +using AccessControlHarness as AC + methods { - // hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) => uniqueHashGhost(target, value, data, predecessor, salt) + getTimestamp(bytes32) returns(uint256) envfree + _DONE_TIMESTAMP() returns(uint256) envfree + _minDelay() returns(uint256) envfree + getMinDelay() returns(uint256) envfree + + cancel(bytes32) + schedule(address, uint256, bytes, bytes32, bytes32, uint256) + execute(address, uint256, bytes, bytes32, bytes32) + + hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree // => uniqueHashGhost(target, value, data, predecessor, salt) } -// ghost uniqueHashGhost(address, uint256, bytes, bytes32, bytes32) returns bytes32; -// -// Assuming the hash is deterministic, and correlates the trio properly -// function hashUniquness(address target1, uint256 value1, bytes data1, bytes32 predecessor1, bytes32 salt1, -// address target2, uint256 value2, bytes data2, bytes32 predecessor2, bytes32 salt2){ -// require ((target1 != target2) || (value1 != value2) || (data1 != data2) || (predecessor1 != predecessor2) || (salt1 != salt2)) <=> -// (uniqueHashGhost(target1, value1, data1, predecessor1, salt1) != uniqueHashGhost(target2, value2, data2, predecessor2, salt2)); -// } -// -// -// rule keccakCheck(method f, env e){ -// address target; -// uint256 value; -// bytes data; -// bytes32 predecessor; -// bytes32 salt; -// -// hashUniquness(target, value, data, predecessor, salt, -// target, value, data, predecessor, salt); -// -// bytes32 a = hashOperation(e, target, value, data, predecessor, salt); -// bytes32 b = hashOperation(e, target, value, data, predecessor, salt); -// -// assert a == b, "hashes are different"; -// } -rule sanity(method f) { - env e; - calldataarg arg; - f(e, arg); - assert false; + +//////////////////////////////////////////////////////////////////////////// +// Definitions // +//////////////////////////////////////////////////////////////////////////// + + +definition unset(bytes32 id) returns bool = + getTimestamp(id) == 0; + +definition pending(bytes32 id) returns bool = + getTimestamp(id) > _DONE_TIMESTAMP(); + +definition ready(bytes32 id, env e) returns bool = + getTimestamp(id) > _DONE_TIMESTAMP() && getTimestamp(id) <= e.block.timestamp; + +definition done(bytes32 id) returns bool = + getTimestamp(id) == _DONE_TIMESTAMP(); + + + +//////////////////////////////////////////////////////////////////////////// +// Functions // +//////////////////////////////////////////////////////////////////////////// + + +function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ + require data.length < 7; + require hashOperation(target, value, data, predecessor, salt) == id; +} + + +//////////////////////////////////////////////////////////////////////////// +// Ghosts // +//////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////////// +// Invariants // +//////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// + + +rule keccakCheck(method f, env e){ + address target; + uint256 value; + bytes data; + bytes32 predecessor; + bytes32 salt; + + require data.length < 3; + + bytes32 a = hashOperation(target, value, data, predecessor, salt); + bytes32 b = hashOperation(target, value, data, predecessor, salt); + + assert a == b, "hashes are different"; +} + + + +///////////////////////////////////////////////////////////// +// STATE TRANSITIONS +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// unset() -> unset() || pending() only +rule unsetPendingTransitionGeneral(method f, env e){ + bytes32 id; + + require unset(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert pending(id) || unset(id); +} + + +// STATUS - verified +// unset() -> pending() via schedule() and scheduleBatch() only +rule unsetPendingTransitionMethods(method f, env e){ + bytes32 id; + + require unset(id); + + calldataarg args; + f(e, args); + + assert pending(id) => f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector , "Why do we need to follow the schedule?"; +} + + +// STATUS - verified +// ready() -> done() via execute() and executeBatch() only +rule readyDoneTransition(method f, env e){ + bytes32 id; + + require ready(id, e); + + calldataarg args; + f(e, args); + + assert done(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not done yet!"; +} + + +// STATUS - verified +// pending() -> cancelled() via cancel() only +rule pendingCancelledTransition(method f, env e){ + bytes32 id; + + require pending(id); + + calldataarg args; + f(e, args); + + assert unset(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; +} + + +// STATUS - verified +// done() -> nowhere +rule doneToNothingTransition(method f, env e){ + bytes32 id; + + require done(id); + + calldataarg args; + f(e, args); + + assert done(id), "Did you find a way to escape? There is no way! HA-HA-HA"; +} + + + +///////////////////////////////////////////////////////////// +// THE REST +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// only TimelockController contract can change minDealy +rule minDealyOnlyChange(method f, env e){ + uint256 delayBefore = _minDelay(); + + calldataarg args; + f(e, args); + + uint256 delayAfter = _minDelay(); + + assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!"; +} + + +// STATUS - verified +// Only proposers can schedule an operation +rule scheduleOnlyWay(method f, env e){ + uint256 delayBefore = _minDelay(); + + calldataarg args; + f(e, args); + + uint256 delayAfter = _minDelay(); + + assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!"; +} + + +// STATUS - in progress (need working hash) +// execute() is the only way to set timestamp to 1 +rule getTimestampOnlyChange(method f, env e){ + bytes32 id; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require getTimestamp(id) != 1; + hashIdCorrelation(id, target, value, data, predecessor, salt); + + calldataarg args; + // write helper function with values from hashOperation() call; + f(e, args); + + assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "Did you find a way to break the system?"; +} + + +// STATUS - in progress (need working hash) +// scheduled operation timestamp == block.timestamp + delay (kind of unit test) +rule scheduleCheck(method f, env e){ + bytes32 id; + + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require getTimestamp(id) < e.block.timestamp; + // require getMinDelay() > 0; + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert getTimestamp(id) == to_uint256(e.block.timestamp + getMinDelay()), "Time doesn't obey to mortal souls"; +} + + +// STATUS - in progress (need working hash) +// Cannot call execute on a pending (not ready) operation +rule cannotCallExecute(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require pending(id) && !ready(id, e); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - in progress +// in unset() execute() reverts +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); + require data.length < 4; + // require hashOperation(target, value, data, predecessor, salt) == id; + require unset(id); + + scheduleCheck1@withrevert(e, id); + + // execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Execute reverts => state returns to pending +rule executeRevertEffectCheck(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + 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"; +} + + +// STATUS - verified +// Canceled operations cannot be executed → can’t move from canceled to ready +rule cancelledNotExecuted(method f, env e){ + bytes32 id; + + require unset(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert !done(id), "The ship is not a creature of the air"; +} + + +// STATUS - in progress +// Only proposers can schedule an operation +rule onlyProposer(method f, env e){ + bytes32 id; + bytes32 role; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require unset(id); + hashIdCorrelation(id, target, value, data, predecessor, salt); + + AC._checkRole@withrevert(e, role); + + bool isCheckRoleReverted = lastReverted; + + schedule@withrevert(e, target, value, data, predecessor, salt, delay); + + bool isScheduleReverted = lastReverted; + + assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +} + + +// STATUS - in progress +// Ready = has waited minimum period after pending +rule cooldown(method f, env e, env e2){ + bytes32 id; + + require unset(id); + + calldataarg args; + f(e, args); + + // e.block.timestamp - delay > time scheduled => ready() + assert e.block.timestamp >= getTimestamp(id) => ready(id, e), "No rush! When I'm ready, I'm ready"; } \ No newline at end of file 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) +}