HOME | DEUTSCH | IMPRESSUM | KIT

VALSOFT/Joana

Information Flow Control in Program Dependence Graphs

When verifying software for security, traditional software analysis methods are often insufficient. Our software analysis system ValSoft/Joana uses dataflow-analysis and deductive methods to detect and analyze relevant information flow in programs.

This project develops techniques that detect all illicit information flow in security relevant software. Our goal is to develop analyses that

  • guarantee security, i.e. miss no information leak
  • analyze established languages, like C or Java
  • process larger software systems with acceptable effort
  • offer maximal precision, such that very few false alarms are generated

Program dependence graphs form the basic technology for our analyses. These graphs precisely represent all information flow within a program. To classify the sensitivity of data, input and output channels of a program are annotated with security levels. ValSoft/Joana determines using a data flow analysis on the program dependence graph whether data of a certain security level may illicitly reach an unauthorized user of the system. If the analysis detects a possible information leak, it can be further inspected with path conditions: Path conditions represent the precise conditions for information flow between two given statements in a program.

The ValSoft/Joana project offers the following functionality:

  • Construction of program dependence graphs for C and Java programs, and their security analysis
  • Computation of path conditions for C and Java programs
  • User interface and visualization of results in the IDE Eclipse. Illicit data flow is highlighted directly in the source code.

Funded by DFG. Previously funded by BMBF.

Previous work was done at the University of Passau, as well as the Technical University of Braunschweig in cooperation with Physikalisch-Technischen Bundesanstalt and the company LINEAS.

Research prototypes

The JOANA information flow framework for Java programs is available for research purposes at http://joana.ipd.kit.edu/

The non-interference analysis for the client server encryption example of the CSF 2012 paper is available at https://github.com/jgf/crypto-client-ifc. It also contains a simple interface to our ifc tools (Joana), so you can try to modifiy it to analyze your own code.

Participants

Department Head
Prof. Gregor Snelting
Scientific Staff
Jürgen Graf
Martin Hecker
Martin Mohr
Former Staff Member
Prof. Dr. Jens Krinke
Jun. Prof. Dr. Christian Hammer
Dr.-Ing. Dennis Giffhorn
Dr. rer. nat. Andreas Lochbihler
Dr. rer. nat. Torsten Robschink

Publications

2015
G. Snelting: Understanding Probabilistic Software Leaks. SCP 2015
2014
D. Giffhorn, G. Snelting: A New Algorithm for Low-Deterministic Security. IJIS
G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, D. Wasserrab: Checking Probabilistic Noninterference Using JOANA. IT
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