AAVE Potential Listings

10

Contracts

106

Rules

81

Rules Verified

noFeeOnTransferFrom

Last update 22/06/2022
feature verified

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;
}

noFeeOnTransfer

Last update 22/06/2022
feature verified

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;
}

transferCorrect

Last update 22/06/2022
security verified

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;
    }
}

transferFromCorrect

Last update 22/06/2022
security failure

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.

transferFromReverts

Last update 22/06/2022
security verified

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

ZeroAddressNoBalance

Last update 22/06/2022
security failure

Description

Balance of address 0 is always 0

METHODS

1

issue()

failure

Pseudo formula

{ balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0
Notes

Zero address might get balance as a result of calling issue() - only callable by system contracts

NoChangeTotalSupply

Last update 22/06/2022
feature failure

Description

Contract calls don't change token total supply.

METHODS

3

burn()

failure

setTotalSupply()

failure

issue()

failure

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

sUSD has methods that change total supply by design.

noBurningTokens

Last update 22/06/2022
feature failure

Description

Token supply is not decreasing.

METHODS

2

setTotalSupply()

failure

burn()

failure

CVL 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.

noMintingTokens

Last update 22/06/2022
feature failure

Description

No new tokens are minted.

METHODS

2

setTotalSupply()

failure

mint()

failure

CVL CODE

rule noMintingTokens(method f) {
    uint256 totalSupplyBefore = totalSupply();
    env e;
    calldataarg args;
    f(e, args);
    assert totalSupply() <= totalSupplyBefore;
}
Notes

sUSD is mintable by design.

ChangingAllowance

Last update 22/06/2022
security verified

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;
    }
}

TransferSumOfFromAndToBalancesStaySame

Last update 22/06/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 22/06/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 22/06/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 22/06/2022
security failure

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

noFeeOnTransferFrom

Last update 27/06/2022
feature verified

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;
}

noFeeOnTransfer

Last update 27/06/2022
feature verified

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;
}

transferCorrect

Last update 27/06/2022
security failure

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.

transferFromCorrect

Last update 27/06/2022
security verified

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.

transferFromReverts

Last update 27/06/2022
security failure

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

ZeroAddressNoBalance

Last update 27/06/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

{ balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

NoChangeTotalSupply

Last update 27/06/2022
feature failure

Description

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

ChangingAllowance

Last update 27/06/2022
security skipped

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

TransferSumOfFromAndToBalancesStaySame

Last update 27/06/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 27/06/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 27/06/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 27/06/2022
security failure

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.

noFeeOnTransferFrom

Last update 28/06/2022
feature verified

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;
}

noFeeOnTransfer

Last update 28/06/2022
feature verified

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;
}

transferCorrect

Last update 28/06/2022
security verified

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;
    }
}

transferFromCorrect

Last update 28/06/2022
security verified

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;
}

transferFromReverts

Last update 28/06/2022
security verified

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

ZeroAddressNoBalance

Last update 28/06/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

{ balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

NoChangeTotalSupply

Last update 28/06/2022
feature failure

Description

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.

ChangingAllowance

Last update 28/06/2022
security failure

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.

TransferSumOfFromAndToBalancesStaySame

Last update 28/06/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 28/06/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 28/06/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 28/06/2022
security failure

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.

noFeeOnTransferFrom

Last update 20/07/2022
feature verified

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;
}

noFeeOnTransfer

Last update 20/07/2022
feature verified

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;
}

transferCorrect

Last update 20/07/2022
security verified

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;
    }
}

transferFromCorrect

Last update 20/07/2022
security verified

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;
}

transferFromReverts

Last update 20/07/2022
security verified

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

ZeroAddressNoBalance

Last update 20/07/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

 { balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

ChangingAllowance

Last update 20/07/2022
security verified

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;
    }
}

TransferSumOfFromAndToBalancesStaySame

Last update 20/07/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 20/07/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 20/07/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 20/07/2022
security verified

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;
}

isMintPrivileged

Last update 20/07/2022
security verified

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

noFeeOnTransferFrom

Last update 24/07/2022
feature verified

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;
}

noFeeOnTransfer

Last update 24/07/2022
feature verified

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;
}

transferCorrect

