Informationsflusskontrolle mit Programmabhängigkeitsgraphen

Um sicherheitsrelevante Software zu überprüfen, reichen herkömmliche Softwareanalyse-Verfahren nicht aus. Unser Softwareanalyse-System ValSoft/Joana setzt Datenflussanalysen und deduktive Verfahren ein, um Beeinflussungen von relevanten Informationspfaden innerhalb von Programmen zu erkennen und zu analysieren.

Dieses Projekt beschäftigt sich mit der Entwicklung von Verfahren, mit denen Informationslecks in sicherheitskritischer Software aufgedeckt werden können. Ziel ist es, Verfahren zur entwickeln, die

• Sicherheit garantieren, d.h. kein Informationsleck übersehen
• für gängige Sprachen einsetzbar sind, wie etwa für C oder Java
• größere Softwaresysteme mit akzeptablem Aufwand analysieren können
• größtmögliche Präzision bieten, d.h. sehr wenige Fehlalarme generieren

Die Grundlage der Analyse bilden sog. Programmabhängigkeitsgraphen. Diese spiegeln den möglichen Informationsfluss innerhalb des Programms präzise wider. Um den Informationsfluss zu klassifizieren, werden den Daten, sowie den Benutzerschnittstellen, Sicherheitsstufen zugewiesen. Mittels einer Datenflussanalyse auf dem Programmabhängigkeitsgraphen berechnet ValSoft/Joana dann, ob Daten einer bestimmten Sicherheitsstufe an unbefugte Benutzer des Systems gelangen können. Findet diese Analyse ein mögliches Informationsleck, kann dieses durch sog. Pfadbedingungen weiter untersucht werden: Pfadbedingungen geben die genauen Umstände an, unter denen es einen Informationsfluss zwischen zwei gegebenen Punkten im Programm geben kann.

Das Projekt bietet momentan die folgende Funktionalität:

• Aufbau von Programmabhängigkeitsgraphen für C- und Java-Programme sowie deren Sicherheitsanalyse
• Berechnung von Pfadbedingungen für C- und Java-Programme
• Bedienung der Analyse und Visualisierung der Analyseergebnisse in der IDE Eclipse. Unzulässiger Datenfluss wird im Programmtext direkt markiert.

Gefördert durch die DFG. Früher gefördert durch das BMBF im Rahmen der »Initiative zur Förderung der Softwaretechnologie in Wirtschaft, Wissenschaft und Technik.«

Frühe Arbeiten wurden an der Universität Passau, sowie an der Technischen Universität Braunschweig in Kooperation mit der Physikalisch-Technischen Bundesanstalt und der Firma LINEAS durchgeführt.

Forschungs Prototypen

Das JOANA Informations Fluss Framework für Java Programme ist unter der Seite http://joana.ipd.kit.edu/ frei verfügbar.

Die non-interference Analyse der Client-Server Beispielanwendung aus dem CSF 2012 Paper ist aut GitHub unter https://github.com/jgf/crypto-client-ifc verügbar. Es ist zudem eine einfache Schnittstelle zu unseren IFC Tools (Joana) enthalten. So ist es möglich seine eigenen Beispielanwendung damit zu testen.

Projektbeteiligte

Lehrstuhlinhaber
Prof. Gregor Snelting

Ehemalige Mitarbeiter
Prof. Dr.-Ing. Christian Hammer
Prof. Dr. Jens Krinke
Dr.-Ing. Dennis Giffhorn
Dr.-Ing. Jürgen Graf
Dr.-Ing. Martin Hecker
Dr. rer. nat. Andreas Lochbihler
Dr.-Ing. Martin Mohr
Dr. rer. nat. Torsten Robschink

Veröffentlichungen

