consensys / scribble-exercise-1 Goto Github PK

License: MIT License

Solidity 62.85% JavaScript 30.47% Makefile 6.69%

scribble-exercise-1's Introduction

Scribble Exercise 1

In this exercise we're going to have a look at a vulnerable ERC20 smart contract. We'll use Scribble to annotate it with properties, and use Mythril to automatically check the properties (and find bugs 🐛).

Handy Links

Scribble Repository -> https://github.com/ConsenSys/Scribble

Mythril Repository -> https://github.com/ConsenSys/Mythril

Scribble Docs 📚 -> https://docs.scribble.codes/

Installation


# Make sure to use node 10-16
npm install eth-scribble --global
npm install truffle --global
npm install ganache-cli --global

Setting up the target

mkdir exercise-1
cd exercise-1
truffle unbox ConsenSys/scribble-exercise-1

Finding the vulnerability

Have a look at the transfer() function:

function transfer(address _to, uint256 _value) external returns (bool) {
    address from = msg.sender;
    require(_value <= _balances[from]);

    uint256 newBalanceFrom = _balances[from] - _value;
    uint256 newBalanceTo = _balances[_to] + _value;
    _balances[from] = newBalanceFrom;
    _balances[_to] = newBalanceTo;

    emit Transfer(msg.sender, _to, _value);
    return true;
}

Adding annotations

Properties that make sense:

If the transfer function succeeds then the recipient had sufficient balance at the start

/// #if_succeeds {:msg "The sender has sufficient balance at the start"} old(_balances[msg.sender] <= _value)
function transfer(address _to, uint256 _value) external returns (bool) {
    ...
}

If the transfer succeeds then the sender will have `_value` subtracted from it’s balance (unless you transfer to yourself)

/// #if_succeeds {:msg "The sender has _value less balance"} msg.sender != _to ==> old(_balances[msg.sender]) - _value == _balances[msg.sender]; 
function transfer(address _to, uint256 _value) external returns (bool) {
    ...
}

If the transfer succeeds then the receiver will have `_value` added to it’s balance (unless you transfer to yourself)

/// #if_succeeds {:msg "The receiver receives _value"} msg.sender != _to ==> old(_balances[_to]) + _value == _balances[_to]; 
function transfer(address _to, uint256 _value) external returns (bool) {
    ...
}

If the transfer succeeds then the sum of the balances between the sender and receiver remains he same

/// #if_succeeds {:msg "Transfer does not modify the sum of balances" } old(_balances[_to]) + old(_balances[msg.sender]) == _balances[_to] + _balances[msg.sender];
function transfer(address _to, uint256 _value) external returns (bool) {
    ...
}

scribble-exercise-1's People

Contributors

Stargazers

Watchers

scribble-exercise-1's Issues

Issue installing mythril

Running it in venv to protect the rest of my setup:

(env) hackathon2021 % pip3 install mythril
Collecting mythril
  Downloading mythril-0.22.19.tar.gz (4.5 MB)
     |████████████████████████████████| 4.5 MB 2.9 MB/s
Collecting eth_abi==1.3.0
  Downloading eth_abi-1.3.0-py3-none-any.whl (21 kB)
Collecting eth-tester==0.1.0b32
  Downloading eth_tester-0.1.0b32-py3-none-any.whl (58 kB)
     |████████████████████████████████| 58 kB 12.1 MB/s
Collecting eth-utils==1.9.0
  Downloading eth_utils-1.9.0-py3-none-any.whl (24 kB)
Collecting numpy==1.19.0
  Downloading numpy-1.19.0.zip (7.3 MB)
     |████████████████████████████████| 7.3 MB 11.9 MB/s
  Installing build dependencies ... done
  Getting requirements to build wheel ... done
    Preparing wheel metadata ... done
Collecting py_ecc==1.6.0
  Downloading py_ecc-1.6.0-py3-none-any.whl (35 kB)
Collecting py-evm==0.3.0a13
  Downloading py_evm-0.3.0a13-py3-none-any.whl (230 kB)
     |████████████████████████████████| 230 kB 9.5 MB/s
Collecting py-solc-x==1.0.0
  Downloading py_solc_x-1.0.0-py3-none-any.whl (15 kB)
Collecting requests==2.25.0
  Downloading requests-2.25.0-py2.py3-none-any.whl (61 kB)
     |████████████████████████████████| 61 kB 10.8 MB/s
Collecting semantic_version==2.8.5
  Downloading semantic_version-2.8.5-py2.py3-none-any.whl (15 kB)
