Which tools to use for smart contract auditing?
A security audit is more than code. You can check syntax 'till the cows come home, but real slipups run deeper and deadlier than surface cracks. Simple syntax mistakes don't mean the logic behind them is flawed, and perfectly indented and well documented code doesn't mean the logic holds up. Anything can happen and - without a good audit - it often does.
Sitting between the linters (syntax checking tools) and the humans (logic checking tools) are EVM code analysis tools. They cover the middle ground and are just one (but important) part of a good security audit. These tools produce reports on the code syntax and possibly some of the implications of the code as it is, and can make the difference between a good ICO and a catastrophic one. Here are some tools that are regularly part of our arsenal.
Mythril
Mythril is a security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities.
Made by ConsenSys, the company behind most of the community outreach and quality tools and resources in the Ethereum ecosystem, Mythril is a code analysis tool which provides a detailed overview of potential holes in smart contract code. Mythril is easy to install and use and is the first tool we fire up when starting an audit.
Manticore
Manticore is second in our test suite and runs immediately after Mythril. It's a symbolic execution tool that's arguably harder to install (Python3's venv is recommended), but it catches some edge cases that Mythril does not (and vice versa). It generates thorough reports and integrates with Ethersplay, a nifty tool for EVM disassembly visualization we'll cover next. Here's a demo of how Manticore works on Solidity (though it supports other languages and environments as well).
Ethersplay
Made by the same people who made Manticore, Ethersplay visually represents disassembled EVM code. This makes it (almost) possible to reverse engineer compiled EVM code which makes checking for logic flow inside smart contracts possible. Reading Ethersplay for useful information requires a certain degree of skill and you need to know what you're looking for, so we don't always fire it up, but when we do we usually find out something interesting.
Echidna
In more complex contracts, we write Echidna tests. Echidna is a fuzz testing framework also made by the security geniuses at TrailOfBits. Fuzz testing is, as per wikipedia:
... automated software testing technique that involves providing invalid, unexpected, or random data as inputs to a computer program. The program is then monitored for exceptions such as crashes, or failing built-in code assertions or for finding potential memory leaks. Typically, fuzzers are used to test programs that take structured inputs. This structure is specified, e.g., in a file format or protocol and distinguishes valid from invalid input. An effective fuzzer generates semi-valid inputs that are "valid enough" in that they are not directly rejected by the parser, but do create unexpected behaviors deeper in the program and are "invalid enough" to expose corner casesthat have not been properly dealt with.
Bonus: Honorable Mentions and benchmarks
Oyente is another Python-based tool that's now under the MelonPort banner. It will analyze smart contracts for common vulnerabilities. Oyente is not to be used stand-alone - it misses a lot of the common cases that Mythril and Manticore pick up, so it's best used as an addition to a mature toolset. Oyente comes with some interesting additional tools - for example, it's transaction_scrape.py script is a utility for quick and easy fetching of transactions on a given contract address (deployed).
Rattle can be used to analyze deployed contracts. It will tear them apart and visualize them, removing up to 60% of the instructions recovered from the bytecode, simplifying things, and then looking for vulnerabilities.
Securify is a web-based scanner of smart contracts which identifies vulnerabilities in the same vein as Manticore and Mythril, maybe a little higher level. It's a good tool to run code in after all the other tools are done, just in case. It cannot be run offline.
Another useful link you might want to visit is this comparison of Mythril / Manticore / Oyente output and their correctness. You'll notice that they are indeed complementary and should all be used together to cover the most possible ground.