MythX smart contract security API update: Revamped vulnerability detection and new property checking mode
The MythX team is proud to announce a new release of the MythX security analysis API! MythX v1.7 includes major updates to our vulnerability detection capabilities and adds a new mode that is optimised for checking custom security properties.
Revamped Vulnerability Detectors
With the latest release of MythX API we have completely revamped the generic bug detection capabilities, including adding new detectors, improving all descriptions and risk ratings, and adapting the detectors to the latest best practises. We now run 46 detectors out-of-the-box. Note that one detector often covers different issues and may leverage multiple analysis techniques — if we’d count each detector individually we’d end up at well over 100 but making the number look as high as possible was not a design goal.
You can think about MythX as a supercharged version of the ”usual suspect” security tools (Solidity/IR static analyzer, bytecode fuzzer and symbolic analyzer), but with extra logic that ensures that the whole becomes more than the sum of its parts. For instance, integer overflows are checked for using both symbolic execution and input fuzzing and the results are assessed and augmented by our static Solidity analyser. As a result, we get increased coverage, some redundancy in case either tool misses a bug, and less false positives.
Try it out with the Remix plugin, MythX command line client or Truffle extension.
Property Checking Mode
MythX 1.7 introduces a new mode that enables users to check smart contract security properties more efficiently. I’ve written before about using MythX for property checking (e.g. here and here). With this new API flag, the fuzzer and symbolic analyser are optimised to check specifically for assertion violations. This will become even more handy when we finally get support for formal specs in Solidity.
Property checking mode currently only supported by the MythX command line client and solfuzz.
To run an assertion check with MythX CLI, install the latest version and add the –check-properties flag:
$ mythx analyze --check-properties <solidity-file>[:contract_name]
Or, install solfuzz with npm install -g solfuzz and run:
$ solfuzz check <solidity_file> [contract_name
This will output all detected assert violations and counter-examples:
$ solfuzz check VerifyERC20_Tether.sol
✔ Loaded solc v0.4.25 from local cache
✔ Compiled with solc v0.4.25 successfully
✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/8effd147-4090-4422-b585-e1dc3a0e3087
--------------------
ASSERTION VIOLATION!
/Users/bernhardmueller/Desktop/Contracts/VerifyERC20_Tether.sol: from 573:17 to 573:154
AssertionFailed('Contract-wide invariant ensures {invariant balanceOf(address(0)) == 0} in contract MythXERC20Verification was violated')
--------------------
Call sequence:
1: transfer(0x0000000000000000000000000000000000000000, 55834574848)
Sender: 0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe [ CREATOR ]
Value: 0
--------------------
ASSERTION VIOLATION!
/Users/bernhardmueller/Desktop/Contracts/VerifyERC20_Tether.sol: from 724:17 to 724:94
AssertionFailed('approve(spender=address(0), ...) should raise an exception')
--------------------
Call sequence:
1: approve(0x0000000000000000000000000000000000000000, 0)
Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa2 [ USER ]
Value: 0
The solfuzz README has further examples.
What’s this magical MythX thing you’re talking about?
MythX is a cloud-based service that uses symbolic analysis and input fuzzing to detect security bugs and verify the correctness of smart contract code. It integrates with IDEs like Remix and Truffle and can be used both during development and in the continuous integration pipeline. Using MythX requires an API access token which is available on the MythX website.
You might also like:
- Generic bug detection with MythX
- Checking custom properties using the AssertionFailed event
- Awesome MythX tools
MythX smart contract security API update: Revamped vulnerability detection and new property… was originally published in ConsenSys Diligence on Medium, where people are continuing the conversation by highlighting and responding to this story.