• Preparation
  • Installing Truffle 5 Prototype
  • Installing GuardRails Alpha
  • Installing Mythril Classic
• Part 1 - The Smart Contract Secure SDLC
• Part 2 - Threat Modeling
• Part 3 - Reentrancy
• Part 4 - The Real Fun Begins
  • Exercise 1 - Truffle Analyze
  • Exercise 2 - Cheating on CTFs with Mythril Classic
  • Exercise 3 - Continuous Integration with Github Projects
  • Exercise 4 - Hacking Contracts on the Mainnet
  • Exercise 5 - Verifying Invariants Using Asserts
  • Exercise 6 - The Final Challenge
• What to Do Next
• Credit

Here's how to get set up for the workshop. It should be super easy except if you're using Windows.

First, you need a web3 capable browser and some testnet ETH. You probably also have both, but if not, get Metamask and grab some ETH from the Ropsten faucets:

• https://faucet.metamask.io/
• https://faucet.ropsten.be/

The workshop exercises are hosted in an separate repo. Get a local copy by cloning the repo:

$ git clone https://github.com/ConsenSys/devcon4-playground/

In this workshop you'll get a sneak peek into the future: We'll be using Mythril Platform prototypes we built together with the Truffle and Guardrails guys, as well as the latest build of Mythril Classic, which was we created just in time for DevCon4 under extreme stress (in most countries such work conditions would be illegal, that's why so many of our devs live in South East Asia).

If you run into insurmountable problems ask the instructors for help. There's also a dedicated Discord channel that we created exclusively for you, the valued workshop participant. Some of our core devs will be on standby to fix bugs in realtime.

Note that this is all super-experimental stuff! The Mythril Platform beta isn't even starting before December. Monitor the #announcements channel on Discord for updates.

Truffle Suite is a popular development framework for Ethereum. For this workshop we'll install a prototype with Mythril Platform integration. Run the following command to install it:

$ npm install -g truffle-plus-analyze
$ truffle+analyze --help
Truffle+Analyze v5.0.0-beta.1g - a development framework for Ethereum

Usage: truffle+analyze <command> [options]

Commands:
(...)
  analyze   Run Mythril Platform analyses on a contract
(...)

Don't worry if you already have Truffle installed - installing the experimental build will not affect your existing installation. You'll get a separate binary called truffle+analyze that you uninstall later without breaking anything.

You'll also need a Mythril Platform alpha key to use the truffle analyze command. In this workshop we'll use a shared temporary API key. To set it up, change into the devcon4-playground directory and run the setup script:

$ cd devcon4-playground
$ source mythril-staging
Congratulations! You are now set up to use the Mythril Platform staging server.

Note that this API key will only work for a couple of days. The official beta launch is still a few weeks away, but contact us on Discord if you want access.

(we'll go through this process in the workshop)

Guardrails is a Github app that hooks into the development workflow and reports security issues on pull requests. To try out Guardrails, fork the devcon4-playground repository using the "Fork" button on the top right. Then, install the Guardrails Github app and point it to your copy of the devcon4-playground repo.

Mythril uses solc to compile Solidity files, so you'll need to install that as well.

Mythril Classic is a command-line tool for advanced users. It can do a lot of stuff, such as analyzing contracts on the blockchain, creating control flow graphs, searching the Ethereum state trie and auto-generating transaction sequences to trigger bugs (plus you can use it to cheat in CTFs).

You can install the latest version from Pypi or Dockerhub (instructions in the Mythril Classic Wiki. Make sure you have version 0.19.3 installed.

Installing from Pypi

$ pip3 install mythril
$ myth --version
Mythril version v0.19.3

Installing from DockerHub

$ docker pull mythril/myth
$ docker run mythril/myth --version
Mythril version v0.19.3

In part 1, Tom Lindeman explains secure SDLC processes. He's not a coder like the rest of us, so please be gentle and don't ask him any hard technical questions.

TL;DR: Security should be incorporated during all phases of development. This info graphic sums things up nicely:

Before and during buidling a smart contract system you should think about potential threats and countermeasures. This process is known as threat modeling. In part 2, Gerhard Wagner introduces threat modeling basics. Here's the workshop material:

• Presentation slides
• Blockchain incident threat list

Threat Modeling Exercise:

After all this theory it's time for some hands-on action. Pick one of the following options:

• Build a threat model for your own smart contract system
• Build a threat model for Crypto Froggies

The infamous TheDAO was exploited by reentrancy in 2016. Although the community is more aware of it, reentrancy struck back in October 2018. Joseph Chow will show patterns and warnings signals to watch out for, and how best practices can help defend against reentrancy. This will also help with one of the exercises in Part 4.

• Presentation slides [Google], [PDF]

For the remainder of the workshop we'll be looking at different ways of identifying, fixing, exploiting and preventing vulnerabilities during development.

In exercise 1 we'll give a sneak peek of the truffle analyze command, an upcoming feature of Truffle Suite. Let's see if Truffle can spot the security bug and think about ways to fix it.

To run truffle analyze, first change into the project directory for exercise 1.

$ cd devcon4-playground/exercise1
$ truffle+analyze analyze

If you get an error message saying "You need to set environment variable MYTHRIL_API_KEY to run analyze", re-run the setup script which as described above.

The results you get from truffle analyze should look similar to this:

0:0   error  Contracts should be deployed with the same compiler version and flags that they have been tested with  SWC-103
20:4  error  The arithmetic operation can result in integer overflow   SWC-101
(...)

Note the "SWC" identifier at the end: That's a reference to the Smart Contract Weakness Classification (EIP 1470). You can look up details about each issue there.

Now things will get serious! We'll take the attacker's side and exploit this exact contract. Depending on your level of skill, pick one of the following:

• Easy: Token
• A bit more difficult: TokenWhale.

Mythril Classic has a few extra tricks up its sleeve. In the second exercise, we'll look at a the Tokensale contract from CaptureTheEther. The source code of that contract is in the exercise2 directory. The question is, does it have any vulnerabilities? Let's do a quick Mythril Classic run to find out:

$ myth -x exercise2/contracts/Tokensale.sol (Pypi)

$ docker run -v $(pwd)/exercise2/contracts:/contracts mythril/myth -x /contracts/Tokensale.sol (Docker)

Looks like another integer-related bug! Let's now think about how to best exploit this issue. What we want is to get a lot of tokens without paying a single ETH. A nice trick is to express the exact opposite of what we want as an invariant using an assert() statement and letting Mythril do the work of finding the solution.

Create a copy of Tokensale.sol called Tokensale-cheat.sol and add an assertion to the function buy as follows:

    function buy(uint256 numTokens) public payable {

        require(msg.value == numTokens * PRICE_PER_TOKEN);

        assert(!(msg.value == 0 && numTokens > 0));

This essentially means "it should never happen that numTokens is greater than zero if msg.value (the amount of Ether sent) is zero". Obviously, as the attacker that's precisely what we want to happen. By adding the --verbose-report flag, Mythril will give you the transaction data needed to violate the assertion.

$ myth -mexceptions -x exercise2/contracts/Tokensale-cheat.sol --verbose-report (Pypi)

$ docker run -v $(pwd)/exercise2/contracts:/contracts mythril/myth -mexceptions -x /contracts/Tokensale-cheat.sol --verbose-report (Docker)

Can you tell why "calldata" in Mythril's output has that particular value?

With the right calldata, you should now able to solve the Tokensale challenge.

Part 1 - Hack

We are going to hack $$$ the Etherbank in exercise 3. Prefund Etherbank with 10 Ether and start hacking. You have solved the challenge when Etherbank is empty, call challengeSolved() to check if you are done. Deploying contracts to the test net and exploiting it there is more fun but it can also be slow to send transactions to the Ropsten test net. For that reason we recommend to deploy and solve the challenge in Remix. If you want to take the risk go ahead and try the CapturetheEther challenge instead.

Part 2 - Defend

Ideally we want to know when vulnerabilities are introduced into the code base before they end up in the master branch. In exercise 3, we'll try the Guardrails Github app (Make sure to allow Issues in the repository settings as Guardrails will create issues), which should help you detect the issue. It's on you to fix it. Clone the devcon4-playground repository and create a new PR to resolve the issue that we exploited in Part 1.

Mythril Classic can analyze smart contracts from many sources, including bytecode on the blockchain. In exercise 4, we'll identify another type of vulnerability that has often been exploited in the past. We'll then show how to detect vulnerable contracts on the mainnet and auto-generate an exploit that extracts the kills the vulnerable contract.

An important aspect is the number of transactions that Mythril (symbolically) executes. The default number is 1, but you can increase it for a more in-depth analysis (note that this increases analysis time significantly). By setting max transactions to 2, you will also detect bugs that are two transactions "deep".

For this example, let's set the max transaction count to 2:

$ myth -x exercise4/contracts/Ownable.sol --max-transaction-count 2 --verbose-report (Pypi)

$ docker run -v $(pwd)/exercise4/contracts:/contracts mythril/myth -x /contracts/Ownable.sol --max-transaction-count 2 --verbose-report (Docker)

Again, the --verbose-report will give you the transaction sequence for triggering the bug - take a good look at the output!

Now the real fun starts: We'll deploy a real-world contract instance with a similar vulnerability. Whoever exploits it first is not only awesome, but also wins 0.1337 ETH for buying Pizza (or hodl). Tip: You can run Mythril Classic against an on-chain contract using the -a flag.

Tip: Use myth -xia <address> run Mythril against mainnet contracts using INFURA, and don't forget what you learned above :)

The Solidity assert() statement is used to specify conditions that are expected to always hold. If you want to prove certain assumptions about your code, you can put them into asserts and use Mythril's symbolic execution engine to do all the hard work for you.

Mythril Classic will detect reachable exceptions by default. To only search for exceptions, add the -mexceptions option.

$ myth -mexceptions -x <Solidity file>

In exercise 5, we'll write a test to (dis-)prove an invariant in a token contract. The token code sample was shown by Josselin Feist on TruffleCon 2018 (shouts to our friends from Trail of Bits).

The invariant we want to verify is that a user's balance can never exceed 1,000. A nice way to do this is to create a separate test contract that inherits from the contract to be tested. Create a new file named token-with-backdoor-test.sol in the exercise5 directory and add a function containing the assertion that balances[msg.sender] must never exceed 1,000:

import "./token-with-backdoor.sol";

contract TokenTest is Token {

    // Verify that the user's balance can never exceed 1000

    function verify_balance() {
        assert(balances[msg.sender] <= 1000);
    }

}

Now we should be ready to go! Run Mythril Classic against the newly created file:

$ myth -mexceptions -x exercise5/token-with-backdoor-test.sol --max-transaction-count 3 --verbose-report (Pypi)

$ docker run -v $(pwd)/exercise5:/exercise5 mythril/myth -mexceptions -x /exercise5/token-with-backdoor-test.sol --max-transaction-count 3 --verbose-report (Docker)

As you can see, in this case three transactions need to be sent in the correct order to violate the invariant. Again, it is useful to have a close look at Mythril's output and match it to the functions in the contract.

As a fully certified Mythril expert, you are now capable of solving a more difficult CTF challenge. This challenge is worth another 0.1337 MYTH. This time there won't be any hints ;)

A great way to continue learning is playing challenges like Capture the Ether, Security Innovation CTF and Ethernaut.

If you're into buidling Ethereum security tooling, the Mythril team is probably not a good place for you. Because in our team, you get near-complete freedom to work on what you like on your own time, plus the resources you need to bring complex ideas life. That sucks, because most tool buidlers see their tools as side projects to work on in-between audits or on weekends. But if you, against all odds, do want to fully focus on building awesome technology that helps the ecosystem, you can always ping us on Discord.

Created by ConsenSys Diligence and the Mythril team. Special thanks to Mick Ayzenberg (Security Innovation), Trail of Bits, Steve Marx of CaptureTheEther and ConsenSys fame and Zeppelin Solutions for vulnerable contract samples and challenges. Also, kudos to the Truffle and Guardrails teams for working with us on Mythril Platform integration.