Collecting blake2b-py<0.2,>=0.1.2
  Downloading blake2b_py-0.1.4-cp39-cp39-macosx_10_7_x86_64.whl (146 kB)
     |████████████████████████████████| 146 kB 17.5 MB/s
Collecting cached-property<2,>=1.5.1
  Downloading cached_property-1.5.2-py2.py3-none-any.whl (7.6 kB)
Collecting certifi>=2020.06.20
  Downloading certifi-2020.12.5-py2.py3-none-any.whl (147 kB)
     |████████████████████████████████| 147 kB 18.9 MB/s
Collecting chardet<4,>=3.0.2
  Downloading chardet-3.0.4-py2.py3-none-any.whl (133 kB)
     |████████████████████████████████| 133 kB 13.4 MB/s
Collecting coloredlogs>=10.0
  Downloading coloredlogs-15.0-py2.py3-none-any.whl (45 kB)
     |████████████████████████████████| 45 kB 9.7 MB/s
Collecting configparser>=3.5.0
  Downloading configparser-5.0.2-py3-none-any.whl (19 kB)
Collecting cytoolz<1.0.0,>=0.8.2
  Downloading cytoolz-0.11.0.tar.gz (477 kB)
     |████████████████████████████████| 477 kB 8.5 MB/s
Collecting eth-account<=0.3.0,>=0.1.0a2
  Downloading eth_account-0.3.0-py3-none-any.whl (18 kB)
Collecting attrdict<3,>=2.0.0
  Downloading attrdict-2.0.1-py2.py3-none-any.whl (9.9 kB)
Collecting eth-bloom<2.0.0,>=1.0.3
  Downloading eth_bloom-1.0.4-py3-none-any.whl (5.4 kB)
Collecting eth-hash<0.3.0
  Downloading eth_hash-0.2.0-py3-none-any.whl (7.2 kB)
Collecting eth-hash[pycryptodome]
  Downloading eth_hash-0.3.1-py3-none-any.whl (8.9 kB)
INFO: pip is looking at multiple versions of eth-hash to determine which version is compatible with other requirements. This could take a while.
Collecting eth-hash<0.3.0
  Downloading eth_hash-0.1.4-py3-none-any.whl (10 kB)
  Downloading eth_hash-0.1.3-py3-none-any.whl (10 kB)
  Downloading eth_hash-0.1.2-py3-none-any.whl (10.0 kB)
  Downloading eth_hash-0.1.1-py3-none-any.whl (9.5 kB)
  Downloading eth_hash-0.1.0-py3-none-any.whl (8.5 kB)
INFO: pip is looking at multiple versions of eth-bloom to determine which version is compatible with other requirements. This could take a while.
Collecting eth-bloom<2.0.0,>=1.0.3
  Downloading eth_bloom-1.0.3-py3-none-any.whl (5.4 kB)
Collecting eth-keyfile>=0.5.1
  Downloading eth_keyfile-0.5.1-py3-none-any.whl (8.3 kB)
Collecting eth-keys<0.3.0,>=0.2.0b3
  Downloading eth_keys-0.2.4-py3-none-any.whl (24 kB)
Collecting eth-rlp>=0.1.0
  Downloading eth_rlp-0.2.1-py3-none-any.whl (5.0 kB)
Collecting eth-typing>=2.0.0
  Downloading eth_typing-2.2.2-py3-none-any.whl (6.2 kB)
Collecting ethereum>=2.3.2
  Downloading ethereum-2.3.2.tar.gz (155 kB)
     |████████████████████████████████| 155 kB 12.1 MB/s
Collecting coincurve>=7.0.0
  Downloading coincurve-15.0.0-cp39-cp39-macosx_10_14_x86_64.whl (372 kB)
     |████████████████████████████████| 372 kB 12.5 MB/s
Collecting cffi>=1.3.0
  Downloading cffi-1.14.5-cp39-cp39-macosx_10_9_x86_64.whl (177 kB)
     |████████████████████████████████| 177 kB 11.6 MB/s
Collecting ethereum-input-decoder>=0.2.2
  Downloading ethereum_input_decoder-0.2.2.tar.gz (5.5 kB)
Collecting hexbytes<1,>=0.1.0
  Downloading hexbytes-0.2.1-py3-none-any.whl (6.0 kB)
Collecting humanfriendly>=9.1
  Downloading humanfriendly-9.1-py2.py3-none-any.whl (86 kB)
     |████████████████████████████████| 86 kB 9.1 MB/s
Collecting idna<3,>=2.5
  Downloading idna-2.10-py2.py3-none-any.whl (58 kB)
     |████████████████████████████████| 58 kB 14.5 MB/s
