Verifikation der Speicherhandhabung in bestehenden C Programmen mit numerischen abstrakten Domänen.

• Antragsteller: Dr. Axel Simon
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2009 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 154707536

Formale Methoden, basierend auf Spezifikationen und design-by-contract, werden seit langem propagiert um verlässliche Software zu konstruieren. Aufgrund der Kosten dieses Ansatzes und dem großen Umfang an bestehender Software, stieg das Interesse an der Erforschung von automatischen Analysen für Softwareprodukte ohne jegliche Spezifikation. Wegen der fehlenden Spezifikation können solche Analysen höchstens die Abwesenheit von gewissen Laufzeitfehlern nachweisen, da Laufzeitfehler von der Ausführungsumgebung bestimmt sind (z.B. von der Sprachspezifikation von C). Interessanterweise, wenn diese Laufzeitfehler ausgeschlossen werden können, sind auch die schwerwiegendsten Sicherheitslücken, in denen beliebiger Kode auf fremden Rechnern ausgeführt werden kann, ausgeschlossen: Diese Fehler nutzen eine inkorrekte Verwaltung des Arbeitsspeichers aus, welches normalerweise zu einem Laufzeitfehler führt. Das Ziel des Projektes ist es daher, eine performante Analyse zu entwickeln die genau genug ist, um die Abwesenheit von Speicherverwaltungsfehlern in bestehenden C Programmen zu zeigen. Das Projekt ist zweigeteilt: Der erste Teil beschäftigt sich mit der Analyse von ausführbarem Kode welches die Behandlung von Software ermöglicht, deren Quellkode nicht zugänglich ist und welches die Betrachtung von nebenläufigen Programmen ermöglicht. Der zweite Teil kombiniert die Analyse von dynamischen Datenstrukturen mit numerischen Abstraktionen. Dieser Ansatz wird danach auf die kontext-sensitive Analyse von Funktionen angewandt, um die wiederholte Analyse von Funktionen für jeden neuen Aufruf zu verhindern.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen