NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Remove non-standard increaseAllowance and decreaseAllowance from ERC20 (#4585)

Browse Source 
Co-authored-by: Francisco <fg@frang.io>
This commit is contained in:
Hadrien Croubois
2023-09-12 16:59:48 +02:00
committed by GitHub
parent 36bf1e46fa
commit 60e3ffe6a3
4 changed files with 5 additions and 285 deletions
Download Patch File Download Diff File Expand all files Collapse all files

72
certora/specs/ERC20.spec
View File

@ -3,10 +3,6 @@ import "methods/IERC20.spec";
import "methods/IERC2612.spec";
methods {
// non standard ERC20 functions
function increaseAllowance(address,uint256) external returns (bool);
function decreaseAllowance(address,uint256) external returns (bool);
// exposed for FV
function mint(address,uint256) external;
function burn(address,uint256) external;
@ -117,7 +113,6 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) {
allowanceAfter > allowanceBefore
) => (
(f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder) ||
(f.selector == sig:increaseAllowance(address,uint256).selector && e.msg.sender == holder) ||
(f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
);
@ -126,7 +121,6 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) {
) => (
(f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
(f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder ) ||
(f.selector == sig:decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) ||
(f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector)
);
}
@ -307,72 +301,6 @@ rule approve(env e) {
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: increaseAllowance behavior and side effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule increaseAllowance(env e) {
require nonpayable(e);
address holder = e.msg.sender;
address spender;
address otherHolder;
address otherSpender;
uint256 amount;
// cache state
uint256 allowanceBefore = allowance(holder, spender);
uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
// run transaction
increaseAllowance@withrevert(e, spender, amount);
// check outcome
if (lastReverted) {
assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256;
} else {
// allowance is updated
assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount;
// other allowances are untouched
assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: decreaseAllowance behavior and side effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule decreaseAllowance(env e) {
require nonpayable(e);
address holder = e.msg.sender;
address spender;
address otherHolder;
address otherSpender;
uint256 amount;
// cache state
uint256 allowanceBefore = allowance(holder, spender);
uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender);
// run transaction
decreaseAllowance@withrevert(e, spender, amount);
// check outcome
if (lastReverted) {
assert holder == 0 || spender == 0 || allowanceBefore < amount;
} else {
// allowance is updated
assert to_mathint(allowance(holder, spender)) == allowanceBefore - amount;
// other allowances are untouched
assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: permit behavior and side effects │