In this tutorial we will learn how to:
start using scribble
add a custom property to an ERC20 token contract
look for violations of our custom property with MythX
Without further ado...
Make sure that you have the following installed:
python3 and pip3
nodejs version 12.x and npm.
To get setup you first need to install scribble:
npm install -g eth-scribble
Next install mythx-cli:
pip3 install -U mythx-cli
Next you will need a MythX account. If you don't already have one, you can make a MythX account here.
Once you have an account you will need an API Key to authenticate to the mythx service. You can generate one by logging into the MythX dashboard, clicking on the "API Key" menu entry and filling out the password field. (detailed instructions here). After you get your key, you can set it as the MYTHX_API_KEY
environment variable:
export MYTHX_API_KEY=<your API KEY>
Now we are ready to begin!
Before we begin, we should clarify what we mean by 'custom properties'. Custom properties in general can be any predicate you have in mind about your code. For example, a custom property can be:
Only the current owner of the contract may change the owner
state variable
My contract will allow trades only after the initialize()
function was called
The number of minted tokens only increases
etc..
In order to be able to reason about these properties formally however, we need to translate their English statements into a formal language that automated tools understand. We will show how to do this using the Scribble spec language. Note that the language choice imposes certain limitations on what can be expressed. We are actively working on adding more expressive power to Scribble.
For this tutorial we will consider a simple ERC20 token, and annotate it with a custom property expressed in the Scribble language. Take the below code and save it as Token.sol
in a directory of your choice:
Token.sol
pragma solidity ^0.6.0;βcontract ERC20 {uint256 private _totalSupply;mapping (address => uint256) private _balances;mapping (address => mapping (address => uint256)) private _allowances;βconstructor() public {_totalSupply = 1000000;_balances[msg.sender] = 1000000;}βfunction totalSupply() external view returns (uint256) {return _totalSupply;}βfunction balanceOf(address _owner) external view returns (uint256) {return _balances[_owner];}βfunction allowance(address _owner, address _spender) external view returns (uint256) {return _allowances[_owner][_spender];}β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;}βfunction approve(address _spender, uint256 _value) external returns (bool) {address owner = msg.sender;_allowances[owner][_spender] = _value;emit Approval(owner, _spender, _value);return true;}βfunction transferFrom(address _from, address _to, uint256 _value) external returns (bool) {uint256 allowed = _allowances[_from][msg.sender];require(_value <= allowed);require(_value <= _balances[_from]);_balances[_from] -= _value;_balances[_to] += _value;_allowances[_from][msg.sender] -= _value;emit Transfer(_from, _to, _value);return true;}βevent Transfer(address indexed _from, address indexed _to, uint256 _value);event Approval(address indexed _owner, address indexed _spender, uint256 _value);}
Lets consider the transfer
function above.
There are several properties that could be specified over the transfer function:
If the transfer function succeeds then the recipient had sufficient balance at the start
If the transfer succeeds then the sender will have `_value` subtracted from itβs balance
If the transfer succeeds then the receiver will have `_value` added to itβs balance
If the transfer succeeds then the sum of the balances between the sender and receiver remains he same
For this example weβll go with property #4;
π‘ Try to write annotations for the other two properties after youβve finished this getting started guide!
Formalizing the property
First things first, we need to dissect what the property actually entails. There are two main parts: if the transfer succeeds
and the sum of the sender and receiver balances is the same before and after the transaction
.
if the transfer succeeds
This specifies when you expect something to hold. In the scribble specification language we use if_succeeds
function annotations to check properties after successful termination of a function. Check out the specification docs for detailed information on the if_succeeds
keyword.
the sum of the sender and receiver balances is the same before and after the transaction
This is the boolean expression that we expect to hold. Note that this property introduces a statement that relates the initial and final state of the contract. That is, we want to know that the sum of the balances (_balances[sender] + _balances[receiver]
) doesnβt change relative to the state before the transaction. To allow you to express such properties the old()
is used. Check out the specification docs for more information on old
.
Using this keyword we can formulate the following expression:
old(_balances[_to]) + old(_balances[msg.sender]) == _balances[_to] + _balances[msg.sender]
Now we can combine the two to get to our specification:
if_succeeds {:msg "Transfer does not modify the sum of balances" } old(_balances[_to]) + old(_balances[msg.sender]) == _balances[_to] + _balances[msg.sender];
Adding the annotation
if_succeeds
annotations are function specifications, which in the Scribble specification language are placed above the function definitions using a docstring comment.
pragma solidity ^0.6.0;βcontract ERC20 {mapping (address => uint256) private _balances;/// 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) public returns (bool) {...}}
To see if the property holds we will move to the terminal, and use the MythX CLI to start fuzzing and symbolic exploration.
In the directory with the annotated contract, run:
# The mythx analyze command can use Scribble to interpret the annotations, and send the instrumented code to the MythX API for analysis$ mythx analyze --scribble Token.solFound 1 job(s). Submit? [y/N]: y[####################################] 100%
β Relax for 2 minutes as the MythX robots do their work!
After about 2 minutes we get the following results:
Report for flattened.solhttps://dashboard.mythx.io/#/console/analyses/1de3dc57-7db3-4d69-9e10-0df745753676ββββββββββ€βββββββββββββββββββββββββββββ€βββββββββββββ€βββββββββββββββββββββββββββββββββββββββββ Line β SWC Title β Severity β Short Description βββββββββββͺβββββββββββββββββββββββββββββͺβββββββββββββͺββββββββββββββββββββββββββββββββββββββββ‘β 40 β (SWC-110) Assert Violation β Low β A user-provided assertion failed. βββββββββββΌβββββββββββββββββββββββββββββΌβββββββββββββΌββββββββββββββββββββββββββββββββββββββββ€β 41 β (SWC-110) Assert Violation β Low β An assertion violation was triggered. βββββββββββ§βββββββββββββββββββββββββββββ§βββββββββββββ§ββββββββββββββββββββββββββββββββββββββββ
The command you just ran actually did several steps. First mythx-cli
invoked scribble
to generate an instrumented version of the contract. That is, a version of the original contract with the mostly the same behavior, except it also converted the property you had in the docstring into a concrete check at the end of transfer
. For more information on how instrumentation works check out this section. If you want to see the instrumented code, you can run
$ scribble Token.sol
π Read Specification Language Docs to learn more about the specification language
π Check out the repository of examples