DSI2: Identifizieren dynamischer Datenstrukturen durch Beobachtung von Programmabläufen

• Antragsteller: Professor Dr. Gerald Lüttgen
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2014 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 242347041

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Softwareentwicklung konzentriert sich in der Praxis mehr auf Evolution und Wartung als auf das Erstellen neuer Software. Während Informationen über das Verhalten einer Softwarekomponente meist vorhanden sind und deren Wiederverwendung ermöglichen, reichen diese für Wartungsaufgaben, die ein detailliertes Verständnis der Komponenteninterna benötigen, oft nicht aus. Eine Datenstruktur ist dabei ein wichtiger Implementierungsaspekt und trägt wesentlich zur Softwarekomplexität bei. Zudem implementieren Entwickler häufig neue Datenstrukturen, falls nicht-funktionale Eigenschaften wie bspw. geringer Speicherbedarf entscheidend sind. Das Verstehen solcher (unüblicher) Datenstrukturen ist oftmals der Schlüssel für das Verstehen der Software. Dieses Projekt konzentrierte sich auf die Analyse dynamischer Datenstrukturen: ihrer Struktur, dem sog. Shape, und ihrer semantischen Aspekte. Der Shape betrifft die Verknüpfungsstruktur, bspw. ob diese einen binären Baum bildet. Semantische Aspekte beziehen sich auf Constraints, bspw. ob ein Baum die Kriterien eines binären Suchbaums erfüllt. Unser Interesse galt der Frage, wie eine formale Spezifikation einer Datenstruktur automatisch synthetisiert und durch diese das Programmverständnis verbessert werden kann. Auch die Visualisierung des dynamischen Speichers profitiert von formalen Spezifikationen, die zudem in der Softwareverifikation benötigt werden. Die Ergebnisse der ersten Projekthälfte haben mithilfe eines von uns entwickelten, neuartigen dynamischen Werkzeugs zur Extraktion, Identifizierung und Aggregation von Zeigerverknüpfungen, sog. Strands, gezeigt, dass selbst unüblich implementierte dynamische Datenstrukturen durch Quellcodeausführungen zuverlässig identifiziert werden können. Dies gilt eingeschränkt auch für kompilierte Programme, bspw. für den Binärcode von Malware, wobei die Analysequalität stark von nicht öffentlich verfügbaren Werkzeugen zur Extraktion von Typinformationen aus Binärcode abhängt. Daher konzentrierten wir uns in der zweiten Projekthälfte auf Programme in Bytecode, etwa kompilierte Java-Programme, wo Typinformation explizit enthalten ist. Wir entwickelten eine automatische Analyse, die formale Shape-Prädikate zur Beschreibung dynamischer Datenstrukturen erzeugt, und zeigten, wie diese zur Erstellung automatischer Abstraktionen für die Visualisierung von Datenstrukturen verwendet werden kann. Zudem entwickelten wir für den Fall, dass kein formales Prädikat verfügbar ist, eine leichtgewichtige Sprache zur Kodierung ähnlicher Abstraktionen. Darüber hinaus entwarfen wir eine neue Analyse, die auch ungültige Datenstrukturzustände berücksichtigt, um präzise Constraints für die Beschreibung semantischer Aspekte von Datenstrukturen zu erhalten. Beim Umgang mit Klassen, die komplexe Verknüpfungsstrukturen aufweisen, liefern unsere Constraints auf Objektzuständen ein Shape-Prädikat, das als Ausgangspunkt für die Programmverifikation dienen kann.

Projektbezogene Publikationen (Auswahl)

• dsOli: data structure operation location and identification. Proceedings of the 22nd International Conference on Program Comprehension, 6617(2014, 6, 2), 48-52. ACM.
  White, David H.
  
• dsOli2: Discovery and Comprehension of Interconnected Lists in C Programs. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS), Bericht2015-IX-1, pp.686-700. TU Vienna, 2015
  White, David H.; Rupprecht, Thomas & Lüttgen, G.
  
