ERC-20 transferFrom greater than allowance not allowed

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
 

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"
+        );
+    }
 }

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"
+        );
+    }
 }