The Tech Behind MythX Smart Contract Security Analysis
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 350,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” came up: What if you could simply submit your contracts to an 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 15 heads and we have built (and acquired) 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 in less than 2 minutes.
Basically, MythX was 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 (well, technically we’re still in beta and things still break sometimes, but those kinks will be ironed out soon). If you have a Solidity file at hand you can try it right now:
$ npm install -g @cleanunicorn/mythos
$ mythos analyze <filename> <contract_name>
MythX Security Analysis
When you submit an analysis job to MythX, a lot of things happen. First, your MythX client submits all compiler artifacts, including bytecode, source maps, and the source code itself to the analysis service. The MythX service then forwards those inputs to several micro-services that run in parallel for a predefined execution time. It then evaluates 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 and performs static security checks. This type of analysis is very fast, but the results are less comprehensive and reliable than the results of more costly analysis types.
The MythX research team is currently working on a transpiler that converts Solidity code into an SSA intermediate representation and drastically improves Maru’s detection capabilities. We’re doing this to enable a “lightning” ⚡ mode that is useful for linters and IDE plugins that need to provide real-time feedback. Lightning mode will be ready to go by mid-2019. It is being built by Gerhard Wagner, Pavel Zverev and Dimitar Bounov and will likely be open-sourced later this year.
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 nearly a year ago. Its symbolic execution engine has been completely refactored. It now performs 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:
- Introduction to Mythril and Symbolic Execution
- Practical Smart Contract Security Analysis and Exploitation — Part 1 (yeah I know, I never wrote part 2 🙄).
- Smashing Smart Contracts
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, because the most interesting possibilities open up by letting the tools “talk” to each other. For example, a static analysis run can pre-determine interesting paths and provide seed states to the fuzzer, or give the symbolic analyzer a prioritized list of interesting states (or exclude certain paths from symbolic analysis altogether). This way, the analysis becomes a lot more efficient, and we are able to return a comprehensive result within seconds to minutes.
There’s actually another player named Maestro who pulls the strings in the background. Maestro decides on what jobs should go to which tool and knows how to interpret the results (all our tools speak a common JSON language). It also helps to remove duplicates and false positives, and can assign a confidence rating by correlating the output of multiple tools.
We’re now putting a lot of work into Maestro to make it “direct” our tools in a Mozart-like fashion and make the analysis more efficient.
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:
- 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 better search strategies and redundant state elimination in Mythril and static pre-analysis to reduce the search space for both Mythril and Harvey;
- Applying machine learning to improve analysis quality over time;
- Support for other EVM-based blockchains such as Quorum;
- Support for additional languages (we’ll add additional ones whenever there’s enough demand).
- Support for other blockchains beyond Ethereum and EVM/eWASM.
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.