Formal Verification of Information Flow Secure Systems with IFlow

This report presents an approach called IFlow which allows the model-driven development of secure systems regarding information flow. The approach focuses on the application domain of mobile applications and web services. A developer starts by creating an abstract UML model of a system where he can additionally specify information flow properties the system must satisfy. From the model, Java code is generated together with an information flow policy that can be checked by automated analysis tools like Jif or Joana. In addition, the UML model is transformed into a formal specification which is the basis for formal reasoning within our formal framework including the interactive theorem prover KIV. While automated tools are designed for the simple property of noninterference, formal verification allows to express more complex properties. In order that the results of verification can be carried to the code level and that the results of automated code analysis can be used as lemmas for formal verification, an information flow-preserving refinement relation is established between the formal specification and the code. The focus of this report is on the aspects of formal verification