HOME | DEUTSCH | IMPRESSUM | KIT

IFC for Mobile Components

Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs

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 Project IFC for Mobile Components is a joint project by Gregor Snelting and Markus Müller-Olm (Westfälische Wilhelms-Universität Münster).
It is funded by the DFG, as part of the Priority Programme 1496 “Reliably Secure Software Systems – RS3”

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

Partner
Prof. Markus Müller-Olm
Benedikt Nordhoff
Alexander Wenner
Department Head
Prof. Gregor Snelting
Scientific Staff
Jürgen Graf
Martin Hecker
Martin Mohr

Publications

2016
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: Tool Demonstration: JOANA. POST 16
J. Graf, M. Hecker, M. Mohr, G. Snelting: Sicherheitsanalyse mit JOANA. Sicherheit 2016
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
R. Küsters, T. Truderung, B. Beckert, D. Bruns, M. Kirsten, M. Mohr: A Hybrid Approach for Proving Noninterference of Java Programs. CSF 2015
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.

 

rs3-logo  wwu-logo  dfg-logo