|
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. |
 |
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
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 7 bytecode (excluding Reflection), works on Java 8 JVMs.
- 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.
Obtaining Joana
Joana can be used with the following applications The annotations used by Joana can be found at Maven Central.JOANA Source Code
Bug Tracker
In case you find some bugs in our tools, feel free to report them to us through the GitHub bug tracker. Keep in mind that our programs are research prototypes, so please be forgiving.
Contact
Please contact Simon Bischof <simon.bischof@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:
- Implementation-Level Analysis of E-Voting Systems (Ralf Küsters, University of Trier): Analysis of e-voting systems and IFC treatment of crypted messages
- Program-level Specification and Deductive Verification of Security Properties - DeduSec (Bernhard Beckert, KIT): Integration of KeY and JOANA
- System-wide data-driven runtime usage control across layers of abstraction - SADAN (Alexander Pretschner, TU Munich): Improvement of run-time usage control with static JOANA information
- Static code analysis for securing Cordova applications (Achim Brucker, SAP)
- Secure Type Systems and Deduction - SecDed (Tobias Nipkow, TU Munich) provides Isabelle support for the machine-checked verification of JOANA's IFC machinery
- Cyber Security Lab (Christian Hammer, Saarland University / CISPA) on the use of Android front for program Analysis using WALA
- Developing Systems with Secure Information Flow - IFlow
(Wolfgang Reif, University of Augsburg)
uses JOANA as IFC tool
Related Projects
Joana has been developed as part of the projects:- VALSOFT/Joana
- IFC for Mobile Components (together with Markus Müller-Olm, University of Münster)