Learning goals:

Gain an…

• Ability to run and configure a real symbolic execution engine to find bugs in smart contracts.
• Understanding of the benefits and utility of a symbolic execution tool.
• Understanding of the limitations of Mythril and an understanding of the limitations of a symbolic execution tool.

Suggested Academic Readings:

1. Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
2. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs

Resources:

• https://github.com/ConsenSys/mythril

Setup:

1. Download the development environment and benchmark set:

hw4.zip

Instructions:

In this homework, you will run the fuzzer Mythril on a bug benchmark of 8 programs. 6 of these were the ethernaut programs from HW2.

1. Level 1: Fallback
2. Level 2: Fal1out
3. Level 4: Telephone