• Learning Assertions to Verify Linked-List Programs. Lecture Notes in Computer Science (2015), 37-52. Springer International Publishing.
  Mühlberg, Jan Tobias; White, David H.; Dodds, Mike; Lüttgen, Gerald & Piessens, Frank
  
• DSI: an evidence-based approach to identify dynamic data structures in C programs. Proceedings of the 25th International Symposium on Software Testing and Analysis, 2008(2016, 7, 18), 259-269. ACM.
  White, David H.; Rupprecht, Thomas & Lüttgen, Gerald
  
• POSTER. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (2016, 10, 24), 1772-1774. ACM.
  Rupprecht, Thomas; Chen, Xi; White, David H.; Mühlberg, Jan Tobias; Bos, Herbert & Lüttgen, Gerald
  
• DSI: Automated Detection of Dynamic Data Structures in C Programs and Binary Code. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS), vol. Math/Inf/02/2017 of Jenaer Schriften zur Mathematik und Informatik, pp. 134-147. Universität Jena, 2017
  Rupprecht, Thomas; Boockmann, Jan H.; White, David H. & Lüttgen, Gerald
  
• DSIbin: Identifying dynamic data structures in C/C++ binaries. 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2304(2017, 10), 331-341. IEEE.
  Rupprecht, Thomas; Chen, Xi; White, David H.; Boockmann, Jan H.; Luttgen, Gerald & Bos, Herbert
  
• Generating Inductive Shape Predicates for Runtime Checking and Formal Verification. Lecture Notes in Computer Science (2018), 64-74. Springer International Publishing.
  Boockmann, Jan H.; Lüttgen, Gerald & Mühlberg, Jan Tobias
  
• Shape Inference from Memory Graphs (Extended Abstract). Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS), pp. 69-71. Shaker Verlag, 2019. ISBN: 978-3-8440-6933-4
  Boockmann, Jan H. & Lüttgen, Gerald
  
• Data Structure Identification from Executions of Pointer Programs. University of Bamberg, Germany, Germany, 2020. ISBN: 978-3-86309-717-2
  Rupprecht, Thomas
  
• Learning Data Structure Shapes from Memory Graphs. EPiC Series in Computing, 73(NA), 151-132. EasyChair.
  Boockmann, Jan H. & Luettgen, Gerald
  
• Tagungsband zum 21. Kolloquium Programmiersprachen und Grundlagen der Programmierung. Kiel Computer Science Series, KCSS (2021, 9, 30). Department of Computer Science of the Faculty of Engineering, Kiel University.
  Boockmann, Jan H.; Jacob, Kerstin & Lüttgen, Gerald
  
• Heap Patterns for Memory Graph Visualization. 2022 Working Conference on Software Visualization (VISSOFT) (2022, 10), 162-166. IEEE.
  Boockmann, Jan H. & Luttgen, Gerald
  
• Model-driven Engineering for Dynamic Data Structures. Softwaretechnik-Trends 42(4):2-7 (2022)
  Boockmann, Jan H.; Jacob, Kerstin & Lüttgen, Gerald
  
• Shape-analysis driven memory graph visualization. Proceedings of the 30th IEEE/ACM International Conference on Program Comprehension, 168(2022, 5, 16), 298-308. ACM.
  Boockmann, Jan H. & Lüttgen, Gerald
  
• Breaking Class Invariants Through Program Mutation-based Object State Space Exploration. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS), vol. AIB-2023-03 of Aachener Informatik-Berichte, pp. 3-4. RWTH Aachen University, 2023
  Boockmann, Jan H. & Lüttgen, Gerald
  
• Comprehending Object State via Dynamic Class Invariant Learning. Lecture Notes in Computer Science (2024), 143-164. Springer Nature Switzerland.
  Boockmann, Jan H. & Lüttgen, Gerald
  
• On the Hunt for Invalid Objects: Exploring the Object State Space with Program Mutants. 2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), 31(2024, 3, 12), 711-716. IEEE.
  Boockmann, Jan H. & Lüttgen, Gerald