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:
- Theoretical Soundness: Prove the correctness of the analysis on paper, relying on the mathematical theory of abstract interpretation.
- Schwarz, Michael; Saan, Simmo; Seidl, Helmut; Erhard, Julian; Vojdani, Vesal. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Programming Languages and Systems: 32nd European Symposium on Programming, ESOP 2023.
- Schwarz, Michael; Saan, Simmo; Seidl, Helmut; Apinis, Kalmer; Erhard, Julian; Vojdani, Vesal. Improving Thread-Modular Abstract Interpretation. Static Analysis: 28th International Symposium, SAS 2021.
- Transparent Evaluation: Implement and evaluate the analysis method transparently, ensuring replicability and generating machine-checkable witnesses to establish trust.
- Saan, Simmo; Schwarz, Michael; Erhard, Julian; Pietsch, Manuel; Seidl, Helmut; Tilscher, Sarah; Vojdani, Vesal. Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023.
- Saan, Simmo; Schwarz, Michael; Apinis, Kalmer; Erhard, Julian; Seidl, Helmut; Vogler, Ralf; Vojdani, Vesal. Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021.
- Tangible Explainability: Work on usability and interactivity to provide accessible, human-readable explanations of analysis results.
- Apinis, Kalmer; Vojdani, Vesal. Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis. Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023.
- Erhard, Julian; Saan, Simmo; Tilscher, Sarah; Schwarz, Michael; Holter, Karoliine; Vojdani, Vesal; Seidl, Helmut. Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap. Arxiv preprint, 2022.
- 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: