From 60ab7a13ad77535f3ba4e03d72ef79bdf2a0b81a Mon Sep 17 00:00:00 2001 From: sarit Date: Tue, 4 Jul 2023 10:42:01 +0300 Subject: [PATCH 1/4] Adding general rules and confs for erc20 and valult contracts --- .../certora/conf/generalRules_ERC20.conf | 9 + .../certora/conf/generalRules_VAULT.conf | 9 + .../GeneralExamples/certora/spec/general.spec | 122 ++++++ .../GeneralExamples/contracts/ERC20.sol | 400 ++++++++++++++++++ .../GeneralExamples/contracts/IERC20.sol | 133 ++++++ .../contracts/IERC20Metadata.sol | 28 ++ .../GeneralExamples/contracts/Vault.sol | 82 ++++ 7 files changed, 783 insertions(+) create mode 100644 CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf create mode 100644 CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf create mode 100644 CVLByExamples/GeneralExamples/certora/spec/general.spec create mode 100644 CVLByExamples/GeneralExamples/contracts/ERC20.sol create mode 100644 CVLByExamples/GeneralExamples/contracts/IERC20.sol create mode 100644 CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol create mode 100644 CVLByExamples/GeneralExamples/contracts/Vault.sol diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf b/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf new file mode 100644 index 00000000..b63c38e7 --- /dev/null +++ b/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "contracts/ERC20.sol:ERC20" + ], + "verify": "ERC20:certora/spec/general.spec", + "solc": "solc8.17", + "solc_args": [], + "msg": "genral Rules on ERC20 contract" +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf b/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf new file mode 100644 index 00000000..2f556d4f --- /dev/null +++ b/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "contracts/Vault.sol:Vault" + ], + "verify": "Vault:certora/spec/general.spec", + "solc": "solc8.17", + "solc_args": [], + "msg": "genral Rules on Vault contract" +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/spec/general.spec b/CVLByExamples/GeneralExamples/certora/spec/general.spec new file mode 100644 index 00000000..0a989e26 --- /dev/null +++ b/CVLByExamples/GeneralExamples/certora/spec/general.spec @@ -0,0 +1,122 @@ +using DummyERC20A as erc20; + +methods { + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + + function erc20.balanceOf(address) external returns (uint256) envfree; +} + +/* + Property: Find and show a path for each method. +*/ +rule reachability(method f) +{ + env e; + calldataarg args; + f(e,args); + satisfy true; +} + +/* + Property: Define and check functions that should never revert + Notice: use f.selector to state which functions should not revert,e.g.f.selector == sig:balanceOf(address).selector +*/ +definition nonReveritngFunction(method f ) returns bool = true; + +rule noRevert(method f) filtered {f -> nonReveritngFunction(f) } +{ + env e; + calldataarg arg; + //consider auto filtering for non-payable functions + require e.msg.value == 0; + f@withrevert(e, arg); + assert !lastReverted, "method should not revert"; +} + + +/* + Property: Checks if a function can be frontrun + Notice: Can be enhanced to check more than one function as rules can be double-parameteric +*/ +rule simpleFrontRunning(method f, method g) filtered { f-> !f.isView, g-> !g.isView } +{ + env e1; + calldataarg arg; + + storage initialStorage = lastStorage; + f(e1, arg); + + + env e2; + calldataarg arg2; + require e2.msg.sender != e1.msg.sender; + g(e2, arg2) at initialStorage; + + f@withrevert(e1, arg); + bool succeeded = !lastReverted; + + assert succeeded, "should be called also if frontrunned"; +} + + +/** + @title - This rule find which functions are privileged. + @notice A function is privileged if there is only one address that can call it. + @dev The rules finds this by finding which functions can be called by two different users. +*/ + +rule privilegedOperation(method f, address privileged) +{ + env e1; + calldataarg arg; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + f@withrevert(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "function is privileged"; +} + + +rule decreaseInSystemEth(method f) { + + uint256 before = nativeBalances[currentContract]; + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = nativeBalances[currentContract]; + + assert after >= before || false ; /* fill in cases where eth can decrease */ +} + + +rule decreaseInERC20(method f) { + + uint256 before = erc20.balanceOf(currentContract); + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = erc20.balanceOf(currentContract); + + assert after >= before || false ; /* fill in cases eth can decrease */ + +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/contracts/ERC20.sol b/CVLByExamples/GeneralExamples/contracts/ERC20.sol new file mode 100644 index 00000000..44fcc7e4 --- /dev/null +++ b/CVLByExamples/GeneralExamples/contracts/ERC20.sol @@ -0,0 +1,400 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (token/ERC20/ERC20.sol) + +pragma solidity ^0.8.0; + +import "./IERC20.sol"; +import "./IERC20Metadata.sol"; + +/** + * @dev Implementation of the {IERC20} interface. + * + * This implementation is agnostic to the way tokens are created. This means + * that a supply mechanism has to be added in a derived contract using {_mint}. + * For a generic mechanism see {ERC20PresetMinterPauser}. + * + * TIP: For a detailed writeup see our guide + * https://forum.zeppelin.solutions/t/how-to-implement-erc20-supply-mechanisms/226[How + * to implement supply mechanisms]. + * + * We have followed general OpenZeppelin Contracts guidelines: functions revert + * instead returning `false` on failure. This behavior is nonetheless + * conventional and does not conflict with the expectations of ERC20 + * applications. + * + * Additionally, an {Approval} event is emitted on calls to {transferFrom}. + * This allows applications to reconstruct the allowance for all accounts just + * by listening to said events. Other implementations of the EIP may not emit + * these events, as it isn't required by the specification. + * + * Finally, the non-standard {decreaseAllowance} and {increaseAllowance} + * functions have been added to mitigate the well-known issues around setting + * allowances. See {IERC20-approve}. + */ +contract ERC20 is IERC20, IERC20Metadata { + mapping(address => uint256) private _balances; + + mapping(address => mapping(address => uint256)) private _allowances; + + uint256 private _totalSupply; + + address public _owner; + + /** + * @dev Sets the values for {name} and {symbol}. + * + * The default value of {decimals} is 18. To select a different value for + * {decimals} you should overload it. + * + * All two of these values are immutable: they can only be set once during + * construction. + */ + constructor() { + } + + modifier onlyOwner() { + require(_owner == msg.sender); + _; + } + + /** + * @dev Returns the name of the token. + */ + function name() public view virtual override returns (string memory) { + return ""; + } + + /** + * @dev Returns the symbol of the token, usually a shorter version of the + * name. + */ + function symbol() public view virtual override returns (string memory) { + return ""; + } + + /** + * @dev Returns the number of decimals used to get its user representation. + * For example, if `decimals` equals `2`, a balance of `505` tokens should + * be displayed to a user as `5.05` (`505 / 10 ** 2`). + * + * Tokens usually opt for a value of 18, imitating the relationship between + * Ether and Wei. This is the value {ERC20} uses, unless this function is + * overridden; + * + * NOTE: This information is only used for _display_ purposes: it in + * no way affects any of the arithmetic of the contract, including + * {IERC20-balanceOf} and {IERC20-transfer}. + */ + function decimals() public view virtual override returns (uint8) { + return 18; + } + + /** + * @dev See {IERC20-totalSupply}. + */ + function totalSupply() public view virtual override returns (uint256) { + return _totalSupply; + } + + /** + * @dev See {IERC20-balanceOf}. + */ + function balanceOf(address account) + public + view + virtual + override + returns (uint256) + { + return _balances[account]; + } + + /** + * @dev See {IERC20-transfer}. + * + * Requirements: + * + * - `recipient` cannot be the zero address. + * - the caller must have a balance of at least `amount`. + */ + function transfer(address recipient, uint256 amount) + public + virtual + override + returns (bool) + { + _transfer(msg.sender, recipient, amount); + return true; + } + + /** + * @dev See {IERC20-allowance}. + */ + function allowance(address owner, address spender) + public + view + virtual + override + returns (uint256) + { + return _allowances[owner][spender]; + } + + /** + * @dev See {IERC20-approve}. + * + * Requirements: + * + * - `spender` cannot be the zero address. + */ + function approve(address spender, uint256 amount) + public + virtual + override + returns (bool) + { + _approve(msg.sender, spender, amount); + return true; + } + + /** + * @dev See {IERC20-transferFrom}. + * + * Emits an {Approval} event indicating the updated allowance. This is not + * required by the EIP. See the note at the beginning of {ERC20}. + * + * Requirements: + * + * - `sender` and `recipient` cannot be the zero address. + * - `sender` must have a balance of at least `amount`. + * - the caller must have allowance for ``sender``'s tokens of at least + * `amount`. + */ + function transferFrom( + address sender, + address recipient, + uint256 amount + ) public virtual override returns (bool) { + uint256 currentAllowance = _allowances[sender][msg.sender]; + require( + currentAllowance >= amount, + "ERC20: transfer amount exceeds allowance" + ); + unchecked { + _approve(sender, msg.sender, currentAllowance - amount); + } + + _transfer(sender, recipient, amount); + + return true; + } + + /** + * @dev Atomically increases the allowance granted to `spender` by the caller. + * + * This is an alternative to {approve} that can be used as a mitigation for + * problems described in {IERC20-approve}. + * + * Emits an {Approval} event indicating the updated allowance. + * + * Requirements: + * + * - `spender` cannot be the zero address. + */ + function increaseAllowance(address spender, uint256 addedValue) + public + virtual + returns (bool) + { + _approve( + msg.sender, + spender, + _allowances[msg.sender][spender] + addedValue + ); + return true; + } + + /** + * @dev Atomically decreases the allowance granted to `spender` by the caller. + * + * This is an alternative to {approve} that can be used as a mitigation for + * problems described in {IERC20-approve}. + * + * Emits an {Approval} event indicating the updated allowance. + * + * Requirements: + * + * - `spender` cannot be the zero address. + * - `spender` must have allowance for the caller of at least + * `subtractedValue`. + */ + function decreaseAllowance(address spender, uint256 subtractedValue) + public + virtual + returns (bool) + { + uint256 currentAllowance = _allowances[msg.sender][spender]; + require( + currentAllowance >= subtractedValue, + "ERC20: decreased allowance below zero" + ); + unchecked { + _approve(msg.sender, spender, currentAllowance - subtractedValue); + } + + return true; + } + + /** + * @dev Moves `amount` of tokens from `sender` to `recipient`. + * + * This internal function is equivalent to {transfer}, and can be used to + * e.g. implement automatic token fees, slashing mechanisms, etc. + * + * Emits a {Transfer} event. + * + * Requirements: + * + * - `sender` cannot be the zero address. + * - `recipient` cannot be the zero address. + * - `sender` must have a balance of at least `amount`. + */ + function _transfer( + address sender, + address recipient, + uint256 amount + ) internal virtual { + require(sender != address(0), "ERC20: transfer from the zero address"); + require(recipient != address(0), "ERC20: transfer to the zero address"); + + _beforeTokenTransfer(sender, recipient, amount); + + uint256 senderBalance = _balances[sender]; + require( + senderBalance >= amount, + "ERC20: transfer amount exceeds balance" + ); + unchecked { + _balances[sender] = senderBalance - amount; + } + _balances[recipient] += amount; + + emit Transfer(sender, recipient, amount); + + _afterTokenTransfer(sender, recipient, amount); + } + + /** @dev Creates `amount` tokens and assigns them to `account`, increasing + * the total supply. + * + * Emits a {Transfer} event with `from` set to the zero address. + * + * Requirements: + * + * - `account` cannot be the zero address. + */ + function mint(address account, uint256 amount) onlyOwner() public virtual override { + require(account != address(0), "ERC20: mint to the zero address"); + + _beforeTokenTransfer(address(0), account, amount); + + _totalSupply += amount; + _balances[account] += amount; + emit Transfer(address(0), account, amount); + + _afterTokenTransfer(address(0), account, amount); + } + + /** + * @dev Destroys `amount` tokens from `account`, reducing the + * total supply. + * + * Emits a {Transfer} event with `to` set to the zero address. + * + * Requirements: + * + * - `account` cannot be the zero address. + * - `account` must have at least `amount` tokens. + */ + function burn(address account, uint256 amount) onlyOwner() public virtual override { + require(account != address(0), "ERC20: burn from the zero address"); + + _beforeTokenTransfer(account, address(0), amount); + + uint256 accountBalance = _balances[account]; + require(accountBalance >= amount, "ERC20: burn amount exceeds balance"); + unchecked { + _balances[account] = accountBalance - amount; + } + _totalSupply -= amount; + + emit Transfer(account, address(0), amount); + + _afterTokenTransfer(account, address(0), amount); + } + + /** + * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens. + * + * This internal function is equivalent to `approve`, and can be used to + * e.g. set automatic allowances for certain subsystems, etc. + * + * Emits an {Approval} event. + * + * Requirements: + * + * - `owner` cannot be the zero address. + * - `spender` cannot be the zero address. + */ + function _approve( + address owner, + address spender, + uint256 amount + ) internal virtual { + require(owner != address(0), "ERC20: approve from the zero address"); + require(spender != address(0), "ERC20: approve to the zero address"); + _allowances[owner][spender] = amount; + emit Approval(owner, spender, amount); + } + + /** + * @dev Hook that is called before any transfer of tokens. This includes + * minting and burning. + * + * Calling conditions: + * + * - when `from` and `to` are both non-zero, `amount` of ``from``'s tokens + * will be transferred to `to`. + * - when `from` is zero, `amount` tokens will be minted for `to`. + * - when `to` is zero, `amount` of ``from``'s tokens will be burned. + * - `from` and `to` are never both zero. + * + * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks]. + */ + function _beforeTokenTransfer( + address from, + address to, + uint256 amount + ) internal virtual {} + + /** + * @dev Hook that is called after any transfer of tokens. This includes + * minting and burning. + * + * Calling conditions: + * + * - when `from` and `to` are both non-zero, `amount` of ``from``'s tokens + * has been transferred to `to`. + * - when `from` is zero, `amount` tokens have been minted for `to`. + * - when `to` is zero, `amount` of ``from``'s tokens have been burned. + * - `from` and `to` are never both zero. + * + * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks]. + */ + function _afterTokenTransfer( + address from, + address to, + uint256 amount + ) internal virtual {} + +} diff --git a/CVLByExamples/GeneralExamples/contracts/IERC20.sol b/CVLByExamples/GeneralExamples/contracts/IERC20.sol new file mode 100644 index 00000000..ae342979 --- /dev/null +++ b/CVLByExamples/GeneralExamples/contracts/IERC20.sol @@ -0,0 +1,133 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.0; + +/** + * @dev Implementation of the {IERC20} interface. + * + * This implementation is agnostic to the way tokens are created. This means + * that a supply mechanism has to be added in a derived contract using {_mint}. + * For a generic mechanism see {ERC20PresetMinterPauser}. + * + * TIP: For a detailed writeup see our guide + * https://forum.zeppelin.solutions/t/how-to-implement-erc20-supply-mechanisms/226[How + * to implement supply mechanisms]. + * + * We have followed general OpenZeppelin Contracts guidelines: functions revert + * instead returning `false` on failure. This behavior is nonetheless + * conventional and does not conflict with the expectations of ERC20 + * applications. + * + * Additionally, an {Approval} event is emitted on calls to {transferFrom}. + * This allows applications to reconstruct the allowance for all accounts just + * by listening to said events. Other implementations of the EIP may not emit + * these events, as it isn't required by the specification. + * + * Finally, the non-standard {decreaseAllowance} and {increaseAllowance} + * functions have been added to mitigate the well-known issues around setting + * allowances. See {IERC20-approve}. + */ + +/** + * Interface of the ERC20 standard as defined in the EIP. + */ +interface IERC20 { + /** + * @dev Returns the amount of tokens in existence. + */ + function totalSupply() external view returns (uint256); + + /** + * @dev Returns the amount of tokens owned by `account`. + */ + function balanceOf(address account) external view returns (uint256); + + /** + * @dev Moves `amount` tokens from the caller's account to `recipient`. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transfer(address recipient, uint256 amount) + external + returns (bool); + + /** + * Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) + external + view + returns (uint256); + + /** + * Sets `amount` as the allowance of `spender` over the caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + function approve(address spender, uint256 amount) external returns (bool); + + /** + * @dev Moves `amount` tokens from `sender` to `recipient` using the + * allowance mechanism. `amount` is then deducted from the caller's + * allowance. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool); + + /** + * @dev generates token to the system by awarding a specified user `account` + * a specific `amount` + * + * Emits a {Transfer} event. + */ + function mint(address, uint256) external; + + /** + * @dev removes token from the system by burning a specific `amount` + * from a specified user `account` + * + * Emits a {Transfer} event. + */ + function burn(address, uint256) external; + + /** + * @dev Emitted when `value` tokens are moved from one account (`from`) to + * another (`to`). + * + * Note that `value` may be zero. + */ + event Transfer(address indexed from, address indexed to, uint256 value); + + /** + * @dev Emitted when the allowance of a `spender` for an `owner` is set by + * a call to {approve}. `value` is the new allowance. + */ + event Approval( + address indexed owner, + address indexed spender, + uint256 value + ); +} diff --git a/CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol b/CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol new file mode 100644 index 00000000..982bc39e --- /dev/null +++ b/CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (token/ERC20/extensions/IERC20Metadata.sol) + +pragma solidity ^0.8.0; + +import "./IERC20.sol"; + +/** + * @dev Interface for the optional metadata functions from the ERC20 standard. + * + * _Available since v4.1._ + */ +interface IERC20Metadata is IERC20 { + /** + * @dev Returns the name of the token. + */ + function name() external view returns (string memory); + + /** + * @dev Returns the symbol of the token. + */ + function symbol() external view returns (string memory); + + /** + * @dev Returns the decimals places of the token. + */ + function decimals() external view returns (uint8); +} diff --git a/CVLByExamples/GeneralExamples/contracts/Vault.sol b/CVLByExamples/GeneralExamples/contracts/Vault.sol new file mode 100644 index 00000000..e546f12a --- /dev/null +++ b/CVLByExamples/GeneralExamples/contracts/Vault.sol @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.17; + +contract Vault { + IERC20 public immutable token; + + uint public totalSupply; + mapping(address => uint) public balanceOf; + + constructor(address _token) { + token = IERC20(_token); + } + + function _mint(address _to, uint _shares) private { + totalSupply += _shares; + balanceOf[_to] += _shares; + } + + function _burn(address _from, uint _shares) private { + totalSupply -= _shares; + balanceOf[_from] -= _shares; + } + + function deposit(uint _amount) external { + /* + a = amount + B = balance of token before deposit + T = total supply + s = shares to mint + + (T + s) / T = (a + B) / B + + s = aT / B + */ + uint shares; + if (totalSupply == 0) { + shares = _amount; + } else { + shares = (_amount * totalSupply) / token.balanceOf(address(this)); + } + + _mint(msg.sender, shares); + token.transferFrom(msg.sender, address(this), _amount); + } + + function withdraw(uint _shares) external { + /* + a = amount + B = balance of token before withdraw + T = total supply + s = shares to burn + + (T - s) / T = (B - a) / B + + a = sB / T + */ + uint amount = (_shares * token.balanceOf(address(this))) / totalSupply; + _burn(msg.sender, _shares); + token.transfer(msg.sender, amount); + } +} + +interface IERC20 { + function totalSupply() external view returns (uint); + + function balanceOf(address account) external view returns (uint); + + function transfer(address recipient, uint amount) external returns (bool); + + function allowance(address owner, address spender) external view returns (uint); + + function approve(address spender, uint amount) external returns (bool); + + function transferFrom( + address sender, + address recipient, + uint amount + ) external returns (bool); + + event Transfer(address indexed from, address indexed to, uint amount); + event Approval(address indexed owner, address indexed spender, uint amount); +} From 5a94adab9fe8f2147990a2f203d8699dbcd76bd8 Mon Sep 17 00:00:00 2001 From: sarit Date: Thu, 6 Jul 2023 12:32:21 +0300 Subject: [PATCH 2/4] adding ERC20Helper --- .../certora/conf/generalRules_ERC20.conf | 4 ++-- .../certora/conf/generalRules_VAULT.conf | 5 +++-- .../certora/helpersContracts/ERC20Helper.sol | 10 ++++++++++ .../GeneralExamples/certora/spec/general.spec | 10 +++++----- 4 files changed, 20 insertions(+), 9 deletions(-) create mode 100644 CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf b/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf index b63c38e7..623f9918 100644 --- a/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf +++ b/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf @@ -1,9 +1,9 @@ { "files": [ - "contracts/ERC20.sol:ERC20" + "contracts/ERC20.sol:ERC20", + "certora/helpersContracts/ERC20helper.sol:ERC20Helper" ], "verify": "ERC20:certora/spec/general.spec", "solc": "solc8.17", - "solc_args": [], "msg": "genral Rules on ERC20 contract" } \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf b/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf index 2f556d4f..2cf287c5 100644 --- a/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf +++ b/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf @@ -1,9 +1,10 @@ { "files": [ - "contracts/Vault.sol:Vault" + "contracts/Vault.sol:Vault", + "contracts/ERC20.sol:ERC20", + "certora/helpersContracts/ERC20helper.sol:ERC20Helper" ], "verify": "Vault:certora/spec/general.spec", "solc": "solc8.17", - "solc_args": [], "msg": "genral Rules on Vault contract" } \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol b/CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol new file mode 100644 index 00000000..a79db067 --- /dev/null +++ b/CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; +import "../../contracts/IERC20.sol"; + +contract ERC20Helper { + + function tokenBalanceOf(address token, address user) public returns (uint256) { + return IERC20(token).balanceOf(user); + } +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/spec/general.spec b/CVLByExamples/GeneralExamples/certora/spec/general.spec index 0a989e26..5e77f26c 100644 --- a/CVLByExamples/GeneralExamples/certora/spec/general.spec +++ b/CVLByExamples/GeneralExamples/certora/spec/general.spec @@ -1,4 +1,4 @@ -using DummyERC20A as erc20; +using ERC20Helper as erc20helper; methods { function _.name() external => DISPATCHER(true); @@ -11,7 +11,7 @@ methods { function _.transfer(address,uint256) external => DISPATCHER(true); function _.transferFrom(address,address,uint256) external => DISPATCHER(true); - function erc20.balanceOf(address) external returns (uint256) envfree; + function erc20helper.tokenBalanceOf(address, address) external returns (uint256) envfree; } /* @@ -108,14 +108,14 @@ rule decreaseInSystemEth(method f) { rule decreaseInERC20(method f) { - - uint256 before = erc20.balanceOf(currentContract); + address token; + uint256 before = erc20helper.tokenBalanceOf(token, currentContract); env e; calldataarg arg; f(e, arg); - uint256 after = erc20.balanceOf(currentContract); + uint256 after = erc20helper.tokenBalanceOf(token, currentContract); assert after >= before || false ; /* fill in cases eth can decrease */ From 73846754343240f4fdee6e8ad9d1ef945aaaae5b Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Wed, 23 Aug 2023 18:11:02 +0300 Subject: [PATCH 3/4] general spec --- .../certora/conf/runReentrancy.conf | 18 ++ .../certora/conf/generalRules_VAULT.conf | 10 - .../certora/conf/generalRules_ERC20.conf | 0 .../certora/conf/generalRules_VAULT.conf | 11 + GenericRules/certora/conf/test.conf | 9 + .../certora/helpersContracts/ERC20Helper.sol | 0 .../certora/spec/erc20Summarization.spec | 68 ++++++ .../certora/spec/erc20Summarization2.spec | 68 ++++++ .../certora/spec/general.spec | 0 GenericRules/certora/spec/generalERC20.spec | 130 ++++++++++ .../contracts/ERC20.sol | 0 GenericRules/contracts/ERC20Mint.sol | 116 +++++++++ GenericRules/contracts/ERC4626.sol | 179 ++++++++++++++ .../contracts/IERC20.sol | 0 .../contracts/IERC20Metadata.sol | 0 .../contracts/Vault.sol | 0 .../contracts/libs/FixedPointMathLib.sol | 222 ++++++++++++++++++ .../contracts/libs/SafeTransferLib.sol | 124 ++++++++++ 18 files changed, 945 insertions(+), 10 deletions(-) create mode 100644 CVLByExample/ConstantProductPool/certora/conf/runReentrancy.conf delete mode 100644 CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf rename {CVLByExamples/GeneralExamples => GenericRules}/certora/conf/generalRules_ERC20.conf (100%) create mode 100644 GenericRules/certora/conf/generalRules_VAULT.conf create mode 100644 GenericRules/certora/conf/test.conf rename {CVLByExamples/GeneralExamples => GenericRules}/certora/helpersContracts/ERC20Helper.sol (100%) create mode 100644 GenericRules/certora/spec/erc20Summarization.spec create mode 100644 GenericRules/certora/spec/erc20Summarization2.spec rename {CVLByExamples/GeneralExamples => GenericRules}/certora/spec/general.spec (100%) create mode 100644 GenericRules/certora/spec/generalERC20.spec rename {CVLByExamples/GeneralExamples => GenericRules}/contracts/ERC20.sol (100%) create mode 100644 GenericRules/contracts/ERC20Mint.sol create mode 100644 GenericRules/contracts/ERC4626.sol rename {CVLByExamples/GeneralExamples => GenericRules}/contracts/IERC20.sol (100%) rename {CVLByExamples/GeneralExamples => GenericRules}/contracts/IERC20Metadata.sol (100%) rename {CVLByExamples/GeneralExamples => GenericRules}/contracts/Vault.sol (100%) create mode 100644 GenericRules/contracts/libs/FixedPointMathLib.sol create mode 100644 GenericRules/contracts/libs/SafeTransferLib.sol diff --git a/CVLByExample/ConstantProductPool/certora/conf/runReentrancy.conf b/CVLByExample/ConstantProductPool/certora/conf/runReentrancy.conf new file mode 100644 index 00000000..7f22b42a --- /dev/null +++ b/CVLByExample/ConstantProductPool/certora/conf/runReentrancy.conf @@ -0,0 +1,18 @@ + +{ + // files that are part of the scene (everything the Certora Prover can reason about) + "files": [ + "contracts/correct/ConstantProductPoolFixed.sol:ConstantProductPool", + "contracts/DummyERC20A.sol", + "contracts/DummyERC20B.sol" + ], + // the main contract under test and the spec file + "verify": "ConstantProductPool:../Reentrancy/certora/spec/noGuardSafety.spec", + // After unrolling loops, assume the loop halt conditions hold : https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops + "optimistic_loop": true, + // Makes the request to the prover but does not wait for verifications results + "send_only": true, + // msg to recognize this run (presented in your list of jobs under prover.cerotra.com) + "msg": "CVLExmaple: ConstantProductPool fixed version" +} +// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --send_only --msg "CVLExmaple: ConstantProductPool fixed version"` \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf b/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf deleted file mode 100644 index 2cf287c5..00000000 --- a/CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf +++ /dev/null @@ -1,10 +0,0 @@ -{ - "files": [ - "contracts/Vault.sol:Vault", - "contracts/ERC20.sol:ERC20", - "certora/helpersContracts/ERC20helper.sol:ERC20Helper" - ], - "verify": "Vault:certora/spec/general.spec", - "solc": "solc8.17", - "msg": "genral Rules on Vault contract" -} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf b/GenericRules/certora/conf/generalRules_ERC20.conf similarity index 100% rename from CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf rename to GenericRules/certora/conf/generalRules_ERC20.conf diff --git a/GenericRules/certora/conf/generalRules_VAULT.conf b/GenericRules/certora/conf/generalRules_VAULT.conf new file mode 100644 index 00000000..b98baefe --- /dev/null +++ b/GenericRules/certora/conf/generalRules_VAULT.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "contracts/Vault.sol:Vault", + /// no need "contracts/ERC20.sol:ERC20", + "certora/helpersContracts/ERC20helper.sol:ERC20Helper" + ], + "verify": "Vault:certora/spec/generalERC20.spec", + "solc": "solc8.17", + "prover_version": "jtoman/deleting-summaries", + "msg": "genral Rules on Vault contract with erc20 summ" +} \ No newline at end of file diff --git a/GenericRules/certora/conf/test.conf b/GenericRules/certora/conf/test.conf new file mode 100644 index 00000000..20ad4b33 --- /dev/null +++ b/GenericRules/certora/conf/test.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "contracts/ERC4626.sol", + "certora/helpersContracts/ERC20Helper.sol" + ], + "process": "emv", + "prover_version": "naftali/fix_calledContract_and_solidy_calls_in_summary", + "verify": "ERC4626:certora/spec/generalERC20.spec" +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol b/GenericRules/certora/helpersContracts/ERC20Helper.sol similarity index 100% rename from CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol rename to GenericRules/certora/helpersContracts/ERC20Helper.sol diff --git a/GenericRules/certora/spec/erc20Summarization.spec b/GenericRules/certora/spec/erc20Summarization.spec new file mode 100644 index 00000000..ee84beb5 --- /dev/null +++ b/GenericRules/certora/spec/erc20Summarization.spec @@ -0,0 +1,68 @@ +methods { + // function _.name() external => NONDET DELETE(true); + // function _.symbol() external => NONDET DELETE(true); + function _.decimals() external => NONDET; + function _.totalSupply() external => erc20_totalSupply[calledContract] expect uint256 ; + function _.balanceOf(address u) external => erc20_balances[calledContract][u] expect uint256; + function _.allowance(address,address) external => NONDET; //TODO + function _.approve(address,uint256) external => NONDET; //TODO + function _.transfer(address to, uint256 amount) external with (env e) => + erc20_transfer(calledContract, e, to, amount) expect bool; + function _.transferFrom(address from, address to, uint256 amount) external with (env e) => + erc20_transferFrom(calledContract, e, from, to, amount) expect bool; +} +/* +methods { + function transfer(address to, uint256 amount) external returns (bool); +} +*/ +function erc20_transfer(address token, env e, address to, uint256 amount) returns bool { + /* if token == currentContract { + return transfer(e, to, amount); + } + else*/ + if (erc20_balances[token][e.msg.sender] < amount) + return false; + else { + erc20_balances[token][e.msg.sender] = assert_uint256(erc20_balances[token][e.msg.sender] - amount); + erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount); + return true; + } + +} + +function erc20_transferFrom(address token, env e, address from, address to, uint256 amount) returns bool { + /* if token == currentContract { + return transferFrom(e, from, to, amount); + } + //todo allowance... + else*/ + if (erc20_balances[token][from] < amount) + return false; + else { + erc20_balances[token][from] = assert_uint256(erc20_balances[token][from] - amount); + erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount); + return true; + } + +} + +// tracking totalSupply for each erc20 address +ghost mapping(address => uint256) erc20_totalSupply; + +// tracking balance for each erc20 address, a mapping for users to +ghost mapping(address => mapping(address => uint256)) erc20_balances; + +// tracking sum balance for each erc20 address, a mapping for users to +ghost mapping(address => uint256) erc20_sum_balances; + + +// @title invariants to use as needed +invariant sumBalancesIsTotalSupply() + forall address t. erc20_sum_balances[t]==erc20_totalSupply[t]; + + +invariant sumBalancesIsTotalSupply() + forall address t. forall address u. erc20_balances[t][u]<=erc20_totalSupply[t]; + + diff --git a/GenericRules/certora/spec/erc20Summarization2.spec b/GenericRules/certora/spec/erc20Summarization2.spec new file mode 100644 index 00000000..a574a616 --- /dev/null +++ b/GenericRules/certora/spec/erc20Summarization2.spec @@ -0,0 +1,68 @@ +methods { + // function _.name() external => NONDET DELETE(true); + // function _.symbol() external => NONDET DELETE(true); + function _.decimals() external => NONDET; + function _.totalSupply() external => erc20_totalSupply[calledContract] expect uint256 ; + function _.balanceOf(address u) external => erc20_balances[calledContract][u] expect uint256; + function _.allowance(address,address) external => NONDET; //TODO + function _.approve(address,uint256) external => NONDET; //TODO + function _.transfer(address to, uint256 amount) external with (env e) => + erc20_transfer(calledContract, e, to, amount) expect bool; + function _.transferFrom(address from, address to, uint256 amount) external with (env e) => + erc20_transferFrom(calledContract, e, from, to, amount) expect bool; +} + +methods { + function transfer(address to, uint256 amount) external returns (bool); +} + +function erc20_transfer(address token, env e, address to, uint256 amount) returns bool { + if token == currentContract { + return transfer(e, to, amount); + } + else + if (erc20_balances[token][e.msg.sender] < amount) + return false; + else { + erc20_balances[token][e.msg.sender] = assert_uint256(erc20_balances[token][e.msg.sender] - amount); + erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount); + return true; + } + +} + +function erc20_transferFrom(address token, env e, address from, address to, uint256 amount) returns bool { + if token == currentContract { + return transferFrom(e, from, to, amount); + } + //todo allowance... + else + if (erc20_balances[token][from] < amount) + return false; + else { + erc20_balances[token][from] = assert_uint256(erc20_balances[token][from] - amount); + erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount); + return true; + } + +} + +// tracking totalSupply for each erc20 address +ghost mapping(address => uint256) erc20_totalSupply; + +// tracking balance for each erc20 address, a mapping for users to +ghost mapping(address => mapping(address => uint256)) erc20_balances; + +// tracking sum balance for each erc20 address, a mapping for users to +ghost mapping(address => uint256) erc20_sum_balances; + + +// @title invariants to use as needed +invariant sumBalancesIsTotalSupply() + forall address t. erc20_sum_balances[t]==erc20_totalSupply[t]; + + +invariant singleBalance() + forall address t. forall address u. erc20_balances[t][u]<=erc20_totalSupply[t]; + + diff --git a/CVLByExamples/GeneralExamples/certora/spec/general.spec b/GenericRules/certora/spec/general.spec similarity index 100% rename from CVLByExamples/GeneralExamples/certora/spec/general.spec rename to GenericRules/certora/spec/general.spec diff --git a/GenericRules/certora/spec/generalERC20.spec b/GenericRules/certora/spec/generalERC20.spec new file mode 100644 index 00000000..2d055008 --- /dev/null +++ b/GenericRules/certora/spec/generalERC20.spec @@ -0,0 +1,130 @@ +import "erc20Summarization2.spec"; +using ERC20Helper as erc20helper; + + +methods { + + function erc20helper.tokenBalanceOf(address, address) external returns (uint256) envfree; +} + +/* + Property: Find and show a path for each method. +*/ +rule reachability(method f) +{ + env e; + calldataarg args; + f(e,args); + satisfy true; +} + +/* + Property: Define and check functions that should never revert + Notice: use f.selector to state which functions should not revert,e.g.f.selector == sig:balanceOf(address).selector +*/ +definition nonReveritngFunction(method f ) returns bool = true; + +rule noRevert(method f) filtered {f -> nonReveritngFunction(f) } +{ + env e; + calldataarg arg; + //consider auto filtering for non-payable functions + require e.msg.value == 0; + f@withrevert(e, arg); + assert !lastReverted, "method should not revert"; +} + + +/* + Property: Checks if a function can be frontrun + Notice: Can be enhanced to check more than one function as rules can be double-parameteric +*/ +rule simpleFrontRunning(method f, method g) filtered { f-> !f.isView, g-> !g.isView } +{ + env e1; + calldataarg arg; + + storage initialStorage = lastStorage; + f(e1, arg); + + + env e2; + calldataarg arg2; + require e2.msg.sender != e1.msg.sender; + g(e2, arg2) at initialStorage; + + f@withrevert(e1, arg); + bool succeeded = !lastReverted; + + assert succeeded, "should be called also if frontrunned"; +} + + +/** + @title - This rule find which functions are privileged. + @notice A function is privileged if there is only one address that can call it. + @dev The rules finds this by finding which functions can be called by two different users. +*/ + +rule privilegedOperation(method f, address privileged) +{ + env e1; + calldataarg arg; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + f@withrevert(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "function is privileged"; +} + + +rule decreaseInSystemEth(method f) { + + uint256 before = nativeBalances[currentContract]; + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = nativeBalances[currentContract]; + + assert after >= before || false ; /* fill in cases where eth can decrease */ +} + + +rule decreaseInERC20(method f) { + address token; + uint256 before = erc20helper.tokenBalanceOf(token, currentContract); + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = erc20helper.tokenBalanceOf(token, currentContract); + + assert after >= before || false ; /* fill in cases eth can decrease */ + +} + + +rule changeInThis(method f) { + address token; + uint256 before = erc20helper.tokenBalanceOf(token, currentContract); + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = erc20helper.tokenBalanceOf(token, currentContract); + + satisfy token == currentContract && after != before ; + +} \ No newline at end of file diff --git a/CVLByExamples/GeneralExamples/contracts/ERC20.sol b/GenericRules/contracts/ERC20.sol similarity index 100% rename from CVLByExamples/GeneralExamples/contracts/ERC20.sol rename to GenericRules/contracts/ERC20.sol diff --git a/GenericRules/contracts/ERC20Mint.sol b/GenericRules/contracts/ERC20Mint.sol new file mode 100644 index 00000000..99217dd7 --- /dev/null +++ b/GenericRules/contracts/ERC20Mint.sol @@ -0,0 +1,116 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +/// @notice Modern and gas efficient ERC20 implementation. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol) +/// @author Modified from Uniswap +/// (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol) +/// @dev Do not manually set balances without updating totalSupply, as the sum of all +/// user balances must not exceed it. +contract ERC20 { + // EVENTS + + event Transfer(address indexed from, address indexed to, uint256 amount); + + event Approval(address indexed owner, address indexed spender, uint256 amount); + + // METADATA STORAGE + + string public name; + + string public symbol; + + uint8 public immutable decimals; + + // ERC20 STORAGE + + uint256 public totalSupply; + + mapping(address => uint256) public balanceOf; + + mapping(address => mapping(address => uint256)) public allowance; + + // CONSTRUCTOR + + constructor( + string memory _name, + string memory _symbol, + uint8 _decimals + ) { + name = _name; + symbol = _symbol; + decimals = _decimals; + } + + // ERC20 LOGIC + + function approve(address spender, uint256 amount) public virtual returns (bool) { + allowance[msg.sender][spender] = amount; + + emit Approval(msg.sender, spender, amount); + + return true; + } + + function transfer(address to, uint256 amount) public virtual returns (bool) { + balanceOf[msg.sender] -= amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(msg.sender, to, amount); + + return true; + } + + function transferFrom( + address from, + address to, + uint256 amount + ) public virtual returns (bool) { + uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount; + + balanceOf[from] -= amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(from, to, amount); + + return true; + } + + // INTERNAL MINT/BURN LOGIC + + function _mint(address to, uint256 amount) internal virtual { + totalSupply += amount; + + // Cannot overflow because the sum of all user + // balances can't exceed the max uint256 value. + unchecked { + balanceOf[to] += amount; + } + + emit Transfer(address(0), to, amount); + } + + function _burn(address from, uint256 amount) internal virtual { + balanceOf[from] -= amount; + + // Cannot underflow because a user's balance + // will never be larger than the total supply. + unchecked { + totalSupply -= amount; + } + + emit Transfer(from, address(0), amount); + } +} diff --git a/GenericRules/contracts/ERC4626.sol b/GenericRules/contracts/ERC4626.sol new file mode 100644 index 00000000..ce5440d3 --- /dev/null +++ b/GenericRules/contracts/ERC4626.sol @@ -0,0 +1,179 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import {ERC20} from "./ERC20Mint.sol"; +import {SafeTransferLib} from "./libs/SafeTransferLib.sol"; +import {FixedPointMathLib} from "./libs/FixedPointMathLib.sol"; + +/// @notice Minimal ERC4626 tokenized Vault implementation. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/mixins/ERC4626.sol) +/// @dev This contract implements the `totalAssets()` function by simply +/// returning the contract's balance. +/// @notice This contract is open to an attack where the first depositor +/// can steal all the other users' funds. +/// This can be done by front-running the deposit transaction and +/// transferring enough tokens to zero the shares calculation. +contract ERC4626 is ERC20 { + using SafeTransferLib for ERC20; + using FixedPointMathLib for uint256; + + // EVENTS + + event Deposit(address indexed caller, address indexed owner, uint256 assets, uint256 shares); + + event Withdraw( + address indexed caller, + address indexed receiver, + address indexed owner, + uint256 assets, + uint256 shares + ); + + // IMMUTABLES + + ERC20 public immutable asset; + + constructor( + ERC20 _asset, + string memory _name, + string memory _symbol + ) ERC20(_name, _symbol, _asset.decimals()) { + asset = _asset; + } + + // DEPOSIT/WITHDRAWAL LOGIC + + function deposit(uint256 assets, address receiver) public virtual returns (uint256 shares) { + // Check for rounding error since we round down in previewDeposit. + require((shares = previewDeposit(assets)) != 0, "ZERO_SHARES"); + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function mint(uint256 shares, address receiver) public virtual returns (uint256 assets) { + assets = previewMint(shares); // No need to check for rounding error, previewMint rounds up. + + // Need to transfer before minting or ERC777s could reenter. + asset.safeTransferFrom(msg.sender, address(this), assets); + + _mint(receiver, shares); + + emit Deposit(msg.sender, receiver, assets, shares); + + afterDeposit(assets, shares); + } + + function withdraw( + uint256 assets, + address receiver, + address owner + ) public virtual returns (uint256 shares) { + shares = previewWithdraw(assets); // No need to check for rounding error, previewWithdraw rounds up. + + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + function redeem( + uint256 shares, + address receiver, + address owner + ) public virtual returns (uint256 assets) { + if (msg.sender != owner) { + uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals. + + if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares; + } + + // Check for rounding error since we round down in previewRedeem. + require((assets = previewRedeem(shares)) != 0, "ZERO_ASSETS"); + + beforeWithdraw(assets, shares); + + _burn(owner, shares); + + emit Withdraw(msg.sender, receiver, owner, assets, shares); + + asset.safeTransfer(receiver, assets); + } + + // ACCOUNTING LOGIC + + function totalAssets() public view returns (uint256) { + return asset.balanceOf(address(this)); + } + + function convertToShares(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivDown(supply, totalAssets()); + } + + function convertToAssets(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivDown(totalAssets(), supply); + } + + function previewDeposit(uint256 assets) public view virtual returns (uint256) { + return convertToShares(assets); + } + + function previewMint(uint256 shares) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? shares : shares.mulDivUp(totalAssets(), supply); + } + + function previewWithdraw(uint256 assets) public view virtual returns (uint256) { + uint256 supply = totalSupply; // Saves an extra SLOAD if totalSupply is non-zero. + + return supply == 0 ? assets : assets.mulDivUp(supply, totalAssets()); + } + + function previewRedeem(uint256 shares) public view virtual returns (uint256) { + return convertToAssets(shares); + } + + // DEPOSIT/WITHDRAWAL LIMIT LOGIC + + function maxDeposit(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxMint(address) public view virtual returns (uint256) { + return type(uint256).max; + } + + function maxWithdraw(address owner) public view virtual returns (uint256) { + return convertToAssets(balanceOf[owner]); + } + + function maxRedeem(address owner) public view virtual returns (uint256) { + return balanceOf[owner]; + } + + // INTERNAL HOOKS LOGIC + + function beforeWithdraw(uint256 assets, uint256 shares) internal virtual {} + + function afterDeposit(uint256 assets, uint256 shares) internal virtual {} +} diff --git a/CVLByExamples/GeneralExamples/contracts/IERC20.sol b/GenericRules/contracts/IERC20.sol similarity index 100% rename from CVLByExamples/GeneralExamples/contracts/IERC20.sol rename to GenericRules/contracts/IERC20.sol diff --git a/CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol b/GenericRules/contracts/IERC20Metadata.sol similarity index 100% rename from CVLByExamples/GeneralExamples/contracts/IERC20Metadata.sol rename to GenericRules/contracts/IERC20Metadata.sol diff --git a/CVLByExamples/GeneralExamples/contracts/Vault.sol b/GenericRules/contracts/Vault.sol similarity index 100% rename from CVLByExamples/GeneralExamples/contracts/Vault.sol rename to GenericRules/contracts/Vault.sol diff --git a/GenericRules/contracts/libs/FixedPointMathLib.sol b/GenericRules/contracts/libs/FixedPointMathLib.sol new file mode 100644 index 00000000..33fbaf87 --- /dev/null +++ b/GenericRules/contracts/libs/FixedPointMathLib.sol @@ -0,0 +1,222 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +/// @notice Arithmetic library with operations for fixed-point numbers. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/FixedPointMathLib.sol) +/// @author Inspired by USM (https://github.com/usmfum/USM/blob/master/contracts/WadMath.sol) +library FixedPointMathLib { + /*////////////////////////////////////////////////////////////// + SIMPLIFIED FIXED POINT OPERATIONS + //////////////////////////////////////////////////////////////*/ + + uint256 internal constant WAD = 1e18; // The scalar of ETH and most ERC20s. + + function mulWadDown(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivDown(x, y, WAD); // Equivalent to (x * y) / WAD rounded down. + } + + function mulWadUp(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivUp(x, y, WAD); // Equivalent to (x * y) / WAD rounded up. + } + + function divWadDown(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivDown(x, WAD, y); // Equivalent to (x * WAD) / y rounded down. + } + + function divWadUp(uint256 x, uint256 y) internal pure returns (uint256) { + return mulDivUp(x, WAD, y); // Equivalent to (x * WAD) / y rounded up. + } + + /*////////////////////////////////////////////////////////////// + LOW LEVEL FIXED POINT OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function mulDivDown( + uint256 x, + uint256 y, + uint256 denominator + ) internal pure returns (uint256 z) { + assembly { + // Store x * y in z for now. + z := mul(x, y) + + // Equivalent to require(denominator != 0 && (x == 0 || (x * y) / x == y)) + if iszero(and(iszero(iszero(denominator)), or(iszero(x), eq(div(z, x), y)))) { + revert(0, 0) + } + + // Divide z by the denominator. + z := div(z, denominator) + } + } + + function mulDivUp( + uint256 x, + uint256 y, + uint256 denominator + ) internal pure returns (uint256 z) { + assembly { + // Store x * y in z for now. + z := mul(x, y) + + // Equivalent to require(denominator != 0 && (x == 0 || (x * y) / x == y)) + if iszero(and(iszero(iszero(denominator)), or(iszero(x), eq(div(z, x), y)))) { + revert(0, 0) + } + + // First, divide z - 1 by the denominator and add 1. + // We allow z - 1 to underflow if z is 0, because we multiply the + // end result by 0 if z is zero, ensuring we return 0 if z is zero. + z := mul(iszero(iszero(z)), add(div(sub(z, 1), denominator), 1)) + } + } + + function rpow( + uint256 x, + uint256 n, + uint256 scalar + ) internal pure returns (uint256 z) { + assembly { + switch x + case 0 { + switch n + case 0 { + // 0 ** 0 = 1 + z := scalar + } + default { + // 0 ** n = 0 + z := 0 + } + } + default { + switch mod(n, 2) + case 0 { + // If n is even, store scalar in z for now. + z := scalar + } + default { + // If n is odd, store x in z for now. + z := x + } + + // Shifting right by 1 is like dividing by 2. + let half := shr(1, scalar) + + for { + // Shift n right by 1 before looping to halve it. + n := shr(1, n) + } n { + // Shift n right by 1 each iteration to halve it. + n := shr(1, n) + } { + // Revert immediately if x ** 2 would overflow. + // Equivalent to iszero(eq(div(xx, x), x)) here. + if shr(128, x) { + revert(0, 0) + } + + // Store x squared. + let xx := mul(x, x) + + // Round to the nearest number. + let xxRound := add(xx, half) + + // Revert if xx + half overflowed. + if lt(xxRound, xx) { + revert(0, 0) + } + + // Set x to scaled xxRound. + x := div(xxRound, scalar) + + // If n is even: + if mod(n, 2) { + // Compute z * x. + let zx := mul(z, x) + + // If z * x overflowed: + if iszero(eq(div(zx, x), z)) { + // Revert if x is non-zero. + if iszero(iszero(x)) { + revert(0, 0) + } + } + + // Round to the nearest number. + let zxRound := add(zx, half) + + // Revert if zx + half overflowed. + if lt(zxRound, zx) { + revert(0, 0) + } + + // Return properly scaled zxRound. + z := div(zxRound, scalar) + } + } + } + } + } + + /*////////////////////////////////////////////////////////////// + GENERAL NUMBER UTILITIES + //////////////////////////////////////////////////////////////*/ + + function sqrt(uint256 x) internal pure returns (uint256 z) { + assembly { + // Start off with z at 1. + z := 1 + + // Used below to help find a nearby power of 2. + let y := x + + // Find the lowest power of 2 that is at least sqrt(x). + if iszero(lt(y, 0x100000000000000000000000000000000)) { + y := shr(128, y) // Like dividing by 2 ** 128. + z := shl(64, z) // Like multiplying by 2 ** 64. + } + if iszero(lt(y, 0x10000000000000000)) { + y := shr(64, y) // Like dividing by 2 ** 64. + z := shl(32, z) // Like multiplying by 2 ** 32. + } + if iszero(lt(y, 0x100000000)) { + y := shr(32, y) // Like dividing by 2 ** 32. + z := shl(16, z) // Like multiplying by 2 ** 16. + } + if iszero(lt(y, 0x10000)) { + y := shr(16, y) // Like dividing by 2 ** 16. + z := shl(8, z) // Like multiplying by 2 ** 8. + } + if iszero(lt(y, 0x100)) { + y := shr(8, y) // Like dividing by 2 ** 8. + z := shl(4, z) // Like multiplying by 2 ** 4. + } + if iszero(lt(y, 0x10)) { + y := shr(4, y) // Like dividing by 2 ** 4. + z := shl(2, z) // Like multiplying by 2 ** 2. + } + if iszero(lt(y, 0x8)) { + // Equivalent to 2 ** z. + z := shl(1, z) + } + + // Shifting right by 1 is like dividing by 2. + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + + // Compute a rounded down version of z. + let zRoundDown := div(x, z) + + // If zRoundDown is smaller, use it. + if lt(zRoundDown, z) { + z := zRoundDown + } + } + } +} diff --git a/GenericRules/contracts/libs/SafeTransferLib.sol b/GenericRules/contracts/libs/SafeTransferLib.sol new file mode 100644 index 00000000..7cae112d --- /dev/null +++ b/GenericRules/contracts/libs/SafeTransferLib.sol @@ -0,0 +1,124 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import {ERC20} from "../ERC20Mint.sol"; + +/// @notice Safe ETH and ERC20 transfer library that gracefully handles missing return values. +/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/utils/SafeTransferLib.sol) +/// @dev Use with caution! Some functions in this library knowingly create dirty bits at the destination of the free memory pointer. +/// @dev Note that none of the functions in this library check that a token has code at all! That responsibility is delegated to the caller. +library SafeTransferLib { + /*////////////////////////////////////////////////////////////// + ETH OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function safeTransferETH(address to, uint256 amount) internal { + bool success; + + assembly { + // Transfer the ETH and store if it succeeded or not. + success := call(gas(), to, amount, 0, 0, 0, 0) + } + + require(success, "ETH_TRANSFER_FAILED"); + } + + /*////////////////////////////////////////////////////////////// + ERC20 OPERATIONS + //////////////////////////////////////////////////////////////*/ + + function safeTransferFrom( + ERC20 token, + address from, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0x23b872dd00000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), from) // Append the "from" argument. + mstore(add(freeMemoryPointer, 36), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 68), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 100 because the length of our calldata totals up like so: 4 + 32 * 3. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 100, 0, 32) + ) + } + + require(success, "TRANSFER_FROM_FAILED"); + } + + function safeTransfer( + ERC20 token, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0xa9059cbb00000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 36), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 68 because the length of our calldata totals up like so: 4 + 32 * 2. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 68, 0, 32) + ) + } + + require(success, "TRANSFER_FAILED"); + } + + function safeApprove( + ERC20 token, + address to, + uint256 amount + ) internal { + bool success; + + assembly { + // Get a pointer to some free memory. + let freeMemoryPointer := mload(0x40) + + // Write the abi-encoded calldata into memory, beginning with the function selector. + mstore(freeMemoryPointer, 0x095ea7b300000000000000000000000000000000000000000000000000000000) + mstore(add(freeMemoryPointer, 4), to) // Append the "to" argument. + mstore(add(freeMemoryPointer, 36), amount) // Append the "amount" argument. + + success := and( + // Set success to whether the call reverted, if not we check it either + // returned exactly 1 (can't just be non-zero data), or had no return data. + or(and(eq(mload(0), 1), gt(returndatasize(), 31)), iszero(returndatasize())), + // We use 68 because the length of our calldata totals up like so: 4 + 32 * 2. + // We use 0 and 32 to copy up to 32 bytes of return data into the scratch space. + // Counterintuitively, this call must be positioned second to the or() call in the + // surrounding and() call or else returndatasize() will be zero during the computation. + call(gas(), token, 0, freeMemoryPointer, 68, 0, 32) + ) + } + + require(success, "APPROVE_FAILED"); + } +} From 021e3fc3241175229f4dcd06ed6c1367aed0149e Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Mon, 15 Jan 2024 16:29:11 +0200 Subject: [PATCH 4/4] Add self call example --- .../certora/conf/generalRules_Pool.conf | 13 +++ GenericRules/certora/spec/generalPool.spec | 38 +++++++++ GenericRules/contracts/Asset.sol | 4 + GenericRules/contracts/Pool.sol | 85 +++++++++++++++++++ 4 files changed, 140 insertions(+) create mode 100644 GenericRules/certora/conf/generalRules_Pool.conf create mode 100644 GenericRules/certora/spec/generalPool.spec create mode 100644 GenericRules/contracts/Asset.sol create mode 100644 GenericRules/contracts/Pool.sol diff --git a/GenericRules/certora/conf/generalRules_Pool.conf b/GenericRules/certora/conf/generalRules_Pool.conf new file mode 100644 index 00000000..0ae7c612 --- /dev/null +++ b/GenericRules/certora/conf/generalRules_Pool.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "contracts/Pool.sol", + "contracts/Asset.sol", + ], + "verify": "Pool:../spec/generalPool.spec", + "msg": "Pool with linking", + "link": [ + "Pool:asset=Asset" + ], + "parametric_contracts": ["Pool"], + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/GenericRules/certora/spec/generalPool.spec b/GenericRules/certora/spec/generalPool.spec new file mode 100644 index 00000000..cc449ab0 --- /dev/null +++ b/GenericRules/certora/spec/generalPool.spec @@ -0,0 +1,38 @@ +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Reentrancy ghost and hook │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition lock_on() returns bool = ghostReentrancyStatus == 2; +definition poll_functions(method f) returns bool = f.selector == sig:withdraw(uint256).selector || + f.selector == sig:deposit(uint256).selector || + f.selector == sig:flashLoan(address, uint256).selector; + + +ghost uint256 ghostReentrancyStatus; +ghost bool lock_status_on_call; + +hook Sload uint256 status currentContract._status STORAGE { + require ghostReentrancyStatus == status; +} + +hook Sstore currentContract._status uint256 status STORAGE { + ghostReentrancyStatus = status; +} + +// we are hooking here on "CALL" opcodes in order to simulate reentrancy to a non-view function and check that the function reverts +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + lock_status_on_call = lock_on(); +} + +// this rule prove the assumption e.msg.sender != currentContract; +rule reentrancyCheck(env e, method f, calldataarg args) filtered{f -> poll_functions(f)}{ + bool lockBefore = lock_on(); + + f(e, args); + + bool lockAfter = lock_on(); + + assert !lockBefore && !lockAfter; + assert lock_status_on_call; +} \ No newline at end of file diff --git a/GenericRules/contracts/Asset.sol b/GenericRules/contracts/Asset.sol new file mode 100644 index 00000000..bce781d9 --- /dev/null +++ b/GenericRules/contracts/Asset.sol @@ -0,0 +1,4 @@ +pragma solidity >=0.8.0; +import {ERC20} from './ERC20.sol'; +contract Asset is ERC20{ +} \ No newline at end of file diff --git a/GenericRules/contracts/Pool.sol b/GenericRules/contracts/Pool.sol new file mode 100644 index 00000000..cfce0464 --- /dev/null +++ b/GenericRules/contracts/Pool.sol @@ -0,0 +1,85 @@ +import {IFlashLoanReceiver} from './IFlashLoanReceiver.sol'; +import {ERC20} from './ERC20.sol'; +import {IERC20} from './IERC20.sol'; +pragma solidity >=0.8.0; + + +contract Pool is ERC20 { + + uint256 private constant _NOT_ENTERED = 1; + uint256 private constant _ENTERED = 2; + + uint256 private _status; + modifier nonReentrant() { + // On the first call to nonReentrant, _notEntered will be true + require(_status != _ENTERED, "ReentrancyGuard: reentrant call"); + + // Any calls to nonReentrant after this point will fail + _status = _ENTERED; + + _; + + // By storing the original value once again, a refund is triggered (see + // https://eips.ethereum.org/EIPS/eip-2200) + _status = _NOT_ENTERED; + } + + IERC20 public asset; + uint256 private constant feePrecision = 10000; + //feeRate is up to 1%, so less than 100 as it is divided by feePrecision + uint256 public feeRate; + uint256 public depositedAmount = 0; + + function sharesToAmount(uint256 shares) public view virtual returns (uint256) { + return shares * depositedAmount / totalSupply(); + } + + + function amountToShares(uint256 amount) public view virtual returns (uint256) { + return amount * totalSupply() / depositedAmount; + } + + function deposit(uint256 amount) public nonReentrant() returns(uint256 shares) { + if (totalSupply()==0 || depositedAmount == 0){ + shares = amount; + } + else{ + shares = amountToShares(amount); + require (shares != 0); + } + asset.transferFrom(msg.sender,address(this),amount); + depositedAmount = depositedAmount + amount; + _mint(msg.sender,shares); + } + + + function withdraw(uint256 shares) public nonReentrant() returns (uint256 amountOut) { + uint256 poolBalance = asset.balanceOf(address(this)); + require (poolBalance != 0); + amountOut = sharesToAmount(shares); + require (amountOut != 0); + _burn(msg.sender,shares); + asset.transferFrom(address(this),msg.sender,amountOut); + depositedAmount = depositedAmount - amountOut; + } + + + function flashLoan(address receiverAddress, uint256 amount) nonReentrant() public { + uint256 totalPremium = calcPremium(amount); + require (totalPremium != 0); + uint256 amountPlusPremium = amount + totalPremium; + asset.transferFrom(address(this),msg.sender,amount); + depositedAmount = depositedAmount - amount; + require(IFlashLoanReceiver(receiverAddress).executeOperation(amount,totalPremium,msg.sender),'P_INVALID_FLASH_LOAN_EXECUTOR_RETURN'); + asset.transferFrom(msg.sender,address(this),amountPlusPremium); + depositedAmount = depositedAmount + amountPlusPremium; + } + + function calcPremium(uint256 amount) public view returns (uint256){ + return ((amount*feeRate)/feePrecision); + } + + function assetBalance() public view returns (uint256) { + return asset.balanceOf(address(this)); + } +} \ No newline at end of file