Evaluation of Jif and Joana as Information Flow Analyzers in a Model-Driven Approach

摘要

Checking for information leaks in real-world applications is a difficult task. IFlow is a model-driven approach which allows to develop information flow-secure applications using intuitive modeling guidelines. It supports the automatic generation of partial Java code while also providing the developer with the ability to formally verify complex information flow properties. To simplify the formal verification, we integrate an automatic Java application information flow analyzer, allowing to check simple noninterference properties. In this paper, we evaluate both Jif and Joana as such analyzers to determine the best suiting information flow control tool in the context of, but not limited to the IFlow approach.