Effiziente Validierung der Ergebnisse von Datenflussanalysen

Das Grundszenario: Trennung von Berechnung und Verwendung von Analyseergebnissen

Ausgangspunkt des Gesamtszenarios ist ein Anweder, der die Ergebnisse von Datenflussanalysen verwenden will, ohne sie zu berechnen. Gründe für die Trennung von Berechnung und Verwendung können zum Beispiel stark beschränkte Resourcen des Anwenders - wie im Falle eines mobilen Gerätes oder eingebetteten Systems - sein.

Mögliche Verwendungen von Ergebnissen aus Datenflussanalysen sind die Überprüfung von Sicherheitseigenschaften oder auch Optimierungen, die nicht zur Analysezeit durchgeführt werden konnten.

Anforderung I: Sicherheit

Erschwert wird die Trennung der Analyse- und der Verwendungsphase durch ein inhärent unsicheres Transportmedium, wie zum Beispiel das Internet. Das heisst, dass sich der Anwender vor der Verwendung von der Validität der Ergebnisse überzeugen muss.

Anforderung II: Effizienz

Da dem Anwender nur begrenzte Resourcen zur Verfügung stehen, soll die Validierung der Ergebnisse natürlich deutlich einfacher sein, als ihre Berechnung. Hier bieten sich insbesondere im Optimierungsszenario, bei dem auch absichtlich auf Analyseinformation verzichtet werden kann, wesentliche Einsparungspotentiale.

Anforderung III: Unvollständige Programme

Immer mehr Software wird aus getrennten Bausteinen auch dynamisch zur Laufzeit zusammengesetzt. Deshalb ist es erforderlich, dass der Validierungsmechanismus auch mit unbekannten Programmbestandsteilen umgehen kann. Zusätzlich eröffnet sich so ein weiteres Anwendungsfeld im Umfeld von mobilem Code, der in einem Netzwerk übertragen und in verschiedene Systeme eingebunden werden soll. Hier können Analyseergebnisse zum Beispiel erforderliche oder bereitgestellte Schnittstellen beschreiben und eine Validierung deren Korrektheit zeigen.

Überblick über das Gesamtszenario

Die Abbildung verdeutlich die wesentlichen Aspekte des Gesamtszenarios. Ursprünglich wurden die Analyseergebnisse direkt bestimmt und von einem Werkzeug wie einem Optimierer genutzt.

In unserem Szenario werden zu getrennten Zeitpunkten oder auf verschiedenen Rechnern Teile eines Programms mittels klassischer Analyseverfahren analysiert und mit Datenflussergebnissen angereichert. Zusätzlich werden dabei diese Ergebnisse für eine effiziente Validierung aufbereitet.

Danach werden die Programmteile zusammen mit den Ergebnissen über ein unsicheres Netzwerk übertragen.

Auf der Empfängerseite nimmt ein Validator die Ergebnisse entgegen und überprüfte ihre Plausibilität bezüglich des erhaltenen Programmfragmentes.

Diese Validierungsphase bildet den eigentlichen Kern des LUPUS-Systems. Allerdings muss natürlich auch die Aufbereitung der Analyseergebnisse auf Erzeugerseite durch das System unterstützt werden.

Das Forschungsfeld

Das Grundszenario der Überprüfung von Programmeigenschaften mit Hilfe von zusätzlichen Informationen am Programmcode, geht zurück auf die Idee des beweistragenden Codes. Ursprünglich wurden Beweise, dass ein Program bestimmte Sicherheitskriterien erfüllt, durch Annotationen am Code beschrieben und überprüft. Die Grundbeobachtung dabei war, dass es im Allgemeinen leichter ist, einen Beweis zu überprüfen als in zu konstruieren. Auch die Ergebnisse von Programmanalysen beschreiben Eigenschaften von Programmen. Dies deutet bereits auf die Verwandschaft der Probleme hin, ebenso wie zum Beispiel Typinferenz - ein klassisches Datenflussproblem - stark mit einfachen Beweissystemen verwandt ist (<cite>Curry-Howard Korrespondenz</cite>).

Interessanterweise streift der Ansatz sehr viele Gebiete klassischer und moderner Programmanalyse:

• Die eigentiche Ermittlung von Programmeigenschaften bedient sich klassischer Analyseverfahren sowohl intraprozeduraler als auch interprozeduraler Art. Diese werden aber in einem Programmgerüst definiert, dass speziell darauf ausgerichtet ist, die besonderen Anforderungen des Anwendungsszenarios zu unterstützen.
• Die Aufbereitung der Analyseergebnisse auf Erzeugerseite hängt sehr stark mit bedarfsgetriebenen Analysen zusammen, die alle relevanten Datenflussinformationen bestimmen die einen bestimmten Programmpunkt beeinflussen. Ursprüngliche wurden solche Ansätze für Anwendungen wie Program-Slicing eingesetzt. Auf einer hohen Abstraktionsebene finden sich hier auch Bezüge zu Techniken des Model-Checking, die bestrebt sind den riesigen Zustandsraum eines Modell-Checking Problems zu verkleinern.
• Interprozedurale Analysen erschweren die Datenflussanalyse, weil die grundlegende Kontrolstruktur wesentlich uneinheitlicher ist, als im intraprozeduralen Fall. Zusätzlich müssen mögliche Pfade durch den Aufrufgraph eingeschränkt werden. Techniken dazu sind seid längerem bekannt, allerdings erschwert die dynamische Methodenbindung in objektorientierten Sprachen die Situation weiter. Hierbei hängt das Ziel eines Aufrufes von dem Laufzeittyp des Empfängerobjektes ab - so dass eine Typ- bzw. Zeigeranalyse erforderlich ist, um die Aufrufstruktur eine Programmms möglichst präzise zu bestimmen.
• Den letzten interessanten Aspekt bieten unbekannte Softwarebausteine, deren Wechselwirkung mit der zu analysierenden Software modelliert werden muss. Dies ist noch immer ein akutelles Forschungsthema, das auch die Fachgruppe bereits beschäftigt hat.

Falls Sie sich für dieses oder verwandte Themen interessieren, stehe ich gerne für Fragen zur Verfügung.