Index
b'# Scribble Exercise 1\n\nIn this exercise we\'re going to have a look at a vulnerable ERC20 smart contract. \nWe\'ll use Scribble to annotate it with properties, and use Mythril to automatically check the properties (and find bugs \xf0\x9f\x90\x9b).\n\n### Handy Links\nScribble Repository -> https://github.com/ConsenSys/Scribble\n\nMythril Repository -> https://github.com/ConsenSys/Mythril\n\nScribble Docs \xf0\x9f\x93\x9a -> https://docs.scribble.codes/\n\n### Installation\n```\n# We\'ll use Mythril to automatically test specifications\npip3 install mythril\n\n# Make sure to use node 10-12\nnpm install eth-scribble --global\nnpm install truffle --global\nnpm install ganache-cli --global\n```\n\n### Setting up the target\n\n```\nmkdir exercise-1\ncd exercise-1\ntruffle unbox ConsenSys/scribble-exercise-1\n```\n\n\n### Finding the vulnerability\nHave a look at the `transfer()` function:\n```\nfunction transfer(address _to, uint256 _value) external returns (bool) {\n address from = msg.sender;\n require(_value <= _balances[from]);\n\n uint256 newBalanceFrom = _balances[from] - _value;\n uint256 newBalanceTo = _balances[_to] + _value;\n _balances[from] = newBalanceFrom;\n _balances[_to] = newBalanceTo;\n\n emit Transfer(msg.sender, _to, _value);\n return true;\n}\n```\n\n### Adding annotations\nProperties that make sense:\n If the transfer function succeeds then the recipient had sufficient balance at the start
\n
\n\n/// #if_succeeds {:msg "The sender has sufficient balance at the start"} old(_balances[msg.sender] <= _value)\nfunction transfer(address _to, uint256 _value) external returns (bool) {\n ...\n}\n\n If the transfer succeeds then the sender will have `_value` subtracted from it\xe2\x80\x99s balance (unless you transfer to yourself)
\n
\n\n/// #if_succeeds {:msg "The sender has _value less balance"} msg.sender != _to ==> old(_balances[msg.sender]) - _value == _balances[msg.sender]; \nfunction transfer(address _to, uint256 _value) external returns (bool) {\n ...\n}\n\n If the transfer succeeds then the receiver will have `_value` added to it\xe2\x80\x99s balance (unless you transfer to yourself)
\n
\n\n/// #if_succeeds {:msg "The receiver receives _value"} msg.sender != _to ==> old(_balances[_to]) + _value == _balances[_to]; \nfunction transfer(address _to, uint256 _value) external returns (bool) {\n ...\n}\n\n If the transfer succeeds then the sum of the balances between the sender and receiver remains he same
\n
\n\n/// #if_succeeds {:msg "Transfer does not modify the sum of balances" } old(_balances[_to]) + old(_balances[msg.sender]) == _balances[_to] + _balances[msg.sender];\nfunction transfer(address _to, uint256 _value) external returns (bool) {\n ...\n}\n\n