ISSE

Search

IFlow


iflow-hand-small

Developing Systems with Secure Information Flow

Start date: 01.10.2010
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local project leader: Kuzman Katkalov
Local scientists: Dr. Kurt Stenzel
Dr. Gerhard Schellhorn
Marian Borek
Prof. Dr. Wolfgang Reif
Publications: Publication list

Abstract

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 desktop computers 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.

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

iflow-hand
The future of information flow.

 

Approach

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

Presentation

The following slides also give an overview of the IFlow approach.

Case Studies

We evaluate our approach with different case studies with different features.

  • Our running example is the Travel Planner. It consists of two apps (a travel planner and a credit card center), a travel agency as a web service, and an airline web service. The example uses explicit declassification and the most important property is that the user's credit card data only flow to the airline after confirmation, but never to the travel agency. The example contains the UML model, formal specification, and code.

  • A Simplified Travel Planner with only one app.

  • And an even more simple Travel Planner without declassification.

  • A Distance Tracker with a complex filter function and KIV proof that no GPS position of the user is uploaded to a server.

  • A Distance Tracker inspired by Heiko Mantel and his group.

  • A user-friendly Flashlight app.

  • A Simple Search app with parameterized domains (one domain for every user or app instance).

  • A Toy banking example with parameterized domains (one domain for every user or app instance).

  • The KIV formalization of various noninterference theories is not an IFlow case study, but a collection of specifications and proofs of several unwinding theorems. The specifications on the left side of the project graph named MAKS-BSD and MAKS-BSRA formalize and prove two definitions and unwinding theorems by Heiko Mantel (backward strict delete and backward strict replace all). The specifications somewhere in the middle named MeydenIntrans and MeydenTrans contain Rushby's intransitive and transitive noninterference definitions and unwinding theorems with improvements by van der Meyden. Specifications LanguageBasedNIFIntrans and LanguageBasedNIFTrans add domains to locations and contain theorems stating that in a system fulfilling the unwinding conditions and some other conditions "low" locations remain unchanged. These properties are similar to the usual definition of language-based noninterference. Other specifications contain variations of the mentioned definitions and/or unwinding theorems (e.g. with or without a fixed initial state, or with or without an invariant for all states). An IFlow formal model is an instance of the MeydenIntrans specification.

Selected publications

  • A Model-Driven Approach to Noninterference.
    Kurt Stenzel and Kuzman Katkalov and Marian Borek and Wolfgang Reif
    Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), volume 5, number 3, pages 30-43, 2014. Link
  • Formalizing information flow control in a model-driven approach.
    Kurt Stenzel, Kuzman Katkalov, Marian Borek, and Wolfgang Reif.
    Information Communication Technology-EurAsia (ICT-EurAsia) 2014. Springer LNCS 8407, 2014. Springerlink, preliminary version.
  • Model-Driven Development of Information Flow-Secure Systems with IFlow
    Kuzman Katkalov, Kurt Stenzel, Marian Borek, and Wolfgang Reif.
    ASE Science Journal Vol.2, No 2 (2013) Link
  • Evaluation of Jif and Joana as information flow analyzers in a model-driven approach.
    Kuzman Katkalov, Peter Fischer, Kurt Stenzel, Nina Moebius, and Wolfgang Reif.
    Data Privacy Management and Autonomous Spontaneous Security 2012 (DPM). Springer LNCS 7731, 2013. Springerlink

Links: