MythX Tech: Behind the Scenes of Smart Contract Security Analysis
The tech behind MythX smart contract analysis, including the microservices Maru, Harvey, and Mythril, and how they work together.
When I first introduced Mythril in 2017, I didn’t expect it to be very useful to smart contract developers. It was a simple symbolic analyzer for Ethereum bytecode with tacked-on Solidity support. Mythril was OK for detecting some security issues and solving CTFs, but it wasn’t written with the needs of developers in mind.
As soon as you want to use Mythril, or any other open source smart contract security tool for that matter, on an actual real-world project, things fall apart very quickly. Mythril takes ages to install and has 30+ command line flags. Running it consumes a lot of computing power. It reports only a limited subset of what’s in the SWC Registry. It doesn’t integrate well with development tools. And most frustratingly, when dealing with large projects, something always breaks. TL;DR: Mythril sucks for developers.
Yet, there seemed to be demand for a tool like Mythril and people actually started using it, building it into their own software, and posting hundreds of issues on Github. As of today, Mythril has been downloaded 470,000 times.
It was always clear to me that whatever we did, Mythril-the-Python-tool could never reach the usability and reliability required to be truly helpful to smart contract developers in their day-to-day job. Then, in early 2018, the “INFURA of smart contract security idea” lightbulb went on: What if one could submit your contracts to a simple API and get back a a security analysis report? Voilà, MythX was born (well actually, Mythril Platform was born, but that had to be renamed due to legal threats from the Tolkien troll army).
The MythX project started in early 2018 with funding from Consensys and two developers. Since then, the MythX team has grown to 18 heads and we have built a lot of awesome tech to pack into our security analysis engine. We also built an API that’s scalable and won’t break down even when people throw gigantic Truffle projects at it (I’m looking at you Aragon).
Our mission statement was to provide comprehensive smart contract security analysis at the click of a button.
MythX is supposed to be the iOS to Mythril’s Android. It sounded easy enough at the time. But as it turned out, creating something that works under lab conditions was a completely different ballgame than creating a production-grade API that that always works™. That said, I’m happy to announce that we have achieved the goal. If you have a Solidity file at hand you can try it right now. Fire up Remix, activate the MythX extension, and copy/paste your code into the editor. Hit the “analyse” button to run a generic vulnerability scan. After a couple of minutes the scan results should be shown in the MythX tab.
MythX does not only detect most known bug types automatically. You can also use MythX’s fuzzing and symbolic execution engines to check custom properties and verify the correctness of your smart contracts. MythX supports both Solidity assert and the custom AssertionFailed event.
MythX Security Analysis
When you submit an analysis job to MythX, a lot of things happen. First, the MythX client submits compiler artefacts, including bytecode, source maps, and the source code itself to the analysis service. The MythX service then passes those inputs on to several micro-services that perform different types of analysis. It then evaluates and combines the results and composes a response describing the security issues detected as well as their precise locations in the code. The tools assembly bears resemblance to a well-coordinated superhero team such as the Avengers. Let’s have look at the main heroes.
Static code analysis — Maru
Our static analysis tool, Maru, takes the Solidity AST as input. It translates the code to an intermediate representation and performs static security checks. This type of analysis is very fast, but the results are less reliable than the results of more costly analysis types. Some of Maru’s results are converted into vulnerability reports, while others are used to augment and improve the results of fuzzing and symbolic execution.
An interesting feature we’re currently adding to Maru is support for a specification language codenamed “Scribble”. MythX users will be able to add custom properties as Solidity comments and Maru will instrument the byte code so the properties can be checked by the MythX engine.
Maru was initially built Gerhard Wagner and is now mainly developed by Dimitar Bounov and Pavel Zverev. It will be open-sourced sometime in 2020.
Greybox Fuzzing — Harvey
Fuzzing is an automated software testing technique that involves providing invalid, unexpected, or random data as inputs to a computer program.
Harvey is a greybox-fuzzer that uses light-weight program instrumentation to record the execution path for each tested input and compute its path identifier. The approach was developed by Valentin Wüstholz and Maria Christakis and published in an 2018 paper (Valentin joined the MythX team mid-2018).
Harvey is capable of rapidly reaching high code coverage even for complex code without using more expensive techniques, such as automated solvers, to reason about the program. Valentin has written extensively about Harvey, so if you’re interested in the nitty-gritty details check out the references below.
Further reading for Harvey:
- Learning Inputs in Greybox Fuzzing (Arxiv)
- Finding Vulnerabilities in Smart Contracts
- Fuzzing Smart Contracts Using Input Prediction
Symbolic Execution and SMT Solving — Mythril
Mythril uses symbolic execution to detect vulnerabilities. With this approach, program inputs are assumed to be symbols that represent arbitrary input values. An EVM interpreter written in Python keeps track of the program states it encounters and collects constraints on inputs from predicates encountered in branch instructions. Every execution path discovered can be expressed as propositional formula. The resulting representation of program states and control flow can be used to prove certain properties of the program, determine reachability of error states, and perform various types of security analysis.
The Mythril of today is a wholly different beast than the Mythril I presented 2 years ago. Its symbolic execution engine has been completely refactored. It now performs highly optimized multi-transactional analysis and improved taint analysis. Mythril’s EVM implementation passes the Ethereum VM tests. Credit for this goes to MythX team members Joran Honig, Nikhil Parasaram and Nathan Peercy.
Further reading for Mythril:
Correlation and Inter-Tool Communication
So we have three tools running in parallel, job well done, let’s pack up and go home right? Wrong. Another challenge is matching and correlating the tool results, as well as decoding the tool outputs to a form that is easy to understand for the user. All this work is done in the post-processing components: They double-check the results, remove duplicated and false positives, and decode the test cases returned by the tools to a user-readable format.
The most interesting possibilities open up by letting the tools “talk” to each other. For example, the static analyser can pre-determine the locations of interesting arithmetic operations or exclude uninteresting paths from dynamic analysis altogether. To facilitate this all Mythx tools adhere to a common JSON protocol. Orchestration and post-processing are mainly developed by Dominik Muhs and Joran Honig.
What We’re Working on Next
In our industry, resting on one’s laurels is not a very good idea. We’re therefore working on countless research projects, including:
- Specification language. The Scribble specification language will enable users to annotate Solidity code with security properties that can be checked using MythX.
- eWASM support. Because eWASM is coming soon (lol), we have built a symbolic execution engine for WASM and are keeping a close eye on eWASM development;
- Various performance improvements such as function summaries in Mythril;
- Support for additional languages (we’ll add additional ones whenever there’s enough demand).
- Support for other blockchains beyond Ethereum and EVM/eWASM.
TL;DR
MythX packs dozens of person-years of Ethereum security research by top experts into an easy-to-use API. While it builds on the original Mythril tech, it is vastly more powerful and just works™.
You can try it out now by running some early awesome MythX tools or using the Truffle Security plugin. We also invite everyone to build their own MythX tools and earn a share of the subscriptions fees paid by their users. The team is active on Discord 24/7 if you have any questions.
About Mythril and MythX
Mythril is a free and open-source smart contract security analyzer. It uses symbolic execution to detect a variety of security vulnerabilities.
MythX is a cloud-based smart contract security service that seamlessly integrates into smart contract development environments and build pipelines. It bundles multiple bleeding-edge security analysis processes into an easy-to-use API that allows anyone to create purpose-built smart contract security tools. MythX is compatible with Ethereum, Tron, Vechain, Quorum, Roostock and other EVM-based platforms.
Ready to test your smart contracts and help keep Ethereum a secure platform for all? [Sign up for a free MythX account today!]