MythX (The Bug’s Shadow) Symbolic Execution for Smart Contracts Analysis. — Tool Comparison.
When it comes to Smart Contracts, you wouldn’t like to ‘play games’ literally, with your code. In fact, it puts your business logic at risk.
We made an analysis of some latest tools to help you enhance your Smart Contracts security under Symbolic Execution & other techniques. We found MythX to be the leader choice for Smart Contracts security as it fast, intuitive, and you can run it in a variety of different ways. Offering high-risk level security analysis performance for your Smart Contracts.
We use a “Betting Fair-Play Game” Smart Contract as we undoubtedly think this contract require high security and user always shall argue if is fair or not to “play” this certain type of games, adding a level of trust by the user because of the Blockchain. Which we think it’s important for our analysis. This contract is Free to use and Open Source.
We also use a simple-test Smart Contract (Guess the Number) which we think it’s fun and shows accuracy on MythX detecting Smart Contract Vulnerability.
MythX Ease of Setup:
Choose your flavor to begin and you’ll be running your Smart Contract analysis in less than 30 minutes if not less:
Remix MythX Plugin (The fastest setup!)
MythX CLI (tasty-cli)
Truffle Plugin (Easy installation for Truffle Lovers)
VSCODE Remix Code (All in One-Place)
Extensible easy of use language libraries:
Running MythX on Remix in a blink.
Remix MythX plugin doing some magic:
We found a SWC-104 Unchecked Call Return Value, on our Smart Contract test audit this contract was designed using a necessary fallback but an exception handling for it’s not implemented. Could potentially cause malfunctioning of the Smart Contract.
Analysis can be fully visualized thru the MythX Dashboard /View Analysis Section.
Remix MythX Plugin Guessing the number:
Found a SWC-105 Unprotected Ether Withdrawal
On this test MythX found a highly critical bug where ANYONE could drain funds from the smart contract by just executing:
msg.sender.transfer(ether amount);
MythX CLI Analysis:
Love MythX CLI and made the comparison with other tools, using this one as easy, fast to install and use.
The fact I like most to use MythX CLI is:
“The MythX CLI allows you to generate HTML or Markdown reports for a single analysis job (denoted by the job’s UUID), or a whole analysis group. For each analysis, the current status, the input, and the report for the detected issues are fetched and rendered onto a template.”
We love HTML and we love outputting things in HTML or Markdown!
Sometimes you don’t need fancy. Just just need to be simple! And having your report in a high-quality HTML or Markdown format its best way to get it.
VSCode MythX Plugin Analysis:
Enough just by going to the extension panel on your VSCode interface.
Typing “MythX” on the search box will find out the official MythX plugin for VSCode
MythX Truffle:
Running MythX through Truffle
After analyzing the contracts MythX on Truffle outputs report logs. Which includes link to the dashboard panel and the report ID
So far you tasted the different MythX flavors to analyze and debug your Smart Contracts in an accurate way. Although. MythX has different plan versioning for diferent kind of users. Choose between:
Free, Dev, Pro or Enterprise plans. Each plan contains different features. Feel free to choose one that adapts to your needs.
Chainsecurity established company in Switzerland. They offer “formal” audit services for Smart Contracts.
They provide you with a “formal” form for auditing your Smart Contract with some of their specialists.
Thus, they also have some tools for auditing your contracts.
Created by ICE center, ETH Zurich and ChainSecurity AG, a top provider for smart contract audits.
You can run Securify through their webapp.
Upon completing your code audit, the system outputs some information on the UI as welll as a link for you to share the audited Smart Contract.
- Securify supports only 38 vulnerabilities as of today.
- You will only be able to analyze Smart Contracts greater or equals to Solidity 0.5.8
- Securify can run through Docker
VerX by Chainsecurity
Chainsecurity provides you with a small VerX test through its webapp
They have a standard ERC20 Token contract for sample aswell as a crowdsale for this Token Smart Contract and a full Overview.
You can run “Verify” and it will output a friendly report on the same app.
If we would like to analyze our own Smart Contract we’d need to go to: VerX Docs
They provide you with a python client for you to analyze the desire Smart Contract.
Running VerX Client:
By following the instructions on their docs you should be able to run the client in a very short time:
VerX CLI Tool returns analysis in JSON data
VerX CLI Tool requires manual Deployment script to execute Smart Contract Analysis beforehand.
- Chainsecurity does not provide a Remix Plugin.
- Chainsecurity does not provide VSCode Plugin.
Manticore Smart Contract Auditing tool is designed to run in traditional computing enviroments ((x86/64, ARM) aswell as on the Etherem Virtual Machine.
Manticore support is under Linux as developers state. Meaning all updates and support are expected to be under this system.
Manticore also provide a full Python API for you to make custom scripts for analyses
Running Manticore CLI on Docker:
- You can run Manticore thru Docker (Very fast).
- Manticore does not provide a Remix Plugin.
- Manticore does not provide a VSCode Plugin.
- Manticore extends analysis support for Linux Scripts.
Manticore Symbolic Execution Contract Analysis Test:
Manticore outputs reports as mcore_ by default which is a folder and it contains a different reporting specific to each for instance to each test cases.
Oyente is another one Smart Contract analysis tool we compare with MythX. Being this latest also highly competitive and it shows mostly positive feedback on the playground.
Versioning dependencies:
Remote contract evaluation
You can analyze a remote contract (e.g. contract link) by providing a link to using Oyente tool as long as it as a solidity contract by simple running:
python oyente.py -ru [link to contract]
Analyzing external remote contract:
Oyente on Docker (Simple):
By far one on the things you can do with Oyente is play with it using Docker and it’s one of the few reasons that makes this app highly competitive because its simplicity.
‘Puzzle’ is a default test Oyente’s contract
so far the analysis outputs:
remote_contract.sol:2:1: Warning: Integer Underflow.
remote_contract.sol:20:4: Warning: Callstack Depth Attack Vulnerability.
remote_contract.sol:27:6: Warning: Transaction-Ordering Dependency.
Running the test analysis we can find out Oyente outputs us its analysis thru the same default console. Making things simpler.
- Oyente runs under Docker
- Oyente does not provide a Remix Plugin.
- Oyente does not provide a VSCode Plugin.
- Oyente supports compiling 0.4.19 as of today.
- Oyente can outputs report in JSON.
Some known vulnerabilities detectable by Oyente:
- Integer Underflow
- Integer Overflow
- Callstack (Deprecated as this isn’t happening in new EVM)
- Money Concurrency
- Time Dependency
- Reentracy
Conclusion:
One of the main advantages of MythX against other smart contract security tools is that you can run the analysis through the MythX Remix Plugin. It’s 10x faster! Easy and forward to outputting your Smart Contract Analysis, and a high-level quality reporting thru the MythX Dashboard interface for those Remix IDE enthusiasts. Brought by Consensys it is being active development and maintenance.
