Source-linked AI summary
Deductive Verification via the Debug Adapter Protocol
Gidon Ernst, Johannes Blau, Toby Murray
TL;DR
Diagnosing failures in deductive verification can require access to proof details, even as automation is described as “push-button.” The paper maps symbolic execution to IDE debugging through DAP; its SecC integration was useful in a competition, though the approach can face exponential path explosion.
Problem
Deductive verification relies on user-supplied specifications and proof annotations, and diagnosing failures in correctly annotated code requires access to verification details.
Source: §1 · p. 1Method
The paper models symbolic execution as a debug target exposed through DAP operations for stepping through proof paths and inspecting symbolic state.
Source: §1 · p. 2, §2 · pp. 2–3Results
The SecC integration was useful during VerifyThis 2021 for inspecting symbolic states while developing a correctness proof, but no systematic evaluation or larger case study was conducted.
Source: §3 · p. 6Takeaways & Limitations
The authors consider the approach general and flexible for retrofitting verification tools and languages, with short-term projects within reach by relying on existing infrastructure.
Source: §4 · p. 6Nondeterministic execution can cause exponential path explosion when branches are not joined, especially with many sequential conditionals.
Source: §4 · p. 6
Abstract
from arXiv · showhide
We propose a conceptual integration of deductive program verification into existing user interfaces for software debugging. This integration is well-represented in the "Debug Adapter Protocol", a widely-used and generic technology to integrate debugging of programs into development environments. Commands like step-forward and step-in are backed by steps of a symbolic structural operational semantics, and the different paths through a program are readily represented by multiple running threads of the debug target inside the user interface. Thus, existing IDEs can be leveraged for deductive verification debugging with relatively little effort. We have implemented this scheme for SecC, an auto-active program verifier for C, and discuss its integration into Visual Studio Code.
1 Introduction
Deductive verification can demand substantial proof-engineering effort, and diagnosing failures in already annotated code requires access to verification details. The paper proposes integrating verification debugging into general-purpose IDEs through the Debug Adapter Protocol (DAP).
1 Introduction
- Diagnosing failures in correctly annotated code requires access to as much verification information as possible, despite the rise of “push-button” automation.Users still provide specifications, auxiliary annotations, lemmas, and proof hints.Source: §1 · p. 1
- Formal-methods IDEs expose proof details in varied ways, while traditional IDE debugging centers on breakpoints, stepping, and runtime data inspection.Examples include annotation highlighting, counterexample access, symbolic-state inspection, and structured verification conditions.Source: §1 · p. 1
- The paper proposes DAP-based integration of deductive verification into general-purpose IDEs to navigate interactively through proofs.It also describes an ongoing SecC implementation in Visual Studio Code and characterizes implementation as relatively easy and straightforward for symbolic-execution tools.Source: §1 · p. 2
2 Conceptual Model of a Debug Server
The conceptual debug server represents symbolic execution states and exposes them through IDE debugging operations. Schedules let users choose which branch to step, while protocol requests support navigation and state inspection.
2 Conceptual Model of a Debug Server
- A debug server maintains symbolic debug targets and exposes operations to the IDE, whose view presents source breakpoints and program state.The illustrated interface also shows variable values, potentially organized by lexical scope.Source: §2 · p. 2
- The semi-formal model omits realistic-language details such as memory, while its ideas are intended to translate to systems with symbolic structural operational semantics.The approach’s generality is stated for formal systems describable by such semantics.Source: §2 · p. 2
- Configurations combine a program, symbolic variable assignment, and path condition; sequential, parallel, and proof-obligation configurations represent execution branches and checks.A proof obligation succeeds when the conjunction of the path condition and the negation of the required condition is unsatisfiable.Source: §2 · p. 3
- A schedule selects which part of a parallel configuration steps next, and symbolic execution can produce multiple path-constrained branches.Unsatisfiable configurations can be dropped; loops may be unwound interactively or summarized with invariants.Source: §2 · p. 3
- Launch constructs configurations from procedures and globals, while GetThreads exposes step-capable branches and their hierarchical schedules.The initialization maps globals and procedure parameters to fresh logical variables and prefixes main with global initialization and its precondition.Source: §2 · pp. 3–4
- GetVariables and Evaluate expose symbolic assignments and expression values, with solver-derived facts such as entailment or concrete values available for evaluation.SecC adds path conditions, symbolic heap data, and attacker-level information to the displayed variables.Source: §2 · p. 4
- Next and StepIn each take one symbolic transition; Next uses a function contract, whereas StepIn inlines the call, and the implementation supports Next only.Continue runs to a breakpoint or completion, and StepBack can restore an earlier configuration from history.Source: §2 · p. 4
3 Debug Server Implementation for SecC
The SecC integration uses the Debug Adapter Protocol to expose symbolic verification debugging in Visual Studio Code. Its interface supports inspecting symbolic state and stepping through a defective proof path; it was useful during a competition challenge, though it has not been systematically evaluated.
3 Debug Server Implementation for SecC
- SecC is an autoactive verifier for functional correctness and security of C programs, built around SecCSL for value-dependent security properties of concurrent heap-manipulating programs.Its symbolic execution engine for Separation Logic makes it suitable for the proposed approach.Source: §3 · p. 5
- The implementation uses lsp4j to abstract the DAP in Java, while the VS Code client requires language-extension registration and hooks to start the configured server.The extended IDE features also require LSP and VS Code extension facilities, not DAP alone.Source: §3 · pp. 5–6
- The VS Code extension was developed over roughly six months, with about 1000 LoC of Scala for the server and 400 LoC of TypeScript for the extension.A working initial version for a toy language took a few days; additional features include syntax highlighting, verify-on-save, a debug console, and a symbolic execution tree view.Source: §3 · pp. 5–6
- The debugging view exposes symbolic store, path condition, and heap state, letting users inspect a defective example that writes a high-classified secret to a public memory location.Stepping at line 14 leads to verification failure.Source: §3 · p. 6
- Although no systematic evaluation or larger case study has been conducted, the integration helped develop the correctness proof for VerifyThis 2021 challenge two.It helped investigate symbolic states, subtle arithmetic constraints, and memory-predicate unfolding and folding.Source: §3 · p. 6
4 Discussion & Conclusion
The paper presents a DAP-based concept for embedding symbolic execution engines in existing IDEs and reports a straightforward, low-effort SecC implementation. It discusses exponential path growth as a limitation and points to larger-scale evaluation and combined concrete-symbolic debugging as future work.
4 Discussion & Conclusion
- The SecC implementation demonstrates that the proposed DAP-based integration can be implemented straightforwardly and with low effort.The approach embeds symbolic execution engines in existing IDEs for interactive debugging.Source: §4 · p. 6
- When branches are not joined, nondeterministic execution causes exponential path explosion, especially with many conditionals in sequence.The authors report not yet being impeded by this limitation and say its remedy through deferred SMT splitting is unclear; selective stepping could complement that approach.Source: §4 · p. 6
- Initial experiments suggest that using zippers avoids repeatedly traversing and rebuilding the configuration tree and yields elegant implementation code.The idea has also been followed before.Source: §4 · p. 6
- The authors consider the approach general and flexible enough to retrofit existing verification tools and languages, with short-term projects within reach by reusing infrastructure.They plan to investigate integrating concrete symbolic and concrete debugging and to conduct a larger SecC IDE case study.Source: §4 · p. 6