.. DO NOT EDIT.
.. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY.
.. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE:
.. "api/gallery/contracts/verification/plot_04_oyente.py"
.. LINE NUMBERS ARE GIVEN BELOW.

.. only:: html

    .. note::
        :class: sphx-glr-download-link-note

        :ref:`Go to the end <sphx_glr_download_api_gallery_contracts_verification_plot_04_oyente.py>`
        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_04_oyente.py:


Oyente: symbolic execution finds the BeautyChain overflow in bytecode (2016)
============================================================================

Oyente, by Luu, Chu, Olickel, Saxena and Hobor, ran symbolic execution on
deployed EVM bytecode, with the Z3 solver deciding which paths were
feasible. Run over 19,366 contracts on the main network, it flagged about
8,800 as vulnerable, including the DAO. Working on bytecode means checking
what actually runs, not what the source was meant to say.

Here the same idea runs over the stack machine of :mod:`blockchainkit.vm`.
Storage slot ``k`` starts as the symbol ``s<k>`` and the argument as
``value``; arithmetic wraps modulo :math:`2^{256}`. The bug is stated as
a condition on a finished path: a recipient's balance grows while the
sender's does not shrink,

.. math::

   \mathrm{slot}_1 \ge s_1 \;\wedge\; \mathrm{slot}_2 > s_2 .

On the BeautyChain-style ``batch_transfer``, the solver finds
:math:`\mathrm{value} = 2^{255}`, the value of the April 2018 attack; with
the SafeMath check no input satisfies the condition.

.. GENERATED FROM PYTHON SOURCE LINES 27-33

.. code-block:: Python

    import matplotlib.pyplot as plt

    import blockchainkit as bk
    from blockchainkit.constants import WORD_MODULUS
    from blockchainkit.contracts.visualizers import plot_symbolic_paths








.. GENERATED FROM PYTHON SOURCE LINES 34-36

Explore the bytecode
--------------------

.. GENERATED FROM PYTHON SOURCE LINES 36-55

.. code-block:: Python


    bug = "slot1 >= s1 and slot2 > s2"
    reports = {}
    for checked in (False, True):
        program = bk.vm.batch_transfer(1, [2, 3], checked=checked)
        result = bk.contracts.symbolic_bytecode(program, arguments=("value",))
        witnesses = []
        for path in result.paths:
            if path.outcome == "stop":
                query = (*path.conditions, bk.contracts.expression(bug, **path.state))
                witness = bk.contracts.solve(query, modulus=WORD_MODULUS)
                if witness is not None:
                    witnesses.append(witness)
        reports[checked] = (result, witnesses)
        print(f"checked={checked}: {result.outcomes}, bug inputs {witnesses}")

    attack = reports[False][1][0]
    assert attack["value"] == 2**255 and not reports[True][1]





.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    checked=False: {'revert': 2, 'stop': 1}, bug inputs [{'s1': 0, 's2': 0, 'value': 57896044618658097711785492504343953926634992332820282019728792003956564819968}]
    checked=True: {'revert': 3, 'stop': 1}, bug inputs []




.. GENERATED FROM PYTHON SOURCE LINES 56-58

Confirm the witness concretely
------------------------------

.. GENERATED FROM PYTHON SOURCE LINES 58-73

.. code-block:: Python


    storage = {1: attack["s1"], 2: attack["s2"], 3: 0}
    run = bk.vm.execute(bk.vm.batch_transfer(1, [2, 3]), arguments=(attack["value"],), storage=storage)
    print(dict(run.storage))
    assert run.storage[2] == run.storage[3] == 2**255 and run.storage[1] == 0

    fig, (left, right) = plt.subplots(1, 2, figsize=(10, 4))
    plot_symbolic_paths(reports[False][0], ax=left)
    left.set_title("batch_transfer: 3 paths")
    plot_symbolic_paths(reports[True][0], ax=right)
    right.set_title("with the SafeMath check: 4 paths")
    fig.tight_layout()

    plt.show()




.. image-sg:: /api/gallery/contracts/verification/images/sphx_glr_plot_04_oyente_001.png
   :alt: batch_transfer: 3 paths, with the SafeMath check: 4 paths
   :srcset: /api/gallery/contracts/verification/images/sphx_glr_plot_04_oyente_001.png
   :class: sphx-glr-single-img


.. rst-class:: sphx-glr-script-out

 .. code-block:: none

    {1: 0, 2: 57896044618658097711785492504343953926634992332820282019728792003956564819968, 3: 57896044618658097711785492504343953926634992332820282019728792003956564819968}




.. GENERATED FROM PYTHON SOURCE LINES 74-80

Exercise
--------
With three recipients the overflowing ``value`` is no longer
:math:`2^{255}`, and the default candidates miss it. Find a value that
makes ``3 * value`` wrap to a small number, and pass it to ``solve``
through ``candidates``. A worked solution is in :doc:`/exercises/contracts`.


.. rst-class:: sphx-glr-timing

   **Total running time of the script:** (0 minutes 0.043 seconds)


.. _sphx_glr_download_api_gallery_contracts_verification_plot_04_oyente.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_04_oyente.ipynb
        :alt: Launch JupyterLite
        :width: 150 px

    .. container:: sphx-glr-download sphx-glr-download-jupyter

      :download:`Download Jupyter notebook: plot_04_oyente.ipynb <plot_04_oyente.ipynb>`

    .. container:: sphx-glr-download sphx-glr-download-python

      :download:`Download Python source code: plot_04_oyente.py <plot_04_oyente.py>`

    .. container:: sphx-glr-download sphx-glr-download-zip

      :download:`Download zipped: plot_04_oyente.zip <plot_04_oyente.zip>`


.. only:: html

 .. rst-class:: sphx-glr-signature

    `Gallery generated by Sphinx-Gallery <https://sphinx-gallery.github.io>`_