8 ms·

Manticore: A Symbolic Execution Framework for Binaries and Smart Contracts

53 points by galapago 7y ago

wslh 7y ago
If you are interested, last November we benchmarked Manticore against other security tools based on common Ethereum smart contract bugs. Here are the results https://blog.coinfabrik.com/smart-contract-auditing-human-vs-machine/ https://blog.coinfabrik.com/smart-contract-auditing-human-vs...
- 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 ago
    How 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 ago
      Manticore 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 ago
    This 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 ago
      The 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.
emilypi 7y ago
We're seeing a small cottage industry of state-machine verification techniques presenting themselves over the past year. K-framework has its accessibility proofs (ranging over the state space of possible program paths), Manticore has its symbolic state analysis, and a few others do roughly the same thing. None of these frameworks are focusing on improvement of the language or supplementing its features - they're just trying to make up for how easy it is to write bug-ridden EVM contracts! Good on them, but it points to how fundamentally flawed the EVM is by design.
- mirekrusin 7y ago
  It's like saying that "assembly is fundamentally flawed" because people came up with haskell.
  - emilypi 7y ago
    It's in the sense that it's extremely difficult to write a program and fully understand what it's doing - that's why higher order representations and correct-by-construction languages were invented. Rather than putting bandaids on it with secondary and tertiary frameworks, languages like Haskell were built to be correct by construction. But then there's the question of whether any of those flaws are even reasonable to take upon your contract when you consider their use-case within a blockchain context. If you're only ever running terminating programs, why expose the entire language to the attack surface of non-determinism and re-entrancy bugs when there are very reasonable and expressive CbyC languages available?
    - mirekrusin 7y ago
      EVM is not a language. EVM is deterministic otherwise the whole Ethereum would not function at all. Your criticism is directed more towards ie. Solidity. However alternatives are not availble as far as I know. There are some research projects but everything in this area is in alpha-research state.
      - DennisP 7y ago
kikinam 7y ago
You don't have to know the Binary code to be able to post your ads online. I have recently sold my car there. Using this site https://www.jacars.net https://www.jacars.net you will find countless options from various sellers in Jamaica. You will contact the sellers or buyers directly. You will also find photos attached to see the goods online.
RichardHeart 7y ago
I'm in need of an audit for HEX.win if any of the super smart folks here want to reach out. RichardHeartAuthor at gmail dot come.
prateek_mir 7y ago
Pardon me if I sound dumb, but going by the abstract, this is essentially concolic analysis of smart contracts ?

53 points by galapago 7y ago

wslh 7y ago

If you are interested, last November we benchmarked Manticore against other security tools based on common Ethereum smart contract bugs. Here are the results https://blog.coinfabrik.com/smart-contract-auditing-human-vs-machine/ https://blog.coinfabrik.com/smart-contract-auditing-human-vs...

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 ago
  How 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 ago
    Manticore 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 ago
  This 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 ago
    The 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.

emilypi 7y ago

We're seeing a small cottage industry of state-machine verification techniques presenting themselves over the past year. K-framework has its accessibility proofs (ranging over the state space of possible program paths), Manticore has its symbolic state analysis, and a few others do roughly the same thing. None of these frameworks are focusing on improvement of the language or supplementing its features - they're just trying to make up for how easy it is to write bug-ridden EVM contracts! Good on them, but it points to how fundamentally flawed the EVM is by design.

mirekrusin 7y ago
It's like saying that "assembly is fundamentally flawed" because people came up with haskell.
- emilypi 7y ago
  It's in the sense that it's extremely difficult to write a program and fully understand what it's doing - that's why higher order representations and correct-by-construction languages were invented. Rather than putting bandaids on it with secondary and tertiary frameworks, languages like Haskell were built to be correct by construction. But then there's the question of whether any of those flaws are even reasonable to take upon your contract when you consider their use-case within a blockchain context. If you're only ever running terminating programs, why expose the entire language to the attack surface of non-determinism and re-entrancy bugs when there are very reasonable and expressive CbyC languages available?
  - mirekrusin 7y ago
    EVM is not a language. EVM is deterministic otherwise the whole Ethereum would not function at all. Your criticism is directed more towards ie. Solidity. However alternatives are not availble as far as I know. There are some research projects but everything in this area is in alpha-research state.
    - DennisP 7y ago

kikinam 7y ago

You don't have to know the Binary code to be able to post your ads online. I have recently sold my car there. Using this site https://www.jacars.net https://www.jacars.net you will find countless options from various sellers in Jamaica. You will contact the sellers or buyers directly. You will also find photos attached to see the goods online.

RichardHeart 7y ago

I'm in need of an audit for HEX.win if any of the super smart folks here want to reach out. RichardHeartAuthor at gmail dot come.

prateek_mir 7y ago

Pardon me if I sound dumb, but going by the abstract, this is essentially concolic analysis of smart contracts ?