slither

Ugh, I have been advocating "Solidity--" for years and can't get funding to build it (Trail of Bits). We use two tools to offer quick turnaround automated testing and verification for Solidity: Echidna (like QuickCheck for Solidity) and Manticore (a symbolic verifier). They each let you write high level properties in the span of 1-2 weeks that cover a large amount of potential use cases. Here's an example of what that looks like: https://github.com/trailofbits/publications/blob/master/revi... Here's Echidna: https://github.com/crytic/echidna and Manticore: https://github.com/trailofbits/manticore Sometimes we also use custom static analyses built around Slither's IR during projects too: https://github.com/crytic/slither/wiki/SlithIR

This feature will be integrated into Slither[1], one of the open-source tools to find bugs in smart contracts the company uses. AFAIK, clients do not pay for specific features, they pay to get efficient security reviews where the company finds bugs in their code and this feature can help to find issues faster. [1] https://github.com/crytic/slither

FWIW I agree with the intent of this statement. The odd lesson we've learned is that extreme testability can overcome broken tools to create secure code. It's not the outcome you would expect since the orthodox in security engineering is that it depends on secure programming languages, frameworks, and compilers, which we have none of in Ethereum. But somehow people are carrying around hundreds of millions of dollars in smart contracts secured with high-powered testing and verification techniques. It's very weird. I explored this topic a bit in a keynote earlier this year: https://github.com/trailofbits/publications/blob/master/pres... I will also note that our long-term goal for Slither is to directly address some of the problems in Solidity (https://github.com/crytic/slither). It's like 2/3rds of a compiler already. It just needs a littl

If you're looking for push-button vulnerability detection for Ethereum smart contracts, then you want to use 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), an abstract interpretation-based verifier, and found that Manticore had the most complete model of the EVM compared to other symbolic execution engines by