Solidity Debugging meets Formal Methods

Sun, Jun 2, 2024, 10:45 AM · 56:50

**Problem** At Runtime Verification our engineers and auditors noticed a lack of advanced Solidity debuggers, especially ones that combine the intuitiveness of classical interactive breakpoint-style debugging with the depth of symbolic execution. **Solution** To close this gap, we propose Simbolik: "the Symbolic Execution Solidity Debugger", a tool specifically designed to significantly lower the entry barrier for one of Computer Science's most advanced quality assurance techniques. **What to expect** While we want to elevate our audience’s knowledge, we don’t expect any prior knowledge of formal methods or symbolic execution. We've opted into an intuitive user interface that merges seamlessly into VSCode, empowering developers to start with classical debugging and progressively advance into expert bug-finding capabilities based on symbolic execution. **How the audience benefits** As you'd anticipate, our debugger offers all conventional functionalities, from setting breakpoints to stepping through code (both at the Solidity and EVM levels), inspecting variables, and navigating call stacks. Its symbolic capabilities set our tool apart: it can begin debugging with arbitrary symbolic storage and call data, allowing users to explore the comprehensive branching control flow graph and delve into the conditions assigned to each path. Essentially, debug a function once, and you've probed every potential behavior it could manifest. **What we show** In our session, we will exemplify the debugger's core functionalities. Together, we'll uncover how it excels in detecting nuanced bugs, which often elude more traditional methodologies like testing, fuzzing, concrete debugging, and static analysis.