Flashloan exploit

Adding flashloan capability

  • The new token code is at MinimalLendingToken.sol.

  • It defines an interface the borrowing contract needs to implement:

    interface IFlashLoanReceiver {
    function execute() external payable;
}

  • It adds a flashLoan function:

        function flashLoan(uint256 amount) public {
        uint256 preBalance = address(this).balance;
        require(preBalance >= amount, "Insufficient funds");

        IFlashLoanReceiver(msg.sender).execute{value: amount}(); 

        uint256 postBalance = address(this).balance;
        require(postBalance >= preBalance, "Loan has not been repaid");
    }

Creating a borrower

We use the Prover’s over-approximation of the storage to create a contract that “might do anything”.

Simplified example

uint8 public storageVar;
uint256 public amount;

function doSomething() public {

    if (storageVar == 0) {  // Deposit
        token.deposit{value: amount}(amount);
    } else if (storageVar == 1) {  // Loan
        token.flashLoan(amount);
    } else if (storageVar == 2) {  // Repay
        payable(address(token)).send(amount);
    } else { // Vote
        voting.vote(booleans[i]);
    }
}

  • By default, the Prover makes no assumptions on the values of storageVar and amount.

  • Therefore doSomething might do any of the actions specified.

Borrower code

  • This is a more sophisticated example, which allows it to do two actions at once.

FlashLoanReceiverHarness.sol
FlashLoanReceiverHarness.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;


import {IFlashLoanReceiver, MinimalToken} from "./MinimalLendingToken.sol";
import {PowerVoting} from "./PowerVoting.sol";

// A contract that may do anything.
// We use the Provver's over-approximation of storage for enabling any possible action.
contract FlashLoanReceiverHarness is IFlashLoanReceiver {

    MinimalToken public token;
    PowerVoting public voting;

    // Which function to call
    enum Func {
        Deposit,
        FlashLoan,
        Vote,
        DoNothing
    }
    mapping(uint8 => Func) public toCalls;

    // The amounts to use in the function calls
    mapping(uint8 => uint256) public amounts;

    // Boolean values to use
    mapping(uint8 => bool) public booleans;

    // The iteration number
    uint8 public i;

    function doSingleSomething() public {
        i += 1;  // Increase iteration

        if (toCalls[i] == Func.Deposit) {
            token.deposit{value: amounts[i]}(amounts[i]);
        } else if (toCalls[i] == Func.FlashLoan) {
            token.flashLoan(amounts[i]);
        } else if (toCalls[i] == Func.DoNothing) {
            // Do nothing
        } else {
            voting.vote(booleans[i]);
        }
    }

    function doSomethings() public {
        for (uint8 j; j < 2; j++) {
            doSingleSomething();
        }
    }

    function execute() external payable override {
        doSomethings();
    }
}

Revisiting tokenSolvency

LenderPowerVotingInvariant.spec
/// @title Total supply not greater than ETH balance
invariant tokenSolvency()
    nativeBalances[token] >= token.totalSupply();

Exercises

Task 10: Understand the violation

Task 11: Checking if exploits are possible

satisfy balanceOf(user1) > balanceOf(user2);

We cannot only use assert statements to verify properties, but we can also check whether there is a path along the execution of contract functions that allows for certain exploits to be applied to our contracts. To this end, we can use satisfy statements that check if there is at least one viable path that allows the execution of some predefined scenario.

Use the satisfy keyword to make the Prover search for a positive example that represents a violation of the following invariant:

  1. Property: total votes are less than or equal to total eth in the system.

Hint

Can you think of a flashloan exploit to increase your voting power?

Solution
LenderPowerVoting.spec
/// @title An exploit example
rule example() {
    // The following requirements are just to make it easier to see the problem
    require totalVotes() == 0;
    require nativeBalances[borrower] == 0;
    require token.balanceOf(borrower) == 0;

    // The total ETH in the system before
    mathint totalBalances = nativeBalances[token] + nativeBalances[borrower];

    env e;
    borrower.doSomethings(e);

    // More votes than total ETH
    satisfy to_mathint(totalVotes()) > totalBalances;
}