AAVE Potential Listings
10
Contracts
106
Rules
81
Rules Verified
sUSD
Description
Verify that there is no fee on transferFrom()
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0. This rule fails on tokens with a blacklist function, like USDC and USDT. The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Notes
sUSD never decreases the allowance if it's set to max uint256. It's a non standard behavior. Not an issue because token supply is orders of magnitude lower than max uint256.
Description
transferFrom() should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
METHODS
1issue()
failurePseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Notes
Zero address might get balance as a result of calling issue() - only callable by system contracts
Description
Contract calls don't change token total supply.
METHODS
3burn()
failuresetTotalSupply()
failureissue()
failurePseudo formula
{
supplyBefore = totalSupply()
}
< f(e, args)>
{
supplyAfter = totalSupply()
supplyBefore == supplyAfter
}CVL CODE
rule NoChangeTotalSupply(method f) {
// require f.selector != burn(uint256).selector && f.selector != mint(address, uint256).selector;
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() == totalSupplyBefore;
}Notes
sUSD has methods that change total supply by design.
Description
Token supply is not decreasing.
METHODS
2setTotalSupply()
failureburn()
failureCVL CODE
rule noBurningTokens(method f) {
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() >= totalSupplyBefore;
}Notes
sUSD has methods that burn tokens by design.
Description
No new tokens are minted.
METHODS
2setTotalSupply()
failuremint()
failureCVL CODE
rule noMintingTokens(method f) {
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() <= totalSupplyBefore;
}Notes
sUSD is mintable by design.
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
22/06/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Notes
Any user's balance can be decreased by burn(address account, uint amount) - only callable by system contracts
sAVAX
Description
Verify that there is no fee on transferFrom()
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0. This rule fails on tokens with a blacklist function, like USDC and USDT. The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Notes
Rule fails since the token is pausable and transfers don't work in a paused state.
Description
Test that transferFrom works correctly and balances are properly updated.
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Notes
Unlike the transferCorrect rule, this rule doesn't test for reverts so it doesn't fail in a paused state.
Description
transferFrom() should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Notes
Fails since the token is pausable
Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Contract calls don't change token total supply.
Pseudo formula
{
supplyBefore = totalSupply()
}
< f(e, args)>
{
supplyAfter = totalSupply()
supplyBefore == supplyAfter
}CVL CODE
rule NoChangeTotalSupply(method f) {
// require f.selector != burn(uint256).selector && f.selector != mint(address, uint256).selector;
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() == totalSupplyBefore;
}Notes
Fails since the token is mintable
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Notes
The prover skipped this rule because the token doesn't have increaseAllowance and decreaseAllowance functions implemented
Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
27/06/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Notes
The rule fails because token contract itself holds a balance that changes as a result of some operations. This is by design.
FRAX
Description
Verify that there is no fee on transferFrom()
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0. This rule fails on tokens with a blacklist function, like USDC and USDT. The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Description
Test that transferFrom works correctly and balances are properly updated.
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Description
transferFrom() should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Contract calls don't change token total supply.
Pseudo formula
{
supplyBefore = totalSupply()
}
< f(e, args)>
{
supplyAfter = totalSupply()
supplyBefore == supplyAfter
}CVL CODE
rule NoChangeTotalSupply(method f) {
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() == totalSupplyBefore;
}Notes
FRAX is mintable, hence the rule fails.
Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>a
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Notes
burnFrom() and permit() methods break the rule because we don't account for them in the spec, as they're not standard erc20 functions. This rule violation is by design.
Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
28/06/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Notes
burnFrom() changes an arbitrary address's balance and breaks the rule. This is by design.
stMatic
Description
Verify that there is no fee on transferFrom() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0 && e.msg.sender != currentContract;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}
CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}
Description
transferFrom should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}
CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}
CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}
TransferFromSumOfFromAndToBalancesStaySame
Last update
20/07/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}
Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}
CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Description
Checks if mint operation is privileged - only one address may mint. Note that tokens might allow the minter role to more than one address
CVL CODE
rule isMintPrivileged(address privileged, address recipient, uint256 amount) {
env e1;
require e1.msg.sender == privileged;
storage initialStorage = lastStorage;
uint256 totalSupplyBefore = totalSupply();
mint(e1, recipient, amount); // no revert
uint256 totalSupplyAfter1 = totalSupply();
require(totalSupplyAfter1 > totalSupplyBefore);
env e2;
require e2.msg.sender != privileged;
mint@withrevert(e2, recipient, amount) at initialStorage;
bool secondSucceeded = !lastReverted;
uint256 totalSupplyAfter2 = totalSupply();
// either non privileged mint reverted or it didn't influence total supply
assert !secondSucceeded || (totalSupplyBefore == totalSupplyAfter2);
}Description
Verify that there is no fee on transferFrom() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0 && e.msg.sender != currentContract;
require lowerThanMaxBlock(e.block.number);
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
uint256 votesTo = getVotes(delegates(to));
require (votesTo + amount) < MAX_SUPPLY();
uint256 votesFrom = getVotes(delegates(e.msg.sender));
require votesFrom >= amount;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
uint256 votesTo = getVotes(delegates(to));
require (votesTo + amount) < MAX_SUPPLY();
uint256 votesFrom = getVotes(delegates(from));
require votesFrom >= amount;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
( allowance(from, e.msg.sender) == allowanceBefore - amount ||
allowance(from, e.msg.sender) == max_uint256);
}Description
transferFrom should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}
CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
require lowerThanMaxBlock(e.block.number);
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
uint256 votesTo = getVotes(delegates(to));
require (votesTo + amount) < MAX_SUPPLY();
uint256 votesFrom = getVotes(delegates(from));
require votesFrom >= amount;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Notes
The rule fails on burnFrom() and permit(), this is by design as these functions are supposed to change allowance.
Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
24/07/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}
Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}
CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Notes
Other's balance changes on burnFrom() function, this is by design
Description
verifies that the mint operation is privileged - only one address may mint.
CVL CODE
rule isMintPrivileged(address privileged, address recipient, uint256 amount) {
env e1;
require e1.msg.sender == privileged;
storage initialStorage = lastStorage;
uint256 totalSupplyBefore = totalSupply();
mint(e1, recipient, amount); // no revert
uint256 totalSupplyAfter1 = totalSupply();
require(totalSupplyAfter1 > totalSupplyBefore);
env e2;
require e2.msg.sender != privileged;
mint@withrevert(e2, recipient, amount) at initialStorage;
bool secondSucceeded = !lastReverted;
uint256 totalSupplyAfter2 = totalSupply();
// either non privileged mint reverted or it didn't influence total supply
assert !secondSucceeded || (totalSupplyBefore == totalSupplyAfter2);
}MAI (Avalanche & Polygon)
Description
Verify that there is no fee on transferFrom() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0 && e.msg.sender != currentContract;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}
Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}
Description
transferFrom should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf(0) = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}
CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}
CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
16/08/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}
CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Description
Checks if mint operation is privileged - only one address may mint.
CVL CODE
rule isMintPrivileged(address privileged, address recipient, uint256 amount) {
env e1;
require e1.msg.sender == privileged;
storage initialStorage = lastStorage;
uint256 totalSupplyBefore = totalSupply();
mint(e1, recipient, amount); // no revert
uint256 totalSupplyAfter1 = totalSupply();
require(totalSupplyAfter1 > totalSupplyBefore);
env e2;
require e2.msg.sender != privileged;
mint@withrevert(e2, recipient, amount) at initialStorage;
bool secondSucceeded = !lastReverted;
uint256 totalSupplyAfter2 = totalSupply();
// either non privileged mint reverted or it didn't influence total supply
assert !secondSucceeded || (totalSupplyBefore == totalSupplyAfter2);
}BTC.b
Description
Verify that there is no fee on transferFrom() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0 && e.msg.sender != currentContract;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Notes
Fails because the contract doesn't allow token transfer to its own address. This is by design.
Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Description
transferFrom should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}
CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf(0) = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}
Notes
Fails because burnFrom() also changes allowance and it is not accounted by the rule. This is by design.
Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}
CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
21/08/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}
CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}Notes
Fails because the burnFrom() function changes balance of an arbitrary address. By design
Description
Checks if mint operation is privileged - only one address may mint.
CVL CODE
rule isMintPrivileged(address privileged, address recipient, uint256 amount) {
env e1;
require e1.msg.sender == privileged;
storage initialStorage = lastStorage;
uint256 totalSupplyBefore = totalSupply();
mint(e1, recipient, amount, 0, 0, 0, 0); // no revert
uint256 totalSupplyAfter1 = totalSupply();
require(totalSupplyAfter1 > totalSupplyBefore);
env e2;
require e2.msg.sender != privileged;
mint@withrevert(e2, recipient, amount, 0, 0, 0, 0) at initialStorage;
bool secondSucceeded = !lastReverted;
uint256 totalSupplyAfter2 = totalSupply();
// either non privileged mint reverted or it didn't influence total supply
assert !secondSucceeded || (totalSupplyBefore == totalSupplyAfter2);
}Notes
Fails because mint() function is access controlled by a bridgeRoles() check and multiple addresses might have this role. By design
CVX
Description
Verify that there is no fee on transferFrom()
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0. This rule fails on tokens with a blacklist function, like USDC and USDT. The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}Description
Test that transferFrom works correctly and balances are properly updated.
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Description
transferFrom() should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf[0] = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Contract calls don't change token total supply.
Pseudo formula
{
supplyBefore = totalSupply()
}
< f(e, args)>
{
supplyAfter = totalSupply()
supplyBefore == supplyAfter
}CVL CODE
rule NoChangeTotalSupply(method f) {
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() == totalSupplyBefore;
}Notes
CVX is mintable, hence the rule fails.
Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>a
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}TransferFromSumOfFromAndToBalancesStaySame
Last update
30/05/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}cbETH
Description
Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance
Pseudo formula
{
allowanceBefore = allowance(from, spender)
}
<
f(e, args)
>
{
f.selector = approve(spender, amount) => allowance(from, spender) = amount
f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
generic f.selector => allowance(from, spender) == allowanceBefore
}CVL CODE
rule ChangingAllowance(method f, address from, address spender) {
uint256 allowanceBefore = allowance(from, spender);
env e;
if (f.selector == approve(address, uint256).selector) {
address spender_;
uint256 amount;
approve(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == transferFrom(address,address,uint256).selector) {
address from_;
address to;
address amount;
transferFrom(e, from_, to, amount);
uint256 allowanceAfter = allowance(from, spender);
if (from == from_ && spender == e.msg.sender) {
assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == decreaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount <= allowanceBefore;
decreaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore - amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else if (f.selector == increaseAllowance(address, uint256).selector) {
address spender_;
uint256 amount;
require amount + allowanceBefore < max_uint256;
increaseAllowance(e, spender_, amount);
if (from == e.msg.sender && spender == spender_) {
assert allowance(from, spender) == allowanceBefore + amount;
} else {
assert allowance(from, spender) == allowanceBefore;
}
} else
{
calldataarg args;
f(e, args);
assert allowance(from, spender) == allowanceBefore;
}
}
Notes
Failure is due to permit() function changing allowance and not being taken into account by standard spec. Behavior by design.
TransferFromSumOfFromAndToBalancesStaySame
Last update
24/11/2022
security
verified
Description
Transfer using transferFrom() from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(a) + balanceOf(b)
}
<
transferFrom(a, b)
>
{
balancesBefore == balanceOf(a) + balanceOf(b)
}CVL CODE
rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
env e;
mathint sum = balanceOf(from) + balanceOf(to);
require sum < max_uint256;
transferFrom(e, from, to, amount);
assert balanceOf(from) + balanceOf(to) == sum;
}
Description
Transfer from msg.sender to alice doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(bob)
}
<
transfer(alice, amount)
>
{
balanceOf(bob) == balanceBefore
}CVL CODE
rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
env e;
require other != e.msg.sender;
require other != to && other != currentContract;
uint256 balanceBefore = balanceOf(other);
transfer(e, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Checks if mint operation is privileged - only one address may mint.
CVL CODE
rule isMintPrivileged(address privileged, address recipient, uint256 amount) {
env e1;
require e1.msg.sender == privileged;
storage initialStorage = lastStorage;
uint256 totalSupplyBefore = totalSupply();
mint(e1, recipient, amount); // no revert
uint256 totalSupplyAfter1 = totalSupply();
require(totalSupplyAfter1 > totalSupplyBefore);
env e2;
require e2.msg.sender != privileged;
mint@withrevert(e2, recipient, amount) at initialStorage;
bool secondSucceeded = !lastReverted;
uint256 totalSupplyAfter2 = totalSupply();
// either non privileged mint reverted or it didn't influence total supply
assert !secondSucceeded || (totalSupplyBefore == totalSupplyAfter2);
}Notes
Fails because the token has a minters array and multiple addresses are allowed to receive the minter role. Behavior by design.
Description
Verify that there is no fee on transfer() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
balances[msg.sender] >= amount
}
<
transfer(bob, amount)
>
{
balances[bob] = y + amount
}
CVL CODE
rule noFeeOnTransfer(address bob, uint256 amount) {
env e;
calldataarg args;
require bob != e.msg.sender;
uint256 balanceSenderBefore = balanceOf(e.msg.sender);
uint256 balanceBefore = balanceOf(bob);
transfer(e, bob, amount);
uint256 balanceAfter = balanceOf(bob);
uint256 balanceSenderAfter = balanceOf(e.msg.sender);
assert balanceAfter == balanceBefore + amount;
}Description
transferFrom() should revert if and only if the amount is too high or the recipient is 0.
Pseudo formula
{
allowanceBefore = allowance(alice, bob)
fromBalanceBefore = balanceOf(alice)
}
<
transferFrom(alice, bob, amount)
>
{
lastReverted <=> allowanceBefore < amount || amount > fromBalanceBefore || to = 0
}CVL CODE
rule transferFromReverts(address from, address to, uint256 amount) {
env e;
uint256 allowanceBefore = allowance(from, e.msg.sender);
uint256 fromBalanceBefore = balanceOf(from);
require from != 0 && e.msg.sender != 0;
require e.msg.value == 0;
require fromBalanceBefore + balanceOf(to) <= max_uint256;
transferFrom@withrevert(e, from, to, amount);
assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0);
}Notes
Rule fails because the token is pausable and in paused state transfers always revert, which is not taken into account by the standard spec. Behavior by design.
Description
Balance of address 0 is always 0
Pseudo formula
{ balanceOf(0) = 0 }CVL CODE
invariant ZeroAddressNoBalance()
balanceOf(0) == 0Description
Transfer from a to b doesn't change the sum of their balances
Pseudo formula
{
balancesBefore = balanceOf(msg.sender) + balanceOf(b)
}
<
transfer(b, amount)
>
{
balancesBefore == balanceOf(msg.sender) + balanceOf(b)
}
CVL CODE
rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
env e;
mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
require sum < max_uint256;
transfer(e, to, amount);
assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}Description
Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.
Pseudo formula
{
balanceFromBefore = balanceOf(msg.sender)
balanceToBefore = balanceOf(to)
}
<
transfer(to, amount)
>
{
lastReverted => to = 0 || amount > balanceOf(msg.sender)
!lastReverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(msg.sender) = balanceFromBefore - amount
}CVL CODE
rule transferCorrect(address to, uint256 amount) {
env e;
require e.msg.value == 0 && e.msg.sender != 0 && e.msg.sender != currentContract;
uint256 fromBalanceBefore = balanceOf(e.msg.sender);
uint256 toBalanceBefore = balanceOf(to);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transfer@withrevert(e, to, amount);
bool reverted = lastReverted;
if (!reverted) {
if (e.msg.sender == to) {
assert balanceOf(e.msg.sender) == fromBalanceBefore;
} else {
assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
assert balanceOf(to) == toBalanceBefore + amount;
}
} else {
assert amount > fromBalanceBefore || to == 0;
}
}
Notes
Rule fails because the token is pausable and in paused state transfers always revert, which is not taken into account by the standard spec. Behavior by design.
Description
Transfer from alice to bob using transferFrom doesn't change the balance of other addresses
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
transferFrom(alice, bob, amount)
>
{
balanceOf(charlie) = balanceBefore
}CVL CODE
rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
env e;
require other != from;
require other != to;
uint256 balanceBefore = balanceOf(other);
transferFrom(e, from, to, amount);
assert balanceBefore == balanceOf(other);
}
Description
Test that transferFrom works correctly. Balances are updated if not reverted. If reverted, it means the transfer amount was too high, or the recipient is 0
Pseudo formula
{
balanceFromBefore = balanceOf(from)
balanceToBefore = balanceOf(to)
}
<
transferFrom(from, to, amount)
>tr
{
lastreverted => to = 0 || amount > balanceOf(from)
!lastreverted => balanceOf(to) = balanceToBefore + amount &&
balanceOf(from) = balanceFromBefore - amount
}
CVL CODE
rule transferFromCorrect(address from, address to, uint256 amount) {
env e;
require e.msg.value == 0;
uint256 fromBalanceBefore = balanceOf(from);
uint256 toBalanceBefore = balanceOf(to);
uint256 allowanceBefore = allowance(from, e.msg.sender);
require fromBalanceBefore + toBalanceBefore <= max_uint256;
transferFrom(e, from, to, amount);
assert from != to =>
balanceOf(from) == fromBalanceBefore - amount &&
balanceOf(to) == toBalanceBefore + amount &&
allowance(from, e.msg.sender) == allowanceBefore - amount;
}Description
Balance of an address, who is not a sender or a recipient in transfer functions, doesn't decrease as a result of contract calls
Pseudo formula
{
balanceBefore = balanceOf(charlie)
}
<
f(e, args)
>
{
f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
}
CVL CODE
rule OtherBalanceOnlyGoesUp(address other, method f) {
env e;
require other != currentContract;
uint256 balanceBefore = balanceOf(other);
if (f.selector == transferFrom(address, address, uint256).selector) {
address from;
address to;
uint256 amount;
require(other != from);
require balanceOf(from) + balanceBefore < max_uint256;
transferFrom(e, from, to, amount);
} else if (f.selector == transfer(address, uint256).selector) {
require other != e.msg.sender;
require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
calldataarg args;
f(e, args);
} else {
require other != e.msg.sender;
calldataarg args;
f(e, args);
}
assert balanceOf(other) >= balanceBefore;
}
Notes
Rule fails as transferWithAuthorization() and receiveWithAuthorization() change "other's" balance and they're not accounted for by our standard spec. This is behavior by design.
Description
Verify that there is no fee on transferFrom() (like potentially on USDT)
Pseudo formula
{
balances[bob] = y
allowance(alice, msg.sender) >= amount
}
<
transferFrom(alice, bob, amount)
>
{
balances[bob] = y + amount
}
CVL CODE
rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) {
env e;
calldataarg args;
require alice != bob;
require allowance(alice, e.msg.sender) >= amount;
uint256 balanceBefore = balanceOf(bob);
transferFrom(e, alice, bob, amount);
uint256 balanceAfter = balanceOf(bob);
assert balanceAfter == balanceBefore + amount;
}