Statische Analyse durch abstrakte Interpretation, WS 2007/2008

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungszettel
• Leistungsnachweise
• Literatur
• Software

Termine

Überblick

Unter der statischen Analyse eines Programms versteht man die korrekte, endliche und approximative Berechnung der möglichen Programmausführungen. Die Approximation ist natürlich erforderlich, weil andernfalls in der Regel gar keine Berechnung mit endlichem Zeit/Speicheraufwand möglich wäre. "Korrekt" bedeutet dabei, dass alle realen Programmausführungen in dem durch die approximative Berechnung eingegrenzten Wirkungsbereich liegen (sog. Über-Approximation). Bei einer adäquaten Approximation (d.h. Abstraktion) kann man daher folgern, dass Korrektheitsaussagen über das abstrahierte Programm in eine Korrektheitsaussage über das konkrete Programm übersetzbar sind. Das Verfahren ist aufgrund der Abstraktion jedoch nicht vollständig: Verletzungen einer Korrektheitseigenschaft auf abstrakter Ebene sind untern Umständen mit den konkreten Variablenbelegungen und Kontrollstrukturen des Programms gar nicht möglich.

Statische Analyse findet heute eine weite Anwendung in der Praxis, mit teilweise äusserst leistungsfähiger Werkzeugunterstützung: Im Compilerbau werden Codeoptimierungen mit Hilfe statischer Analyse auf Zulässigkeit geprüft. Vor allem bei sicherheitsrelevanten Systemen wird entwickelter Code auf die Abwesenheit von Laufzeitfehlern (z.B. Speicherbereichsüberschreitungen, Auftreten arithmetischer Ausnahmen) überprüft. Für die automatische Testfallerzeugung werden Verfahren der statischen Analyse verwendet, um die Nichterreichbarkeit bestimmter Codekomponenten nachzuweisen und (mit einer Variante der nachfolgend beschriebenen abstrakten Interpretation) um automatisch Testfälle und zugehörige Daten zu erzeugen.

Die wichtigste Technik für statische Analysen ist abstrakte Interpretation: Hier wird die o.g. Approximation durch eine Abstraktionsabbildung von den konkreten Variablenbelegungen und Ablaufstrukturen auf abstrahierte Valuationen und Strukturen abgebildet. Abstrakte Interpretation steht daher im Vordergrund dieser Vorlesung.

Inhalte der Vorlesung:

1. Verbandstheorie und ihre Bedeutung für die Abstraktion
2. Galois Zusammenhänge zum Nachweis adäquater Abstraktionen
3. Ableitung der Abstraktionssemantik bei gegebener Programmsemantik und zugehörigem Galois Zusammenhang
4. Programmverifikation durch Prädikat-Abstraktion
5. Erste Anwendungen:
   • Vorzeichenprüfung beim Aufruf mathematischer Funktionen mit nicht-negativem Definitionsbereich
   • Typ-Inferenz bei der Interpretation ungetypter Sprachen
6. Kontrollflussgraphen und Datenflussanalyse, Fixpunktbestimmung
7. Abstrakte Interpretation durch Intervall-Analysis
   • Einführung
   • Anwendung bei der Verifikation auf Abwesenheit von Laufzeitfehlern
   • Anwendung bei der Testdatengenerierung
   • Widening und Narrowing zur Erzeugung von Fixpunkten
   • Anwendung bei der Erreichbarkeitsanalyse
   • Programmverifikation durch Erreichbarkeitsanalyse
8. Interprozedurale Analyse
9. Pointeranalyse und zugehörige Speichermodelle
10. Abstrakte Interpretation von CSP-Prozessen, - der CSP Verfeinerungsbegriff und seine Bedeutung für den Nachweis der Adäquatheit von Abstraktionen

Alle benötigten Konzepte und Definitionen werden im Rahmen der Vorlesung eingeführt. Ein Vorlesungsmanuskript wird zur Verfügung gestellt. In den Übungen werden die eingeführten Methoden auf konkrete Programme eines eingeschränkten C-Spachdialektes angewendet.