Collecting jinja2>=2.9
  Using cached Jinja2-3.0.1-py3-none-any.whl (133 kB)
Collecting lru-dict>=1.1.6
  Downloading lru-dict-1.1.7.tar.gz (10 kB)
Collecting MarkupSafe>=2.0
  Downloading MarkupSafe-2.0.1-cp39-cp39-macosx_10_9_x86_64.whl (13 kB)
Collecting mypy-extensions>=0.4.1
  Downloading mypy_extensions-0.4.3-py2.py3-none-any.whl (4.5 kB)
Collecting parsimonious<0.9.0,>=0.8.0
  Downloading parsimonious-0.8.1.tar.gz (45 kB)
     |████████████████████████████████| 45 kB 8.8 MB/s
Collecting persistent>=4.2.0
  Downloading persistent-4.7.0-cp39-cp39-macosx_10_14_x86_64.whl (147 kB)
     |████████████████████████████████| 147 kB 9.2 MB/s
Collecting pycryptodome<4.0.0,>=3.4.7
  Downloading pycryptodome-3.10.1-cp35-abi3-macosx_10_9_x86_64.whl (1.5 MB)
     |████████████████████████████████| 1.5 MB 5.5 MB/s
Collecting pyethash<1.0.0,>=0.1.27
  Downloading pyethash-0.1.27.tar.gz (38 kB)
Collecting pysha3>=1.0.1
  Downloading pysha3-1.0.2.tar.gz (829 kB)
     |████████████████████████████████| 829 kB 12.2 MB/s
Collecting rlp<2.0.0,>=1.0.1
  Downloading rlp-1.2.0-py2.py3-none-any.whl (19 kB)
Collecting six
  Using cached six-1.16.0-py2.py3-none-any.whl (11 kB)
Collecting toolz>=0.8.0
  Downloading toolz-0.11.1-py3-none-any.whl (55 kB)
     |████████████████████████████████| 55 kB 6.8 MB/s
Collecting transaction>=2.2.1
  Downloading transaction-3.0.1-py2.py3-none-any.whl (47 kB)
     |████████████████████████████████| 47 kB 10.6 MB/s
Collecting trie<2.0.0,>=1.4.0
  Downloading trie-1.4.0-py3-none-any.whl (25 kB)
Collecting urllib3<1.27,>=1.21.1
  Downloading urllib3-1.26.4-py2.py3-none-any.whl (153 kB)
     |████████████████████████████████| 153 kB 20.1 MB/s
Collecting z3-solver>=4.8.8.0
  Downloading z3_solver-4.8.10.0-py2.py3-none-macosx_10_15_x86_64.whl (18.9 MB)
     |████████████████████████████████| 18.9 MB 10.7 MB/s
Collecting asn1crypto
  Downloading asn1crypto-1.4.0-py2.py3-none-any.whl (104 kB)
     |████████████████████████████████| 104 kB 14.5 MB/s
Collecting coverage
  Downloading coverage-5.5-cp39-cp39-macosx_10_9_x86_64.whl (207 kB)
     |████████████████████████████████| 207 kB 11.7 MB/s
Collecting eth-hash[pycryptodome]
  Downloading eth_hash-0.3.0-py3-none-any.whl (8.7 kB)
Collecting future
  Using cached future-0.18.2.tar.gz (829 kB)
Collecting matplotlib
  Downloading matplotlib-3.4.2-cp39-cp39-macosx_10_9_x86_64.whl (7.2 MB)
     |████████████████████████████████| 7.2 MB 4.3 MB/s
Collecting cycler>=0.10
  Downloading cycler-0.10.0-py2.py3-none-any.whl (6.5 kB)
Collecting kiwisolver>=1.0.1
  Downloading kiwisolver-1.3.1-cp39-cp39-macosx_10_9_x86_64.whl (61 kB)
     |████████████████████████████████| 61 kB 1.2 MB/s
Collecting pillow>=6.2.0
  Downloading Pillow-8.2.0-cp39-cp39-macosx_10_10_x86_64.whl (2.8 MB)
     |████████████████████████████████| 2.8 MB 12.3 MB/s
Collecting pyparsing>=2.2.1
  Using cached pyparsing-2.4.7-py2.py3-none-any.whl (67 kB)
Collecting python-dateutil>=2.7
  Downloading python_dateutil-2.8.1-py2.py3-none-any.whl (227 kB)
     |████████████████████████████████| 227 kB 21.3 MB/s
Collecting mock
  Downloading mock-4.0.3-py3-none-any.whl (28 kB)
