diff --git a/.changeset/tender-needles-dance.md b/.changeset/tender-needles-dance.md new file mode 100644 index 00000000000..d75adec9582 --- /dev/null +++ b/.changeset/tender-needles-dance.md @@ -0,0 +1,5 @@ +--- +'openzeppelin-solidity': minor +--- + +`ERC20Wrapper`: self wrapping and deposit by the wrapper itself are now explicitelly forbiden. diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol index cc66358b298..dd0aacae2fa 100644 --- a/certora/harnesses/ERC20PermitHarness.sol +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -2,10 +2,9 @@ pragma solidity ^0.8.0; -import "../patched/token/ERC20/ERC20.sol"; import "../patched/token/ERC20/extensions/ERC20Permit.sol"; -contract ERC20PermitHarness is ERC20, ERC20Permit { +contract ERC20PermitHarness is ERC20Permit { constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} function mint(address account, uint256 amount) external { diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol new file mode 100644 index 00000000000..50a96cc170a --- /dev/null +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/extensions/ERC20Wrapper.sol"; + +contract ERC20WrapperHarness is ERC20Wrapper { + constructor(IERC20 _underlying, string memory _name, string memory _symbol) ERC20(_name, _symbol) ERC20Wrapper(_underlying) {} + + function underlyingTotalSupply() public view returns (uint256) { + return underlying().totalSupply(); + } + + function underlyingBalanceOf(address account) public view returns (uint256) { + return underlying().balanceOf(account); + } + + function underlyingAllowanceToThis(address account) public view returns (uint256) { + return underlying().allowance(account, address(this)); + } + + function recover(address account) public returns (uint256) { + return _recover(account); + } +} diff --git a/certora/run.js b/certora/run.js index 172309e198c..f3234c1a344 100644 --- a/certora/run.js +++ b/certora/run.js @@ -31,7 +31,7 @@ if (request) { } for (const { spec, contract, files, options = [] } of Object.values(specs)) { - limit(runCertora, spec, contract, files, [...options, ...extraOptions]); + limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]); } // Run certora, aggregate the output and print it at the end @@ -50,7 +50,7 @@ async function runCertora(spec, contract, files, options = []) { const urls = data.toString('utf8').match(/https?:\S*/g); for (const url of urls ?? []) { if (url.includes('/jobStatus/')) { - console.error(`[${spec}] ${url}`); + console.error(`[${spec}] ${url.replace('/jobStatus/', '/output/')}`); stream.off('data', logStatusUrl); break; } @@ -108,8 +108,8 @@ function writeEntry(spec, contract, success, url) { spec, contract, success ? ':x:' : ':heavy_check_mark:', - `[link](${url})`, - `[link](${url?.replace('/jobStatus/', '/output/')})`, + url ? `[link](${url})` : 'error', + url ? `[link](${url?.replace('/jobStatus/', '/output/')})` : 'error', ), ); } diff --git a/certora/specs.json b/certora/specs.json index 8e4fe21f4cc..228e85fe4f3 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -29,6 +29,18 @@ ], "options": ["--optimistic_loop"] }, + { + "spec": "ERC20Wrapper", + "contract": "ERC20WrapperHarness", + "files": [ + "certora/harnesses/ERC20PermitHarness.sol", + "certora/harnesses/ERC20WrapperHarness.sol" + ], + "options": [ + "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness", + "--optimistic_loop" + ] + }, { "spec": "Initializable", "contract": "InitializableHarness", diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec new file mode 100644 index 00000000000..c10173766de --- /dev/null +++ b/certora/specs/ERC20Wrapper.spec @@ -0,0 +1,198 @@ +import "helpers.spec" +import "ERC20.spec" + +methods { + underlying() returns(address) envfree + underlyingTotalSupply() returns(uint256) envfree + underlyingBalanceOf(address) returns(uint256) envfree + underlyingAllowanceToThis(address) returns(uint256) envfree + + depositFor(address, uint256) returns(bool) + withdrawTo(address, uint256) returns(bool) + recover(address) returns(uint256) +} + +use invariant totalSupplyIsSumOfBalances + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +function underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool { + return underlyingBalanceOf(a) <= underlyingTotalSupply(); +} + +function sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool { + return a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= underlyingTotalSupply(); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: wrapped token can't be undercollateralized (solvency of the wrapper) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyIsSmallerThanUnderlyingBalance() + totalSupply() <= underlyingBalanceOf(currentContract) && + underlyingBalanceOf(currentContract) <= underlyingTotalSupply() && + underlyingTotalSupply() <= max_uint256 + { + preserved { + requireInvariant totalSupplyIsSumOfBalances; + require underlyingBalancesLowerThanUnderlyingSupply(currentContract); + } + preserved depositFor(address account, uint256 amount) with (env e) { + require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract); + } + } + +invariant noSelfWrap() + currentContract != underlying() + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: depositFor liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule depositFor(env e) { + require nonpayable(e); + + address sender = e.msg.sender; + address receiver; + address other; + uint256 amount; + + // sanity + requireInvariant noSelfWrap; + requireInvariant totalSupplyIsSumOfBalances; + requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; + require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, sender); + + uint256 balanceBefore = balanceOf(receiver); + uint256 supplyBefore = totalSupply(); + uint256 senderUnderlyingBalanceBefore = underlyingBalanceOf(sender); + uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender); + uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract); + uint256 underlyingSupplyBefore = underlyingTotalSupply(); + + uint256 otherBalanceBefore = balanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + + depositFor@withrevert(e, receiver, amount); + bool success = !lastReverted; + + // liveness + assert success <=> ( + sender != currentContract && // invalid sender + sender != 0 && // invalid sender + receiver != 0 && // invalid receiver + amount <= senderUnderlyingBalanceBefore && // deposit doesn't exceed balance + amount <= senderUnderlyingAllowanceBefore // deposit doesn't exceed allowance + ); + + // effects + assert success => ( + balanceOf(receiver) == balanceBefore + amount && + totalSupply() == supplyBefore + amount && + underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore + amount && + underlyingBalanceOf(sender) == senderUnderlyingBalanceBefore - amount + ); + + // no side effect + assert underlyingTotalSupply() == underlyingSupplyBefore; + assert balanceOf(other) != otherBalanceBefore => other == receiver; + assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: withdrawTo liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule withdrawTo(env e) { + require nonpayable(e); + + address sender = e.msg.sender; + address receiver; + address other; + uint256 amount; + + // sanity + requireInvariant noSelfWrap; + requireInvariant totalSupplyIsSumOfBalances; + requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; + require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(currentContract, receiver); + + uint256 balanceBefore = balanceOf(sender); + uint256 supplyBefore = totalSupply(); + uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver); + uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract); + uint256 underlyingSupplyBefore = underlyingTotalSupply(); + + uint256 otherBalanceBefore = balanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + + withdrawTo@withrevert(e, receiver, amount); + bool success = !lastReverted; + + // liveness + assert success <=> ( + sender != 0 && // invalid sender + receiver != 0 && // invalid receiver + amount <= balanceBefore // withdraw doesn't exceed balance + ); + + // effects + assert success => ( + balanceOf(sender) == balanceBefore - amount && + totalSupply() == supplyBefore - amount && + underlyingBalanceOf(currentContract) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && + underlyingBalanceOf(receiver) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) + ); + + // no side effect + assert underlyingTotalSupply() == underlyingSupplyBefore; + assert balanceOf(other) != otherBalanceBefore => other == sender; + assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: recover liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule recover(env e) { + require nonpayable(e); + + address receiver; + address other; + + // sanity + requireInvariant noSelfWrap; + requireInvariant totalSupplyIsSumOfBalances; + requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; + + uint256 value = underlyingBalanceOf(currentContract) - totalSupply(); + uint256 supplyBefore = totalSupply(); + uint256 balanceBefore = balanceOf(receiver); + + uint256 otherBalanceBefore = balanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + + recover@withrevert(e, receiver); + bool success = !lastReverted; + + // liveness + assert success <=> receiver != 0; + + // effect + assert success => ( + balanceOf(receiver) == balanceBefore + value && + totalSupply() == supplyBefore + value && + totalSupply() == underlyingBalanceOf(currentContract) + ); + + // no side effect + assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore; + assert balanceOf(other) != otherBalanceBefore => other == receiver; +} diff --git a/contracts/token/ERC20/extensions/ERC20Wrapper.sol b/contracts/token/ERC20/extensions/ERC20Wrapper.sol index ce515693e7c..bfe782e43a9 100644 --- a/contracts/token/ERC20/extensions/ERC20Wrapper.sol +++ b/contracts/token/ERC20/extensions/ERC20Wrapper.sol @@ -19,6 +19,7 @@ abstract contract ERC20Wrapper is ERC20 { IERC20 private immutable _underlying; constructor(IERC20 underlyingToken) { + require(underlyingToken != this, "ERC20Wrapper: cannot self wrap"); _underlying = underlyingToken; } @@ -44,7 +45,9 @@ abstract contract ERC20Wrapper is ERC20 { * @dev Allow a user to deposit underlying tokens and mint the corresponding number of wrapped tokens. */ function depositFor(address account, uint256 amount) public virtual returns (bool) { - SafeERC20.safeTransferFrom(_underlying, _msgSender(), address(this), amount); + address sender = _msgSender(); + require(sender != address(this), "ERC20Wrapper: wrapper can't deposit"); + SafeERC20.safeTransferFrom(_underlying, sender, address(this), amount); _mint(account, amount); return true; }