Rigorous Debugging Techniques for Software Systems

Abstract

Debugging is a well-studied process in software engineering and formal methods, yet providing formal guarantees for debugging techniques remains an open challenge. This thesis introduces formal frameworks for rigorous software debugging. It targets three fundamental problems throughout the debugging lifecycle, from understanding why bugs occur to locating them precisely and ensuring that the specification against which a system is checked indeed describes the intended behavior. Across all three contributions, we explicitly state the assumptions underlying the debugging techniques and analyze how these assumptions affect the guarantees that can be obtained. First, we formalize Heisenbugs, elusive faults that occur on some but not on all executions, even if the inputs are identical. We present a causal framework that characterizes which nondeterministic mechanisms are responsible for the bug to occur and illustrate it through case studies. Further, we prove that our approach yields subsets of causes even in the presence of hidden nondeterminism, providing guarantees despite limited observability. Second, we advance the state of the art of consistency-based software diagnosis, a formal approach to software fault localization that identifies program components whose repair would restore correctness. We improve accuracy by ensuring that every diagnosis can be realized with a memory-safe repair for programs with arrays and pointers. Furthermore, we present a tool using efficient algorithms from hardware diagnosis, which significantly outperforms existing tools on standard benchmarks. In addition to these improvements, we expose fundamental limitations of consistency-based diagnosis for software, guiding future development of more robust techniques. Third, in order to validate specifications, we introduce differential property monitoring as a systematic method for comparing and refining specifications. Repeated updates to specifications are, for example, needed in security analyses when new attack vectors are discovered. By monitoring a set of system executions with multiple versions of specifications, the technique identifies executions where specifications disagree, guiding an iterative refinement process. We validate the approach in multiple case studies about detecting security backdoors. Overall, this thesis provides theoretical foundations for formal software debugging. It establishes rigorous causal reasoning about Heisenbugs, advances accuracy and scalability of formal fault localization, and introduces systematic specification validation through differential property monitoring.