From e107c8a2c646522edae79aead5db26750a1cbea7 Mon Sep 17 00:00:00 2001 From: broccolirob Date: Tue, 29 Aug 2023 01:52:24 -0400 Subject: [PATCH 1/3] ERC-20 transferFrom greater than allowance not allowed --- PROPERTIES.md | 1 + .../ERC20ExternalBasicProperties.sol | 26 +++++++++++++++++++ .../properties/ERC20BasicProperties.sol | 26 +++++++++++++++++++ 3 files changed, 53 insertions(+) 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..8cd3fe9 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 amount approved source allowance" + ); + assertEq( + token.balanceOf(target), + balance_receiver, + "TransferFrom for more than amount approved target allowance" + ); + } } diff --git a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol index 4159312..ce6b421 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 = 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 amount approved source allowance" + ); + assertEq( + token.balanceOf(target), + balance_receiver, + "TransferFrom for more than amount approved target allowance" + ); + } } From 7d203659910ad3c05ed39bbc9f22f006a7334bf8 Mon Sep 17 00:00:00 2001 From: broccolirob Date: Tue, 29 Aug 2023 09:56:38 -0400 Subject: [PATCH 2/3] Update internal ERC-20 property to use internal references --- .../internal/properties/ERC20BasicProperties.sol | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol index ce6b421..5b48f5f 100644 --- a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol +++ b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol @@ -294,23 +294,23 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { function test_ERC20_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)); + 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 = token.transferFrom(msg.sender, target, allowance + 1); + bool r = this.transferFrom(msg.sender, target, allowance + 1); assertWithMsg( r == false, "Successful transferFrom for more than allowance" ); assertEq( - token.balanceOf(msg.sender), + balanceOf(msg.sender), balance_sender, "TransferFrom for more than amount approved source allowance" ); assertEq( - token.balanceOf(target), + balanceOf(target), balance_receiver, "TransferFrom for more than amount approved target allowance" ); From f7d0766f2324763aaf08126a86896c2746fbfa2c Mon Sep 17 00:00:00 2001 From: broccolirob Date: Fri, 8 Sep 2023 10:18:27 -0400 Subject: [PATCH 3/3] Fix error message --- .../external/properties/ERC20ExternalBasicProperties.sol | 4 ++-- contracts/ERC20/internal/properties/ERC20BasicProperties.sol | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol b/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol index 8cd3fe9..44ee53d 100644 --- a/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol +++ b/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol @@ -335,12 +335,12 @@ abstract contract CryticERC20ExternalBasicProperties is assertEq( token.balanceOf(msg.sender), balance_sender, - "TransferFrom for more than amount approved source allowance" + "TransferFrom for more than approval affected source balance" ); assertEq( token.balanceOf(target), balance_receiver, - "TransferFrom for more than amount approved target allowance" + "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 5b48f5f..babee83 100644 --- a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol +++ b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol @@ -307,12 +307,12 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { assertEq( balanceOf(msg.sender), balance_sender, - "TransferFrom for more than amount approved source allowance" + "TransferFrom for more than approval affected source balance" ); assertEq( balanceOf(target), balance_receiver, - "TransferFrom for more than amount approved target allowance" + "TransferFrom for more than approval affected target balance" ); } }