Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic

  • Statische Analyse von Zeigerprogrammen - Integration von Graphgrammatiken und Separation Logic

Jansen, Christina; Katoen, Joost-Pieter (Thesis advisor); Huisman, Marieke (Thesis advisor); Noll, Thomas (Thesis advisor)

Aachen (2017)
Doktorarbeit

Dissertation, RWTH Aachen University, 2017

Kurzfassung

In dieser Dissertation wird ein Framework zur abstrakten Analyse von Zeigerprogrammen vorgestellt, dessen Einsatzgebiet prozedurale, rekursive und nebenläufige Programme umfasst. Den Grundstein des Frameworks bildet eine auf Hypergraphen basierende Repräsentation des Heaps. Hypergraphen stellen eine Verallgemeinerung von herkömmlichen Graphen dar, in der Kanten beliebig viele Knoten verbinden können und eine Beschriftung tragen. Durch diese Generalisierung bringen Hypergraphen alle notwendigen Voraussetzungen zur Heapabstraktion mit: Während Kanten zwischen zwei Knoten als Zeiger aufgefasst werden, fungieren alle übrigen Kanten als Platzhalter. Diese Platzhalter können durch Heapteile ersetzt werden, deren Struktur von sogenannten Hyperedge Replacement-Grammatiken formal beschrieben wird. Konkretisierung und Abstraktion der Heaprepräsentation entspricht der Anwendung von Produktionsregeln der Grammatik: eine Rückwärtsanwendung abstrahiert den Heap, während eine Vorwärtsanwendung einer Konkretisierung entspricht. Im ersten Teil der Dissertation werden die formalen Voraussetzungen für die Heaprepräsentation sowie ihrer Konkretisierung und Abstraktion geschaffen. Auf dieser Grundlage wird ein Ansatz zur Analyse von nicht-prozeduralen Zeigerprogrammen vorgestellt. Dazu werden alle Anforderungen an Hyperedge Replacement-Grammatiken erarbeitet, die für eine korrekte und terminierende Konkretisierung und Abstraktion nötig sind. Weiterhin wird die Konstruktion einer äquivalenten, diese Eigenschaften erfüllenden Grammatik adressiert. Der zweite Teil der Dissertation schlägt eine Brücke in Form eines beidseitigen Übersetzungsalgorithmus zwischen Hyperedge Replacement-Grammatiken und dem symbolic heap-Fragment der Separation Logic. Neben dem Korrektheitsbeweis der Übersetzung werden die Gegenstücke der Anforderungen an Hyperedge Replacement-Grammatiken aus dem ersten Teil für die Separation Logic definiert und ihre Erhaltung während der Übersetzung bewiesen. Die hergestellte Beziehung zwischen Separation Logic und Hyperedge Replacement-Grammatiken bildet den Grundstein für die Erweiterung des Analyseframeworks. Im letzten Teil dieser Dissertation wird das Spektrum der analysierbaren Zeigerprogramme auf prozedurale sowie nebenläufige Programme ausgedehnt. Dazu bedienen wir uns des Konzepts der Contracts, die bereits im Bereich der Zeigerprogrammanalyse mithilfe von Separation Logic erfolgreich eingesetzt werden. Ein Contract bildet ein Paar aus Vor- und Nachbedingung, wobei die Nachbedingung den Effekt einer Prozedur oder eines Threads auf die Vorbedingung erfasst. Damit erlaubt er eine modulare Analyse von Programmen auf Prozedur- bzw. Threadebene. Um auch im Fall von nebenläufigen Programmen Threads unabhängig voneinander untersuchen zu können, werden zusätzlich so genannte Permissions, d.h. Berechtigungen zum Lesen oder Schreiben von Teilen des Heaps, eingeführt. Auch hier handelt es sich um ein Konzept, das für die Separation Logic etabliert ist. Das Hauptresultat des letzten Dissertationsteils besteht in der Erarbeitung eines neuartigen Ansatzes, der zu einem Zeigerprogramm sowohl Prozedur- als auch (Permission-annotierte) Threadcontracts automatisiert generiert.

Identifikationsnummern