2022
M. Hecker, S. Bischof, G. Snelting: On Time-Sensitive Control Dependencies. TOPLAS 2022
2020
F. D. Loch, M. Johns, M. Hecker, M. Mohr, G. Snelting: Hybrid Taint Analysis for Java EE. SAC 2020
2018
S. Bischof, J. Breitner, D. Lohner, G. Snelting: Illi Isabellistes Se Custodes Egregios Praestabant.
S. Bischof, J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting: Low-Deterministic Security For Low-Nondeterministic Programs. JCS
B. Beckert, S. Bischof, M. Herda, M. Kirsten, M. K. Büning: Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control. ICFEM 2018
2017
B. Beckert, S. Bischof, M. Herda, M. Kirsten, M. K. Büning: Combining Graph-Based and Deduction-Based Information-Flow Analysis. HOTSPOT 2017
2016
J. Graf: Information Flow Control with System Dependence Graphs -- Improving Modularity, Scalability and Precision for Object Oriented Languages.
M. Wiesner: Intent-Analyse von Android-Applikationen.
J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting: On Improvements Of Low-Deterministic Security. POST 16
J. Graf, M. Hecker, M. Mohr, G. Snelting: Sicherheitsanalyse mit JOANA. Sicherheit 2016
J. Graf, M. Hecker, M. Mohr, G. Snelting: Tool Demonstration: JOANA. POST 16
2015
R. Küsters, T. Truderung, B. Beckert, D. Bruns, M. Kirsten, M. Mohr: A Hybrid Approach for Proving Noninterference of Java Programs. CSF 2015
J. Graf, M. Hecker, M. Mohr, G. Snelting: Checking Applications using Security APIs with JOANA. ASA 2015
G. Snelting: Understanding Probabilistic Software Leaks. SCP 2015
D. Giffhorn, G. Snelting: A new algorithm for low-deterministic security. IJIS
M. Mohr, J. Graf, M. Hecker: JoDroid: Adding Android Support to a Static Information Flow Control Tool.
E. Lovat, A. Fromm, M. Mohr, A. Pretschner: SHRIFT System-Wide HybRid Information Flow Tracking. IFIPSec 2015
2014
G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, D. Wasserrab: Checking Probabilistic Noninterference Using JOANA. IT 2014
R. Küsters, E. Scapin, T. Truderung, J. Graf: Extending and Applying a Framework for the Cryptographic Verification of Java Programs. POST 14
R. Küsters, E. Scapin, T. Truderung, J. Graf: (accompanying technical report) Extending and Applying a Framework for the Cryptographic Verification of Java Programs..
2013
R. Küsters, T. Truderung, B. Beckert, D. Bruns, J. Graf, C. Scheben: A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs. GRSRD 2013
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. ATPS 2013
J. Graf, M. Hecker, M. Mohr, B. Nordhoff: Lock-sensitive Interference Analysis for Java: Combining Program Dependence Graphs with Dynamic Pushdown Networks. ID 2013
2012
R. Küsters, T. Truderung, J. Graf: A Framework for the Cryptographic Verification of Java-like Programs. CSF 2012
D. Giffhorn, G. Snelting: Probabilistic Noninterference Based on Program Dependence Graphs.
R. Küsters, T. Truderung, J. Graf: (accompanying technical report) A Framework for the Cryptographic Verification of Java-like Programs.
D. Giffhorn: Slicing of Concurrent Programs and its Application to Information Flow Control.
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide.
2011
D. Giffhorn: Advanced chopping of sequential and concurrent programs. SQJ
2010
M. Taghdiri, G. Snelting, C. Sinz: Information Flow Analysis via Path Condition Refinement. FAST 2010
J. Graf: Speeding up context-, object- and field-sensitive SDG generation. SCAM 2010
B. Katz, M. Krug, A. Lochbihler, I. Rutter, G. Snelting, D. Wagner: Gateway Decompositions for Constrained Reachability Problems. SEA 2010
C. Hammer: Experiences with PDG-based IFC. ESSoS'10
2009
C. Hammer, G. Snelting: Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. IJIS
D. Giffhorn: Chopping Concurrent Programs. SCAM 2009
C. Hammer: Information Flow Control for Java - A Comprehensive Approach based on Path Conditions in Dependence Graphs. Ph.D. thesis
A. Lochbihler, G. Snelting: On Temporal Path Conditions in Dependence Graphs. JASE
D. Giffhorn, C. Hammer: Precise Slicing of Concurrent Programs - An Evaluation of Static Slicing Algorithms for Concurrent Programs. JASE
J. Graf: Improving and Evaluating the Scalability of Precise System Dependence Graphs for Objectoriented Languages.
2008
C. Hammer, G. Snelting: Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs.
D. Giffhorn, C. Hammer: Precise Analysis of Java Programs using JOANA (Tool Demonstration). SCAM 2008
C. Hammer, R. Schaade, G. Snelting: Static Path Conditions for Java. PLAS 2008
2007
D. Giffhorn, C. Hammer: An Evaluation of Slicing Algorithms for Concurrent Programs. SCAM 2007
A. Lochbihler, G. Snelting: On Temporal Path Conditions in Dependence Graphs. SCAM 2007
2006
C. Hammer, J. Krinke, F. Nodes: Intransitive Noninterference in Dependence Graphs. ISoLA 2006
G. Snelting, T. Robschink, J. Krinke: Efficient Path Conditions in Dependence Graphs for Software Safety Analysis. TOSEM 2006
C. Hammer, J. Krinke, G. Snelting: Information Flow Control for Java Based on Path Conditions in Dependence Graphs. ISSSE 2006
C. Hammer, M. Grimme, J. Krinke: Dynamic Path Conditions in Dependence Graphs. PEPM 2006
2005
C. Hammer: Parallelitätsanlayse für Slicing von Java Threads. WSR 2005
G. Snelting: Quantifier Elimination and Information Flow Control for Software Security. A3L 2005
T. Robschink: Pfadbedingungen in Abhängigkeitsgraphen und ihre Anwendung in der Softwaresicherheitstechnik.
2004
C. Hammer, G. Snelting: An Improved Slicer for Java. PASTE 2004
2003
J. Krinke: Barrier Slicing and Chopping. SCAM 2003
J. Krinke: Context-Sensitive Slicing of Concurrent Programs. FSE 2003
J. Krinke: Advanced Slicing of Sequential and Concurrent Programs.
2002
J. Krinke: Evaluating Context-Sensitive Slicing and Chopping. ICSM 2002
T. Robschink, G. Snelting: Efficient Path Conditions in Dependence Graphs. ICSE 2002
1999
J. Krinke, T. Robschink, G. Snelting: Software-Sicherheitsprüfung mit VALSOFT. IFE 1999
1998
J. Krinke, G. Snelting: Validation of Measurement Software as an Application of Slicing and Constraint Solving. IST 1998
J. Krinke: Static Slicing of Threaded Programs. PASTE 1998
J. Krinke, G. Snelting, T. Robschink: Software-Sicherheitsprüfung mit VALSOFT. ST 1998
1996
G. Snelting: Combining Slicing and Constraint Solving for Validation of Measurement Software. SAS 1996