Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

DSI2: Identifizieren dynamischer Datenstrukturen durch Beobachtung von Programmabläufen

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)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung