Developing Systems with Secure Information Flow - IFlow

IFlow integrates formally verified information flow control (IFC) properties and language based type systems for IFC with a software engineering approach based on model driven development.

Description

As currently private information moves from Home-PCs to mobile devices and public platforms (e.g. Google calendar, Facebook etc.) protection of information against unintended access becomes a more and more important issue. This concerns protection against attackers (black box view), but also protection against unintended information flow between programs and devices, that are trusted for certain applications (white box view). In this project we focus on the second aspect. We will develop a new approach that integrates formally verified information flow control (IFC) properties and language based type systems for IFC with a software engineering approach based on model driven development. The approach will start with abstract UML models enhanced with application-specific specifications of information flow properties (e.g. credit card information is sent only after confirming a booking). Model to model transformations are used to get platform-specific (Java) code as well as formal models. To verify information flow properties of single programs, we will make use of automatic techniques based on type systems and abstract interpretation. The results of this analysis will be used as key lemmas to establish application-specific security properties. We will also investigate how correct programs can be integrated into a security architecture of the full system.

The project is part of the DFG Priority Programme 1496 Reliably Secure Software Systems - RS3.

(NASA/courtesy of nasaimages.org) Current state of information flow.

The future of information flow.

Approach

The developer starts by modeling the system (1) using a subset of UML extended by a UML profile. The system's structure is modeled as well as its behavior. The latter is done with a focus on the communication between different participants of the system while local functionality is modeled as a black box. The modeling guidelines enable expressing security properties that have to be satisfied by this system of multiple stakeholders. These properties talk about confidentiality of data, i.e., where information may or may not flow under certain conditions. From the UML model, partial Java code is generated (3). To obtain the fully functional Java code (4), parts of the local functionality are then programmed manually. Of course, this may not introduce new information flows which is guaranteed by an information flow aware type check.

As we want to give security guarantees beyond plain noninterference, there is another branch in the model-driven approach where the UML model is transformed into a formal model (2) suitable for our theorem prover KIV. Then it is possible to prove more specific information flow properties, e.g., that information can only flow after another action has occurred, or exactly what information flows through a declassification channel. The code must be an information flow preserving refinement of the formal model in order to ensure that formally verified properties hold for it. Then there is the additional benefit that results of the IF type check can be lifted to the formal model. However, correctly translating the results into theorems is highly non-trivial and depends on the exact behavior of the type check. In the end, a user of the application is given strong guarantees on how her personal data is treated.

Case Study

We evaluate our approach with the case study application "Travel Planner". Click here for details.

Publications

• Report on the RS3 Topic Workshop "Security Properties in Software Engineering".
  Martin Ochoa, Sebastian Pape, Thomas Ruhroth, Barbara Sprick, Kurt Stenzel, Henning Sudbrock.
  Technical Report 2012-02, Universität Augsburg, 2012; PDF
• Model-driven code generation of information flow secure systems with IFlow.
  Kuzman Katkalov, Peter Fischer, Kurt Stenzel, Wolfgang Reif.
  Technical Report 2012-04, Universität Augsburg, 2012; PDF
• Formal verification of information flow secure systems with IFlow.
  Peter Fischer, Kuzman Katkalov, Kurt Stenzel, Wolfgang Reif.
  Technical Report 2012-05, Universität Augsburg, 2012; PDF
• Formal Verification of QVT Transformations for Code Generation.
  Nina Moebius, Kurt Stenzel, Wolfgang Reif.
  Proceedings of MODELS 2011 - 14th International Conference on Model Driven Engineering Languages and Systems;
  Springer LNCS 6981
• Pitfalls in Formal Reasoning about Security Protocols
  Nina Moebius, Kurt Stenzel, Wolfgang Reif
  Proceedings of ARES 2010 - Fifth International Conference on Availability, Reliability and Security;
  IEEE Press 2010