Echidna Enters a New Era of Symbolic Execution

Summary

In this post, we will see a bit of the new Echidna capabilities using the enhanced symbolic execution from hevm. In a nutshell, symbolic execution works in the same way as fuzzing, checking whether a program has specific issues, like assertion failures. However, unlike fuzzing, it either confirms the program works correctly by showing no paths lead to these issues, or it finds examples that prove such issues exist. An initial implementation of Echidna’s symbolic execution capabilities was added last year, but it was recently consolidated after PR 1349 was merged, which implemented symbolic execution in two “flavors”:Verification mode for stateless tests: This mode aims to prove the absence of bugs, aligning with tools like hevm, Halmos, and Certora.Exploration mode for stateful tests: This mode combines symbolic execution with fuzzing campaigns to identify assertion failures in scenarios involving state changes.The integration of symbolic execution into Echidna is guided by a key principle: vulnerability research tools should minimize the requirements placed on users. In the context of smart contract security, this means no new cheat codes or specialized tests are needed, just the same codebase used in traditional fuzzing campaigns.Before diving deeper, we would like to acknowledge the hevm team for their exceptional work over the past year. Their improvements to symbolic execution performance and capabilities, detailed in the recent release, have been critical to enabling seamless integration with tools like Echidna.Verification ModeVerification mode mirrors formal verification techniques applied to stateless (or single-transaction) code. In Echidna’s new verification mode, the tool analyzes a contract by first executing its constructor and then symbolically testing each method. This approach is ideal for fully stateless functions (e.g., mathematical logic) but can also be used strategically in stateful code, similar to Halmos’ methodology.When a test is explored u...