Developing Systems with Secure Information Flow
|Funded by:||DFG (Deutsche Forschungsgemeinschaft)|
|Local project leader:||Kuzman Katkalov|
Dr. Gerhard Schellhorn
Prof. Dr. Wolfgang Reif
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.
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.
The following slides also give an overview of the IFlow approach.
We evaluate our approach with different case studies with different features.