HOME | DEUTSCH | IMPRESSUM | KIT

JOANA (Java Object-sensitive ANAlysis) - Information Flow Control Framework for Java

JOANA analyses Java programs for security leaks (Information Flow Control, IFC). It guarantees to find all violations of integrity or confidentiality – that is, all leaks which result from illegal information flow within a program. JOANA analyses up to 100kLOC of full Java with arbitrary threads (without reflection).

JOANA is one of the few internationally available tools which can handle full Java and guarantees to find all leaks inside programs. JOANA thus complements other techniques such as access control, certificates, or intrusion detection.

JOANA Logo

Technology

JOANA is based on a stack of sophisticated program analysis techniques, such as pointer analysis, exception analysis, and program dependence graphs. Technically, these techniques are flow-sensitive, context-sensitive, object-sensitive, and lock-sensitive, which means that JOANA minimizes false alarms. JOANA includes a new “RLSOD” algorithm for finding all probabilistic leaks; these malicious leaks result from subtle interactions between threads and interleaving. JOANA comes with a machine-checked soundness proof.

JOANA is open source, needs few program annotations and comes as Eclipse plug-in, providing a nice GUI.

Further reading

An overview of JOANA can be found in Checking Probabilistic Noninterference Using JOANA, a practical guide can be found in Using JOANA for Information FlowControl in Java Programs, while X-Rays,not Passport checks - Information Flow Control using JOANA provides an overview presentation.

In-depth technical descriptions can be found in the articles Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs
and A New Algorithm for Low-Deterministic Security.

Work on JOANA has been partly supported by the DFG-funded SPP 1496 "Reliably Secure Software Systems – RS3" and the BMBF-funded competence center for applied IT security technology KASTEL.

JOANA builds upon the WALA program analysis framework.

Information flow control for Java in a nutshell

Joana in a nutshell.

Information flow control is concerned with the security of information inside a program. It covers confidentiality as well as integrity. Confidentiality describes the property that sensitive information, like passwords or personal data, is not leaked to public visible channels. Integrity, the dual property to confidentiality, guarantees that untrusted input is not able to alter sensitive data or influence critical computations inside the program.

JOANA is a framework that allows to statically analyze a given Java program for integrity and confidentiality. Therefore the user has to provide annotations describing which parts of the program correspond to sensitive (high) information, e.g. a variable storing a password, and where untrusted (low) input or output occurs, e.g. calls to readln or println. The user can also specifiy declassification annotations, when the security level of certain information needs to be lowered. E.g. when a password is encrypted, it technically contains the same information as the unencrypted value, but it does not require the same amount of caution.

JOANA builds a system dependence graph (SDG) from the program source. This graph is an overapproximation of the information flow inside the program. It contains nodes for each statement (resp. expression) and edges between them iff the outcome of one statement depends on the execution of the other. These dependencies do not only cover direct dependencies through values, known as data dependencies; they also cover indirect dependencies, called control dependencies. Control dependencies arise when the outcome of a statement decides if another statement is executed, for example the condition of an if-clause decides which statement is executed next. JOANA is based on a machine-checked proof that any information flow is only possible along realizable paths in the SDG.

JOANA analyzes the information flow inside the program through graph based analyses, like slicing and chopping, on the system dependence graph. If no path inside the SDG is found that corresponds to illegal flow, the program is guaranteed to be secure. On the other hand if a violating path exists, it may be a real security leak, but in some cases it could also be a false alarm that stems from an overapproximation in the analysis.

Features of JOANA

  • Support for full Java bytecode (excluding Reflection).
  • Minimize false alarms through precise object-, flow-, context- and field-sensitive program analysis techiques.
  • Analysis of multithreaded programs: Detect possibilistic and probabilistic leaks.
  • Minimal user interaction required: Automated propagation of security labels, only few annotations needed.
  • Declassification: The user can specify points in the program where the security level of information should be lowered.

Web Start Applications

These applications are also part of the source release of JOANA. They are additionally provided as Web Start applications for convenience. However they may not always be the latest version.

Application Run Web Start Download .jnlp file
IFC Console
joana-ifcconsole.jnlp
GraphViewer
joana-graphviewer.jnlp

JOANA Source Code

JOANA source code on GitHub

Bug Tracker

In case you find some bugs in our tools, feel free to report them to us through our bug tracker: Joana Bug Tracker. Keep in mind that our programs are research prototypes, so please be forgiving.

Contact

Please contact Martin Mohr <martin.mohr@kit.edu>, Martin Hecker <martin.hecker@kit.edu> or Jürgen Graf <graf@kit.edu> for further information about this project.

Research Cooperation

JOANA is used in research projects outside of the programming paradigms group. We cooperate with the following projects and research groups:

Related Projects

Joana has been developed as part of the projects: Visit these projects sites for further information about publications and technical details.

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