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
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 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.
| 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 |
