Future software sytems will be dynamically configured from mobile components, and will
heavily use parallellism. Security checks thus have to deal precisely with mobile software
components and their plug-in, as well as with parallel constructs and multi-threaded programs.
Current information Flow algorithms for mobile components and multi-threaded software can
be greatly improved if they leverage modern program analysis.
In this project, we use information Flow control based on program dependence graphs
for the construction of new and precise security analysis
methods for mobile components and their dynamic integration, as well as for their concurrent
interaction. New theoretical insights into the analysis of parallel programs and invariance
detection (as developed at the Software Construction and Verification Group headed by Prof. Dr. Markus Müller-Olm) will improve analysis precision in particular for
information Flow in parallel programs. New techniques for context approximation and context
inference allow to construct modular dependence graphs and handle missing application
contexts for isolated components. A scaling implementation for full Java is being developed
and exercised on realistic case studies.
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.
| 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, 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.
|
|
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 |
|
A. Lochbihler:
Making the Java Memory Model Safe.
TOPLAS 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 |
|
A. Lochbihler:
Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler.
LNI - Ausgezeichnete Informatikdissertationen 2012 |
| 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.
|
|
A. Lochbihler:
Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation.
ESOP 2012 |
|
R. Küsters, T. Truderung, J. Graf:
(accompanying technical report) A Framework for the Cryptographic Verification of Java-like Programs.
|
|
A. Flexeder, M. Müller-olm, M. Petter, H. Seidl:
Fast interprocedural linear two-variable equalities.
|
|
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 |
|
T. Gawlitza, P. Lammich, M. Müller-Olm, H. Seidl, A. Wenner:
Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation.
|
|
M. D. Schwarz, H. Seidl, V. Vojdani, P. Lammich, M. Müller-Olm:
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.
|
| 2010 |
|
D. Wasserrab:
From Formal Semantics to Verified Slicing - A Modular Framework with
Applications in Language Based Security.
Ph.D. thesis |
|
M. Taghdiri, G. Snelting, C. Sinz:
Information Flow Analysis via Path Condition Refinement.
FAST 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 |
|
C. Hammer:
Information Flow Control for Java - A Comprehensive Approach based
on Path Conditions in Dependence Graphs.
Ph.D. thesis |
|
D. Wasserrab, D. Lohner, G. Snelting:
On PDG-Based Noninterference and its Modular Proof.
PLAS 2009 |
|
P. Lammich, M. Müller-Olm, A. Wenner:
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
|
| 2008 |
|
C. Hammer, R. Schaade, G. Snelting:
Static Path Conditions for Java.
PLAS 2008 |
|
P. Lammich, M. Müller-Olm:
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
|
| 2007 |
|
M. Müller-Olm, H. Seidl:
Analysis of modular arithmetic.
|
|
P. Lammich, M. Müller-Olm:
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.
|
| 2006 |
|
C. Hammer, J. Krinke, G. Snelting:
Information Flow Control for Java Based on Path Conditions in Dependence
Graphs.
ISSSE 2006 |
|
M. Müller-Olm:
Variations on Constants: Flow Analysis of Sequential and Parallel Programs (Lecture Notes in Computer Science).
|
| 2005 |
|
A. Bouajjani, M. Müller-Olm, T. Touili:
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems.
|
| 2004 |
|
M. Müller-Olm:
Precise interprocedural dependence analysis of parallel programs.
|
|
M. Müller-Olm, H. Seidl:
Precise interprocedural analysis through linear algebra.
|
| 2001 |
|
M. Müller-Olm, H. Seidl:
On optimal slicing of parallel programs.
|