Collecting pbkdf2
  Downloading pbkdf2-1.3.tar.gz (6.4 kB)
Collecting plyvel
  Downloading plyvel-1.3.0.tar.gz (149 kB)
     |████████████████████████████████| 149 kB 13.4 MB/s
Collecting py-flags
  Downloading py_flags-1.1.4-py3-none-any.whl (17 kB)
Collecting dictionaries==0.0.2
  Downloading dictionaries-0.0.2-py2.py3-none-any.whl (7.9 kB)
Collecting py-solc
  Downloading py_solc-3.2.0-py3-none-any.whl (12 kB)
Collecting pycparser
  Downloading pycparser-2.20-py2.py3-none-any.whl (112 kB)
     |████████████████████████████████| 112 kB 6.4 MB/s
Collecting pythx
  Downloading pythx-1.7.1-py2.py3-none-any.whl (41 kB)
     |████████████████████████████████| 41 kB 1.2 MB/s
Collecting inflection==0.5.1
  Downloading inflection-0.5.1-py2.py3-none-any.whl (9.5 kB)
Collecting mythx-models==2.0.1
  Downloading mythx_models-2.0.1-py2.py3-none-any.whl (41 kB)
     |████████████████████████████████| 41 kB 2.4 MB/s
Collecting jsonschema==3.2.0
  Downloading jsonschema-3.2.0-py2.py3-none-any.whl (56 kB)
     |████████████████████████████████| 56 kB 12.9 MB/s
Requirement already satisfied: setuptools in ./env/lib/python3.9/site-packages (from jsonschema==3.2.0->mythx-models==2.0.1->pythx->mythril) (51.1.1)
Collecting pydantic==1.7.3
  Downloading pydantic-1.7.3-cp39-cp39-macosx_10_9_x86_64.whl (2.4 MB)
     |████████████████████████████████| 2.4 MB 11.4 MB/s
Collecting PyJWT==1.7.1
  Downloading PyJWT-1.7.1-py2.py3-none-any.whl (18 kB)
Collecting attrs>=17.4.0
  Downloading attrs-21.2.0-py2.py3-none-any.whl (53 kB)
     |████████████████████████████████| 53 kB 3.2 MB/s
Collecting pyrsistent>=0.14.0
  Downloading pyrsistent-0.17.3.tar.gz (106 kB)
     |████████████████████████████████| 106 kB 12.3 MB/s
Collecting PyYAML
  Using cached PyYAML-5.4.1-cp39-cp39-macosx_10_9_x86_64.whl (259 kB)
Collecting repoze.lru
  Downloading repoze.lru-0.7-py3-none-any.whl (10 kB)
Collecting scrypt
  Downloading scrypt-0.8.18.tar.gz (56 kB)
     |████████████████████████████████| 56 kB 9.8 MB/s
Collecting zope.interface
  Downloading zope.interface-5.4.0-cp39-cp39-macosx_10_14_x86_64.whl (208 kB)
     |████████████████████████████████| 208 kB 10.8 MB/s
Using legacy 'setup.py install' for mythril, since package 'wheel' is not installed.
Using legacy 'setup.py install' for cytoolz, since package 'wheel' is not installed.
Using legacy 'setup.py install' for ethereum, since package 'wheel' is not installed.
Using legacy 'setup.py install' for ethereum-input-decoder, since package 'wheel' is not installed.
Using legacy 'setup.py install' for lru-dict, since package 'wheel' is not installed.
Using legacy 'setup.py install' for parsimonious, since package 'wheel' is not installed.
Using legacy 'setup.py install' for pyethash, since package 'wheel' is not installed.
Using legacy 'setup.py install' for pysha3, since package 'wheel' is not installed.
Using legacy 'setup.py install' for future, since package 'wheel' is not installed.
Using legacy 'setup.py install' for pbkdf2, since package 'wheel' is not installed.
Using legacy 'setup.py install' for plyvel, since package 'wheel' is not installed.
Using legacy 'setup.py install' for pyrsistent, since package 'wheel' is not installed.
Using legacy 'setup.py install' for scrypt, since package 'wheel' is not installed.
Building wheels for collected packages: numpy
  Building wheel for numpy (PEP 517) ... done
  Created wheel for numpy: filename=numpy-1.19.0-cp39-cp39-macosx_11_0_x86_64.whl size=4599385 sha256=94274876074fbcc9fbd3ec3e8a634c020556c85a6ff4ae9cd431ef9573ec440b
  Stored in directory: /Users/nicolas/Library/Caches/pip/wheels/d2/d9/5e/6ce8602ab8be91874fa00a1286a82f4430d7b0f9daece5fa3e
