Software-Manipulationsprüfung

• Antragsteller: Professor Dr.-Ing. Gregor Snelting
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2003 bis 2009
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5410050

Ob Berechnungen in sicherheitskritischer Software von außen manipuliert werden können, ist - gerade auch mit Blick auf den 11. September - eine wichtige Frage. Wir wollen in diesem Forschungsvorhaben entsprechende Programmanalyseverfahren entwickeln, die entweder garantieren, dass keine Manipulation möglich ist, oder aber konkrete Manipulationsszenarien automatisch inferieren. Auf diese Weise wird insbesondere eine vollständige "Information Flow Control" im Sinne der "Common Criteria" für sicherheitskritische Software realisiert, die weit durchschlagender als existierende Verfahren ist. Ausgangspunkt ist das in den letzten Jahren am Lehrstuhl entwickelte System VALSOFT, dass für gegebene Programmpunkte genaue Bedingungen dafür inferieren kann, dass zwischen den Punkten ein Informationsfluss stattfindet. VALSOFT ist jedoch auf Ansi-C beschränkt und kann maximal 20000 LOC analysieren. Ziel des vorliegenden Antrags ist es, VALSOFT zu einem real einsetzbaren System zur Information Flow Control und Manipulationsprüfung zu machen. Dazu muss nicht nur das Konzept von Sicherheitsstufen explizit eingeführt, die Algorithmik verbessert und der Sprachumfang erweitert werden; es sollen auch dynamische Informationen zur a-posteriori Rekonstruktion von Sicherheitsverletzungen eingehen und temporale Logik zur a-priori Prüfung dynamischer Aspekte. Die Anwendung auf reale sicherheitskritische Software wird in Kooperation mit dem IBM T.j. Watson Lab erfolgen.

• DFG-Verfahren: Sachbeihilfen