Echidna: property-based fuzzing finds a self-transfer bug (2020)

Echidna, from Trail of Bits, tests a contract the way QuickCheck tests a function. The author writes properties, functions that must always return true; the fuzzer sends random sequences of transactions, with random senders and arguments, checks every property after each one, and shrinks any failing sequence to a short counterexample.

The token below caches both balances before writing either. A transfer to oneself therefore writes the sender’s reduced balance, then overwrites it with the old balance plus the amount: money from nothing. Total supply is the property:

\[\sum_{a} \mathrm{balance}(a) = \mathrm{supply}.\]

Fuzzing finds the bug within a few transactions and shrinks the sequence to a self-transfer, preceded at most by the payment that gave the sender tokens. The rate at which random sequences hit it grows with their length, which is why fuzzers run long campaigns.

import matplotlib.pyplot as plt

import blockchainkit as bk
from blockchainkit.contracts import Contract

A token with a caching bug, and its property

class CachedToken(Contract):
    layout = ("supply", "balances")

    def constructor(self, supply):
        self.write("supply", supply)
        self.write("balances", self.sender, supply)

    def transfer(self, to, amount):
        source, target = self.read("balances", self.sender), self.read("balances", to)
        self.require(source >= amount, "insufficient balance")
        self.write("balances", self.sender, source - amount)
        self.write("balances", to, target + amount)

    def total(self):
        return sum(self.entries("balances").values())


def setup(world):
    return world.deploy("alice", CachedToken, 100)


def supply_conserved(world, token):
    return world.view(token, "total") == world.read(token, "supply")


accounts = ["alice", "bob", "carol"]
functions = {"transfer": [accounts, [0, 1, 10, 50, 200]]}
result = bk.contracts.fuzz(setup, functions, supply_conserved, senders=accounts, seed=2)
print(result)
assert result.failed and len(result.sequence) <= 2
last = result.sequence[-1]
assert last.sender == last.args[0] and last.args[1] > 0

FuzzResult(failed=True, sequence=(FuzzCall(sender='alice', function='transfer', args=('bob', 50)), FuzzCall(sender='bob', function='transfer', args=('bob', 10))), found_after=15, runs=2, transactions=15, original_length=5)

How often does a random sequence find it?

depths = [1, 2, 4, 8, 16]
rates = []
for depth in depths:
    found = sum(
        bk.contracts.fuzz(
            setup, functions, supply_conserved, senders=accounts, runs=1, depth=depth, seed=seed
        ).failed
        for seed in range(60)
    )
    rates.append(found / 60)
print(dict(zip(depths, rates, strict=True)))
assert rates[-1] > rates[0]

fig, ax = plt.subplots(figsize=(6, 4))
ax.plot(depths, rates, "o-", color="#2563eb")
ax.set(
    xscale="log",
    xticks=depths,
    xticklabels=depths,
    xlabel="transactions per random sequence",
    ylabel="fraction of sequences breaking the property",
    ylim=(0, 1),
    title="Longer sequences reach the bug more often",
)
fig.tight_layout()

plt.show()

{1: 0.06666666666666667, 2: 0.16666666666666666, 4: 0.2, 8: 0.48333333333333334, 16: 0.7666666666666667}

Exercise

Fix transfer by reading the recipient’s balance after writing the sender’s. Does the fuzzer still find a counterexample? What does a clean run of 100 sequences prove, and what does it not?