Software-Manipulationsprüfung
Final Report Abstract
Ziel dieses Projekts war die Entwicklung eines Verfahrens, das es ermöglicht, realistische Programme in realistischen Programmiersprachen auf Informationslecks zu untersuchen. Das Verfahren beruht auf Programmabhängigkeitsgraphen, Slicing und Pfadbedingungen und hat damit gegenüber den existierenden Typsystem-basierten Verfahren (wie etwa Jif) folgende Vorteile: Es ist deutlich präziser, kann auf existierende Sprachen angewandt werden, benötigt weniger Benutzerannotationen und kann durch die Pfadbedingungen konkrete Szenarien für gemeldete Informationslecks und Manipulationswege aufzeigen. Am Ende des Projekts steht ein praktisch einsetzbares, zuverlässiges und automatisches Tool zur Informationsflusskontrolle für C und Java. Wir besitzen mittlerweile je eine Datenflussanalyse für Ansi C und volles Java, die kontext, fluss-, objekt- und feldsensitive PDGs für Programme mit bis zu 30.000 LOC erzeugen können. Dadurch konnten wir den Anwendungsbereich deutlich erweitern: Hatten wir uns bis 2006 auf JavaCard-Programme für Smart Cards fokussiert, werden nun auch typische JavaME-Programme für mobile Geräte problemlos analysiert. Wir haben präzise Slicing- und Chopping-Algorithmen für Java Threads entwickelt und implementiert, und sind zurzeit eine der wenigen Einrichtungen weltweit, die eine solche Implementierung besitzen. Insbesondere sind wir bei Java in der Lage, Nebenläufigkeit und Exceptions präzise zu modellieren. Für Java-Pfadbedingungen wurde eine erste Implementierung realisiert. Aufbauend auf diesen Technologien verfügen wir über den weltweit ersten Slicing-basierten IFC-Algorithmus, der beliebige Sicherheitsverbände sowie Deklassifikationen erlaubt. Bis auf die Pfadbedingungen wurden diese Verfahren in einem Eclipse-Plugin integriert und können dort bequem über eine graphische Oberfläche verwendet werden. Unsere Evaluierungen zeigen, dass dieses Verfahren für mittelgroße Programme praktikabel ist: Es sind nur wenige Benutzerannotationen nötig und die Laufzeit beträgt bis zu wenigen Minuten. Bei den temporalen Pfadbedingungen mussten wir hingegen feststellen, dass sie sich nicht einfach in die bisherige Infrastruktur zu Pfadbedingungen integrieren lassen. Eine prototypische Implementierung zeigte aber, dass die automatische Berechnung von Zeugen für Informationslecks und Manipulationslecks mit diesen Pfadbedingungen durch den Einsatz moderner Model Checker wesentlich einfacher wird. Eine vollständige Neuimplementierung für Pfadbedingungen einschließlich des Korrektheitsbeweises soll im Rahmen eines neuen Antrags im SPP Zuverlässig sichere Software“ entwickelt werden. Die Ergebnisse wurden in hochkarätigen internationalen Journalen publiziert, und das Projekt trug mit zur erfolgreichen Gründung des neuen SPP 1496 "Zuverlässig sichere Software“ bei. Die vorhandene Implementierung muss allerdings als Forschungsprototyp betrachtet werden, die von einem Produkt noch recht weit entfernt ist.
Publications
- Advanced Slicing of Sequential and Concurrent Programs. PhD Thesis, Universität Passau, Fak. f. Mathematik u. Informatik 2003
J. Krinke
- Context-sensitive slicing of concurrent programs. Proc. ESEC/FSE’03, pages 178–187. ACM Press, 2003
J. Krinke
- An improved slicer for Java. Proc. PASTE’04, pages 17–22. ACM Press, 2004
C. Hammer and G. Snelting
- Pfadbedingungen in Abhängigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik Dissertation, Universitat Passau, Fakultät für Informatik und Mathematik, 2005
T. Robschink
- Efficient Path Conditions in Dependence Graphs for Software Safety Analysis. ACM Transactions on Software Engineering and Methodology 15(4):410-457, 2006
G. Snelting, T. Robschink and J. Krinke
- On Temporal Path Conditions in Dependence Graphs. 7th IEEE Working Conference on Source Code Analysis and Manipulation (SCAM 2007), pages 49–58, 2007
A. Lochbihler and G. Snelting
- Precise Analysis of Java Programs using JOANA (Tool Demonstration). 8th IEEE International Working Conference on Source Code Analysis and Manipulation, pages 267–268, 2008
D. Giffhorn and C. Hammer
- Static Path Conditions for Java. Proc. of the 3rd Workshop on Programming Languages and Analysis for Security, pages 55–66, 2008
C. Hammer, R. Schaade and G. Snelting
- Chopping Concurrent Programs. Proc of the 9th IEEE International Working Conference on Source Code Analysis and Manipulation, pages 13–22, 2009
D. Giffhorn
- Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. International Journal of Information Security 8(6):399-422, 2009
C. Hammer and G. Snelting
- Improving and Evaluating the Scalability of Precise System Dependence Graphs for Objectoriented Languages. Technical Report, Universität Karlsruhe (TH), Fak. f. Informatik
J. Graf
- Information Flow Control for Java - A Comprehensive Approach based on Path Conditions in Dependence Graphs. PhD Thesis, Universitätsverlag Karlsruhe, ISBN 978-3-86644-398-3, Universität Karlsruhe (TH), Fak. f. Informatik 2009
C. Hammer
- On Temporal Path Conditions in Dependence Graphs. Journal of Automated Software Engineering, pages 263–290, 2009.
A. Lochbihler and G. Snelting
- Precise slicing of concurrent programs - An evaluation of static slicing algorithms for concurrent programs. Journal of Automated Software Engineering, 16(2):197-234, 2009
D. Giffhorn and C. Hammer
