Programme, die verstärkt auf dynamischen Speicher und Pointer zurückgreifen, sind bekanntlich besonders schwer zu analysieren, insbesondere wenn Programmierer die von Programmiersprachen wie C ermöglichten Freiheiten ausschöpfen. Dieses Forschungsprojekt zielt darauf ab, Programmanalysen dadurch zu vereinfachen, dass die in einem Programm verwendeten dynamischen Datenstrukturen zunächst identifiziert werden. Die von uns angestrebte automatische Identifikation schließt dabei nicht nur die Datenstruktur (z. B. eine einfach verkettete Liste) sondern auch deren Verhalten ein (z. B. eine einfach verkettete Liste verwendet als Queue oder Stack).

Zur Identifikation einer Datenstruktur und deren Verhalten ist es zunächst notwendig, diejenigen Operationen zu analysieren, welche die Datenstruktur von einem Speicherzustand zum darauf folgenden transformieren. Dazu verwenden wir eine dynamische Analyse, bei der das zu untersuchende Programm so instrumentiert wird, dass die von ihm verursachte Sequenz von Speicherzuständen zur Programmlaufzeit zurückgewonnen werden kann. Mit Hilfe von Techniken des maschinellen Lernens suchen wir in dieser Sequenz zuerst nach sich wiederholenden Mustern, die durch ein mehrfaches Ausführen von Code-Fragmenten verursacht werden. Falls dabei Operationen auf dynamischen Datenstrukturen ausgeführt werden (z. B. Einfügen am Ende oder Löschen in einer einfach verketteten Liste), so präsentieren einige dieser Muster die zu den Operationen gehörenden Code-Fragmente. Um die Operationen zu benennen, benutzen wir Techniken des Pattern Matching, welche die durch die identifizierten Code-Fragmente verursachten Speichertransformationen analysieren. Die verwendete Kombination von Operationen, die eine bestimmte Datenstruktur manipulieren, erlaubt uns schließlich, das Verhalten der Datenstruktur zu bestimmen.

Über den offensichtlichen Nutzen eines verbesserten Programmverständnisses hinaus, wenden wir unsere Technik auch im Bereich der formalen Programmverifikation an. Dazu kollaborieren wir mit Verifikationsexperten der University of York, Großbritannien im Rahmen des Forschungsprojekts Moderne Heap-Analyse und -Verifikation, welches durch die Deutsche Forschungsgemeinschaft (DFG) gefördert wird (Projekt-Nr. LU 1748/2-1), sowie mit Dr. Jan Tobias Mühlberg (K.U. Leuven, Belgien).

Kontakt: Dr. David White

Publikationen:

• White, D. H. and Lüttgen, G. Identifying dynamic data structures by learning evolving patterns in memory. In N. Piterman and S. A. Smolka, eds., 19th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), vol. 7795 of Lecture Notes in Computer Science, pp. 354-369, Rome, Italy, March 2013. Springer-Verlag.