AAVE Potential Listings

1

Contracts

15

Rules

9

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

sUSD never decreases the allowance if it's set to max uint256. It's a non standard behavior. Not an issue because token supply is orders of magnitude lower than max uint256.

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
Subtitle

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

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

Pseudo formula


CVL CODE

rule noBurningTokens(method f) {
    uint256 totalSupplyBefore = totalSupply();
    env e;
    calldataarg args;
    f(e, args);
    assert totalSupply() >= totalSupplyBefore;
}
Subtitle

sUSD has methods that burn tokens by design.

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

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

Any user's balance can be decreased by burn(address account, uint amount) - only callable by system contracts