Last update 24/07/2022
security verified

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;
    }
}

transferFromCorrect

Last update 24/07/2022
security verified

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

transferFromReverts

Last update 24/07/2022
security verified

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

ZeroAddressNoBalance

Last update 24/07/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

 { balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

ChangingAllowance

Last update 24/07/2022
security failure

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

The rule fails on burnFrom() and permit(), this is by design as these functions are supposed to change allowance.

TransferSumOfFromAndToBalancesStaySame

Last update 24/07/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 24/07/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 24/07/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 24/07/2022
security failure

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

isMintPrivileged

Last update 24/07/2022
security verified

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)

noFeeOnTransferFrom

Last update 16/08/2022
feature verified

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;
}

noFeeOnTransfer

Last update 16/08/2022
feature verified

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;
}

transferCorrect

Last update 16/08/2022
security verified

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;
    }
}

transferFromCorrect

Last update 16/08/2022
security verified

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;
}

transferFromReverts

Last update 16/08/2022
security verified

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

ZeroAddressNoBalance

Last update 16/08/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

 { balanceOf(0) = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

ChangingAllowance

Last update 16/08/2022
security verified

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;
    }
}

TransferSumOfFromAndToBalancesStaySame

Last update 16/08/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 16/08/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 16/08/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 21/08/2022
security verified

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;
}

isMintPrivileged

Last update 21/08/2022
security verified

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

noFeeOnTransferFrom

Last update 21/08/2022
feature verified

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;
}

noFeeOnTransfer

Last update 21/08/2022
feature verified

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;
}

transferCorrect

Last update 21/08/2022
security failure

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.

transferFromCorrect

Last update 21/08/2022
security verified

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;
}

transferFromReverts

Last update 21/08/2022
security verified

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

ZeroAddressNoBalance

Last update 21/08/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

  { balanceOf(0) = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

ChangingAllowance

Last update 21/08/2022
security failure

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

Fails because burnFrom() also changes allowance and it is not accounted by the rule. This is by design.

TransferSumOfFromAndToBalancesStaySame

Last update 21/08/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 21/08/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 21/08/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 21/08/2022
security failure

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

isMintPrivileged

Last update 21/08/2022
security failure

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

noFeeOnTransferFrom

Last update 30/05/2022
feature verified

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;
}

noFeeOnTransfer

Last update 30/05/2022
feature verified

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;
}

transferCorrect

Last update 30/05/2022
security verified

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;
    }
}

transferFromCorrect

Last update 30/05/2022
security verified

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;
}

transferFromReverts

Last update 30/05/2022
security verified

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

ZeroAddressNoBalance

Last update 30/05/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

{ balanceOf[0] = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

NoChangeTotalSupply

Last update 30/05/2022
feature failure

Description

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.

ChangingAllowance

Last update 30/05/2022
security verified

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;
    }
}

TransferSumOfFromAndToBalancesStaySame

Last update 30/05/2022
security verified

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;
}

TransferDoesntChangeOtherBalance

Last update 30/05/2022
security verified

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

TransferFromDoesntChangeOtherBalance

Last update 30/05/2022
security verified

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

OtherBalanceOnlyGoesUp

Last update 30/05/2022
security verified

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;
}

ChangingAllowance

Last update 24/11/2022
security failure

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;
}

TransferDoesntChangeOtherBalance

Last update 24/11/2022
security verified

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

isMintPrivileged

Last update 24/11/2022
security failure

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.

noFeeOnTransfer

Last update 24/11/2022
feature verified

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;
}

transferFromReverts

Last update 24/11/2022
security failure

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.

ZeroAddressNoBalance

Last update 24/11/2022
security verified

Description

Balance of address 0 is always 0

Pseudo formula

{ balanceOf(0) = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

TransferSumOfFromAndToBalancesStaySame

Last update 24/11/2022
security verified

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;
}

transferCorrect

Last update 24/11/2022
security failure

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.

TransferFromDoesntChangeOtherBalance

Last update 24/11/2022
security verified

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

transferFromCorrect

Last update 24/11/2022
security verified

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;
}

OtherBalanceOnlyGoesUp

Last update 24/11/2022
security failure

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.

noFeeOnTransferFrom

Last update 24/11/2022
feature verified

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;
}