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;
}
Subtitle
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) == 0
Subtitle
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;
}
Subtitle
sUSD has methods that change total supply by design.
Description
Token supply is not decreasing.
METHODS
2setTotalSupply()
failureburn()
failurePseudo formula
CVL CODE
rule noBurningTokens(method f) {
uint256 totalSupplyBefore = totalSupply();
env e;
calldataarg args;
f(e, args);
assert totalSupply() >= totalSupplyBefore;
}
Subtitle
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;
}
Subtitle
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
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;
}
Subtitle
Any user's balance can be decreased by burn(address account, uint amount) - only callable by system contracts