3 ms·
If you're looking for push-button vulnerability detection for Ethereum smart contracts, then you want to use Slither (https://github.com/crytic/slither https://
by dguido 7y ago
If you're looking for push-button vulnerability detection for Ethereum smart contracts, then you want to use Slither (https://github.com/crytic/slither https://github.com/crytic/slither), not Manticore. Manticore's detector features were shoe-horned in because it kept getting compared to Mythril, not because they are a core feature. Manticore's core feature is its ability to reliably explore the state space of a program and generate inputs to reach them.
If you want to compare the effectiveness of symbolic execution engines, then you should compare how many unique codepaths they can reach. ETH Zurich recently completed such an analysis in their paper on VerX (https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf https://files.sri.inf.ethz.ch/website/papers/sp20-verx.pdf), an abstract interpretation-based verifier, and found that Manticore had the most complete model of the EVM compared to other symbolic execution engines by far, and we have continued to improve its accuracy in the releases since then. That said, ETH Zurich did underestimate a few of the capabilities of Manticore that we hope to better describe in an upcoming academic paper.
If you're looking to start using Manticore, then browse through the manticore-examples repository (https://github.com/trailofbits/manticore-examples https://github.com/trailofbits/manticore-examples) where we have complete working solutions to CTF challenges, crackmes, logic bombs, and other programs that Manticore excels at exploring.
- xwvvvvwx 7y agoHow accurate is Manticores EVM implementation? Does it pass the EVM state tests [1]? How does it’s accuracy compare to KEVM? [2]? [1]: https://github.com/ethereum/tests https://github.com/ethereum/tests [2]: https://jellopaper.org/ https://jellopaper.org/
- dguido 7y agoManticore is tested extensively against real contracts from our clients, a database of purposefully challenging code samples and mutants we've developed, and the Ethereum VMTests, a version of the state tests you linked. It has found many real bugs in our client's code.
- wslh 7y agoThis is our benchmark for Slither: https://blog.coinfabrik.com/auditing-solidity-code-with-slither/ https://blog.coinfabrik.com/auditing-solidity-code-with-slit... and also another for Securify: https://blog.coinfabrik.com/auditing-with-securify/ https://blog.coinfabrik.com/auditing-with-securify/
- dguido 7y agoThe SWC benchmark is not an effective way to test bug detection tools. The SWC only contains contrived examples that are not representative of vulnerabilities in real code. As such, it fails to capture important outcomes like false positives, which quickly lead to developers uninstalling the tool, and rewards "noisey" tools that simply alert on everything. It would be more effective to test bug detection tools against a database of real smart contract code with precisely identified vulnerabilities and example patches. Any benchmark must contain more than simple tests: it must approximate real software with enough complexity to properly stress tools for automated bug discovery. There is more discussion about what a good bug detection benchmark looks like in our own Challenge Sets from DARPA (https://blog.trailofbits.com/2016/08/01/your-tool-works-better-than-mine-prove-it/ https://blog.trailofbits.com/2016/08/01/your-tool-works-bett...) and something we were working on that is similar for smart contracts in "Not So Smart Contracts" (https://github.com/crytic/not-so-smart-contracts https://github.com/crytic/not-so-smart-contracts). You'll note that ETH Zurich and ChainSecurity came up with their own benchmark that meets the description above when they evaluated VerX in the paper I linked above. I'm eagerly awaiting the release of those test cases since they'll help us improve the functionality of many of our tools.