diff --git a/PROPERTIES.md b/PROPERTIES.md index c24d8ae..a68f6a0 100644 --- a/PROPERTIES.md +++ b/PROPERTIES.md @@ -42,6 +42,7 @@ This file lists all the currently implemented Echidna property tests for ERC20, | ERC20-BASE-015 | [test_ERC20_setAllowance](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20BasicProperties.sol#L160) | Allowances should be set correctly when `approve` is called. | | ERC20-BASE-016 | [test_ERC20_setAllowanceTwice](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20BasicProperties.sol#L167) | Allowances should be updated correctly when `approve` is called twice. | | ERC20-BASE-017 | [test_ERC20_spendAllowanceAfterTransfer](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20BasicProperties.sol#L178) | After `transferFrom`, allowances should be updated correctly. | +| ERC20-BASE-018 | [test_ERC20_transferFromMoreThanAllowance](https://github.com/crytic/properties/blob/main/contracts/ERC20/internal/properties/ERC20BasicProperties.sol#L294) | `transferFrom`s for more than allowance should not be allowed. | ### Tests for burnable tokens diff --git a/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol b/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol index c984c0a..44ee53d 100644 --- a/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol +++ b/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol @@ -317,4 +317,30 @@ abstract contract CryticERC20ExternalBasicProperties is ); } } + + // Transfers for more than allowance should not be allowed + function test_ERC20external_transferFromMoreThanAllowance( + address target + ) public { + uint256 balance_sender = token.balanceOf(msg.sender); + uint256 balance_receiver = token.balanceOf(target); + uint256 allowance = token.allowance(msg.sender, address(this)); + require(balance_sender > 0 && allowance < balance_sender); + + bool r = token.transferFrom(msg.sender, target, allowance + 1); + assertWithMsg( + r == false, + "Successful transferFrom for more than allowance" + ); + assertEq( + token.balanceOf(msg.sender), + balance_sender, + "TransferFrom for more than approval affected source balance" + ); + assertEq( + token.balanceOf(target), + balance_receiver, + "TransferFrom for more than approval affected target balance" + ); + } } diff --git a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol index 4159312..babee83 100644 --- a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol +++ b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol @@ -289,4 +289,30 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } } + + // TransferFrom for more than allowance should not be allowed + function test_ERC20_transferFromMoreThanAllowance( + address target + ) public { + uint256 balance_sender = balanceOf(msg.sender); + uint256 balance_receiver = balanceOf(target); + uint256 allowance = allowance(msg.sender, address(this)); + require(balance_sender > 0 && allowance < balance_sender); + + bool r = this.transferFrom(msg.sender, target, allowance + 1); + assertWithMsg( + r == false, + "Successful transferFrom for more than allowance" + ); + assertEq( + balanceOf(msg.sender), + balance_sender, + "TransferFrom for more than approval affected source balance" + ); + assertEq( + balanceOf(target), + balance_receiver, + "TransferFrom for more than approval affected target balance" + ); + } }