Für Hörer dieser Vorlesung könnte ebenfalls die Vorlesung Testautomatisierung II von Interesse sein: Dort wird abstrakte Interpretation durch Intervall-Analysis vertieft für die Testfall-/Testdatengenerierung angwendet.

Veranstaltungsinhalte

Session 1

• Informelle Einführung in abstrakte Interpretation anhand der Vortragsfolien Introduction to abstraction and static analysis von David Schmidt
• Abstraktion und Konkretisierung
• Anwendungsgebiete: Statische Analyse und Compilerbau
• Partielle Halbordnungen und Verbände
• Galoisverbindungen zwischen Verbänden
• Beispiel: Abstrakte Interpretation einer Funktion durch Verband ({Τ,even,odd,⊥},&sube)
• Konkrete Semantik und Abstraktionssemantik
• Kriterien für eine korrekte abstrakte Interpretation

Session 2

• Formale Definition: Halbordnung
• Formale Definition: Verband
• Kleinste/größte obere/untere Schranke
• Meet/Join Operationen
• Vollständige und unvollständige Verbände
• Formale Definition: Galois Zusammenhang
• Lifting von Operationen

Session 3

• Operationelle Semantiken als Transitionssysteme
• Zustandsraum
• Startzustände
• Zustandsübergangsrelationen
• Potenzmengenverband und zugehöriges Transitionssystem
• Zustandsübergangsrelation für Potenzmengenverband
• Operationelle Regeln
• Definition: Zulässigkeit einer abstrakten Transitionsrelation
• Definition: Zulässigkeit einer abstrakten Interpretation

Session 4

• Klassischer Zustandsraum für imperative Programmiersprachen
• Programmtext als Locations
• Valuationsfunktionen
• Kanonische Verbandskonstruktionen
• Kartesisches Produkt von Verbänden
• Partielle Funktionen mit Verbänden als Bildmenge
• Abstraktion von Valuationsfunktionen durch Abstraktion von Datentypen
• Kanonische Konstruktion des Abstraktionstransitionssystems
• Operationelle Regeln für die abstrakte Zustandsübergangsrelation
• Kanonische Konstruktion einer Galois Verbindung zwischen Potenzmengenverband und Abstraktionsverband

Session 5

• Beweis der Zulässigkeit einer Abstraktion nach Konstruktionsvorschrift
• GC zwischen Zustandsräumen
• Zulässigkeit der abstrakten Transitionsrelation
• U- und L-Simulationen über konkrete und abstrakte Zustände

Session 6

• Verband Loc → (X → PARITY)
• Ordnungsrelation
• GC zu Verband ℘(Loc × (X → PARITY))
• Verband Loc → (X → I(int))
• Ordnungsrelation
• GC zu Verband ℘(Loc × (X → IR))
• Beispielprogramm und Berechnungen in Verbänden
• ℘(Loc × (X → int))
• ℘(Loc × (X → I(int)))
• ℘(Loc × (X → PARITY))
• Loc → (X → I(int))
• Loc → (X → PARITY)

Session 7

• While-Sprache G1
• Valuationsfunktionen für Arrayvariablen
• Operationelle Semantikregeln für G1
• Operationelle Semantikregeln für Loc → (X → L(t)) auf Basis von G1

Hintergrundmaterial

• Skript zur Vorlesung
(letzte Aktualisierung: 2008-02-04)
• Beispielbeweis aus dem Tutorium vom 14.11.2007
• Folien zum Tutorium vom 28.11.2007
• Beispielbeweis aus dem Tutorium vom 9.1.2008

Übungszettel

Leistungsnachweise

• Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben inkl. bestandenem Fachgespräch,
• oder durch eine bestandene mündliche Prüfung (alias mündliche Modulprüfung).

Die genauen Bedingungen werden in der ersten Vorlesung verhandelt.

Literatur