Research: Truthful Explainable Program Analysis

Software errors are not only costly but also have significant impacts on human well-being. Shifting quality assurance earlier in the development process, known as "shifting left," is an emerging trend in cyber security, allowing software vulnerabilities to be detected before they are released and exploited. We aim to contribute to this so called Great Shift Left by developing user-friendly, yet truthful, automated verification tools.

Working with the Technical University of Munich, we have developed Goblint, a program analyzer for concurrent programs. Despite being the top race detection tool in competition conditions, Goblint's output on large real-world programs needs improvement. Our main objective now is Truthful Explainable Program Analysis, where we aim to provide explanations that are useful to developers and guaranteed to be true.

Truthful Methods for Program Analysis

Our work towards generating truthful explanations can be organized around what we call the Four Ts of Truthful Methods:

  1. Theoretical Soundness: Prove the correctness of the analysis on paper, relying on the mathematical theory of abstract interpretation.
  2. Transparent Evaluation: Implement and evaluate the analysis method transparently, ensuring replicability and generating machine-checkable witnesses to establish trust.
  3. Tangible Explainability: Work on usability and interactivity to provide accessible, human-readable explanations of analysis results.
  4. Transformative Teaching: Equip users with the necessary knowledge to effectively use analyzers and understand program correctness principles.

Our project's novelty and relevance lie in its focus on usability and explainability for abstract interpretation tools. We are committed to end-to-end truthfulness in program analysis, unlike the approaches based on heuristics and large language models.

Open-Source Projects

By achieving these goals, we hope to promote the mass adoption of sound static analysis. Thus, the most important deliverables of our work are the following publicly available open-source static analysis tools:

  • Goblint, a sound static analyzer for multithreaded C that we develop with the Technical University of Munich.
  • Põder, static analyzer for Java bytecode, developed by Kalmer Apinis, with an emphasis on explainability.