Successfully built numpy
Installing collected packages: toolz, eth-typing, eth-hash, cytoolz, six, pyrsistent, pycryptodome, pycparser, eth-utils, attrs, urllib3, rlp, python-dateutil, pydantic, parsimonious, mypy-extensions, jsonschema, inflection, idna, hexbytes, eth-keys, chardet, cffi, certifi, asn1crypto, zope.interface, trie, semantic-version, scrypt, requests, repoze.lru, PyYAML, pysha3, pyparsing, PyJWT, pyethash, py-ecc, pillow, pbkdf2, numpy, mythx-models, MarkupSafe, lru-dict, kiwisolver, humanfriendly, future, eth-rlp, eth-keyfile, eth-bloom, eth-abi, dictionaries, cycler, coincurve, cached-property, blake2b-py, attrdict, z3-solver, transaction, pythx, py-solc-x, py-solc, py-flags, py-evm, plyvel, persistent, mock, matplotlib, jinja2, ethereum-input-decoder, ethereum, eth-tester, eth-account, coverage, configparser, coloredlogs, mythril
    Running setup.py install for cytoolz ... done
    Running setup.py install for pyrsistent ... done
    Running setup.py install for parsimonious ... done
    Running setup.py install for scrypt ... done
    Running setup.py install for pysha3 ... done
    Running setup.py install for pyethash ... done
    Running setup.py install for pbkdf2 ... done
    Running setup.py install for lru-dict ... done
    Running setup.py install for future ... done
    Running setup.py install for plyvel ... error
    ERROR: Command errored out with exit status 1:
     command: /Users/nicolas/Develop/hackathon2021/env/bin/python3 -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-install-50gl3fqe/plyvel_185033656d3a4afdb3000e03cfa7ec91/setup.py'"'"'; __file__='"'"'/private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-install-50gl3fqe/plyvel_185033656d3a4afdb3000e03cfa7ec91/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-record-i3dk_qfm/install-record.txt --single-version-externally-managed --compile --install-headers /Users/nicolas/Develop/hackathon2021/env/include/site/python3.9/plyvel
         cwd: /private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-install-50gl3fqe/plyvel_185033656d3a4afdb3000e03cfa7ec91/
    Complete output (18 lines):
    running install
    running build
    running build_py
    creating build
    creating build/lib.macosx-11-x86_64-3.9
    creating build/lib.macosx-11-x86_64-3.9/plyvel
    copying plyvel/_version.py -> build/lib.macosx-11-x86_64-3.9/plyvel
    copying plyvel/__init__.py -> build/lib.macosx-11-x86_64-3.9/plyvel
    running build_ext
    building 'plyvel._plyvel' extension
    creating build/temp.macosx-11-x86_64-3.9
    creating build/temp.macosx-11-x86_64-3.9/plyvel
    clang -Wno-unused-result -Wsign-compare -Wunreachable-code -fno-common -dynamic -DNDEBUG -g -fwrapv -O3 -Wall -I/usr/local/include -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk -I/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include -I/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/System/Library/Frameworks/Tk.framework/Versions/8.5/Headers -I/usr/local/include -I/usr/local/opt/[email protected]/include -I/usr/local/opt/sqlite/include -I/Users/nicolas/Develop/hackathon2021/env/include -I/usr/local/Cellar/[email protected]/3.9.1_5/Frameworks/Python.framework/Versions/3.9/include/python3.9 -c plyvel/_plyvel.cpp -o build/temp.macosx-11-x86_64-3.9/plyvel/_plyvel.o -Wall -g -x c++ -std=c++11 -stdlib=libc++
    plyvel/_plyvel.cpp:632:10: fatal error: 'leveldb/db.h' file not found
    #include "leveldb/db.h"
             ^~~~~~~~~~~~~~
    1 error generated.
    error: command '/usr/bin/clang' failed with exit code 1
    ----------------------------------------
ERROR: Command errored out with exit status 1: /Users/nicolas/Develop/hackathon2021/env/bin/python3 -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-install-50gl3fqe/plyvel_185033656d3a4afdb3000e03cfa7ec91/setup.py'"'"'; __file__='"'"'/private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-install-50gl3fqe/plyvel_185033656d3a4afdb3000e03cfa7ec91/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /private/var/folders/zt/z7k8lh1511lgqnzx_cvt5bww0000gn/T/pip-record-i3dk_qfm/install-record.txt --single-version-externally-managed --compile --install-headers /Users/nicolas/Develop/hackathon2021/env/include/site/python3.9/plyvel Check the logs for full command output.

Missing a gitignore file

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.