Graduelle Abstrakte Interpretation

• Antragsteller: Professor Dr. Sebastian Erdweg
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 527381013

Die statische Analyse von Quellcode ist entscheidend für Programmierer-Feedback, die Validierung von Korrektheits- und Sicherheitseigenschaften und Compiler-Optimierungen. Eine statische Analyse leitet Eigenschaften über ein Programm ab, ohne konkrete Eingaben zu berücksichtigen oder das Programm auszuführen. Stattdessen sagt eine statische Analyse die möglichen Ergebnisse und Effekte der Ausführung des Programms für alle möglichen Eingaben voraus. Leider ist die statische Analyse praktischer Programmiersprachen aufgrund unentscheidbar, weshalb statische Analysen einen Kompromiss zwischen Präzision, Recall und Performanz eingehen müssen. Frühere Arbeiten haben gezeigt, dass die Kombination von statischer und dynamischer Analyse in einer hybriden Analyse die Analyseergebnisse erheblich verbessern kann. Während eine statische Analyse konservativ sein muss (was zu Präzisionsverlusten führt) oder Unsoundness riskiert, kann eine hybride Analyse optimistisch sein (was die Präzision beibehält) und die Überprüfung der Soundness an eine dynamische Laufzeit-Analyse delegieren. Leider sind die meisten bisherigen Ansätze für die Konstruktion hybrider Analysen ad-hoc: die statische und die dynamische Analyse müssen einzeln implementiert werden, sie kollaborieren per Konvention aber nicht per Design, und es gibt keine Korrektheitsgarantien. Kürzlich schlugen PI Tanter und Kollegen die graduelle Programmanalyse als neuartige Theorie für die Konstruktion hybrider Analysen durch graduelle Anpassung einer statischen Analyse vor, basierend auf gradueller Typisierung, welche in der Industrie große Verbreitung gefunden hat. Erste Arbeiten zur graduellen Programmanalyse zeigten, wie die Theorie zur Entwicklung einer einfachen graduellen Null-Pointer-Analyse eingesetzt werden kann. Obwohl vielversprechend, ist unklar, wie dieser Ansatz auf aussagekräftigere und fortgeschrittenere Analysen übertragen werden kann. In diesem Projekt werden wir die Theorie der graduellen Programmanalyse zu einem allgemeinen Ansatz für die Entwicklung gradueller Analysen vertiefen, der einfach zu verwenden ist, anspruchsvolle Programmiersprachen und Programmeigenschaften unterstützt und Implementierungen gradueller Analysen hervorbringt, die auf reale Codebasen skalieren. Dabei müssen wir Antworten auf grundlegende Fragen finden, wie zum Beispiel: Wie kann man abstrakte Domänen unendlicher Höhe gradualisieren, wie kann man schrittweise über effektive Berechnungen nachdenken und wie kann man eine dynamische Programmanalyse systematisch ableiten? Wir werden diese Fragen nicht nur theoretisch erforschen, sondern auch untersuchen, wie man graduelle Programmanalysen modular als graduelle definitionale abstrakte Interpreter in PI Erdwegs Analyse-Framework Sturdy realisieren kann, das für die statische Analyse von realen WebAssembly-Programmen verwendet wird. Wir werden Sturdy erweitern, um das erste praktische Framework für graduelle Programmanalysen zu schaffen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Chile
• Partnerorganisation: Agencia Nacional de Investigación y Desarrollo (ANID)
• Kooperationspartner: Professor Dr. Éric Tanter; Professor Dr. Matías Toro Ipinza