.. DO NOT EDIT. .. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY. .. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE: .. "api/gallery/contracts/verification/plot_05_echidna_fuzzing.py" .. LINE NUMBERS ARE GIVEN BELOW. .. only:: html .. note:: :class: sphx-glr-download-link-note :ref:`Go to the end ` to download the full example code or to run this example in your browser via JupyterLite. .. rst-class:: sphx-glr-example-title .. _sphx_glr_api_gallery_contracts_verification_plot_05_echidna_fuzzing.py: 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: .. math:: \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. .. GENERATED FROM PYTHON SOURCE LINES 27-32 .. code-block:: Python import matplotlib.pyplot as plt import blockchainkit as bk from blockchainkit.contracts import Contract .. GENERATED FROM PYTHON SOURCE LINES 33-35 A token with a caching bug, and its property -------------------------------------------- .. GENERATED FROM PYTHON SOURCE LINES 35-70 .. code-block:: Python 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 .. rst-class:: sphx-glr-script-out .. code-block:: none 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) .. GENERATED FROM PYTHON SOURCE LINES 71-73 How often does a random sequence find it? ----------------------------------------- .. GENERATED FROM PYTHON SOURCE LINES 73-102 .. code-block:: Python 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() .. image-sg:: /api/gallery/contracts/verification/images/sphx_glr_plot_05_echidna_fuzzing_001.png :alt: Longer sequences reach the bug more often :srcset: /api/gallery/contracts/verification/images/sphx_glr_plot_05_echidna_fuzzing_001.png :class: sphx-glr-single-img .. rst-class:: sphx-glr-script-out .. code-block:: none {1: 0.06666666666666667, 2: 0.16666666666666666, 4: 0.2, 8: 0.48333333333333334, 16: 0.7666666666666667} .. GENERATED FROM PYTHON SOURCE LINES 103-108 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? .. rst-class:: sphx-glr-timing **Total running time of the script:** (0 minutes 0.072 seconds) .. _sphx_glr_download_api_gallery_contracts_verification_plot_05_echidna_fuzzing.py: .. only:: html .. container:: sphx-glr-footer sphx-glr-footer-example .. container:: lite-badge .. image:: images/jupyterlite_badge_logo.svg :target: ../../../../lite/lab/index.html?path=api/gallery/contracts/verification/plot_05_echidna_fuzzing.ipynb :alt: Launch JupyterLite :width: 150 px .. container:: sphx-glr-download sphx-glr-download-jupyter :download:`Download Jupyter notebook: plot_05_echidna_fuzzing.ipynb ` .. container:: sphx-glr-download sphx-glr-download-python :download:`Download Python source code: plot_05_echidna_fuzzing.py ` .. container:: sphx-glr-download sphx-glr-download-zip :download:`Download zipped: plot_05_echidna_fuzzing.zip ` .. only:: html .. rst-class:: sphx-glr-signature `Gallery generated by Sphinx-Gallery `_