Project Lead: Prof. Dr. Heiko Mantel
Information-flow control is the basis for a property-centric and semantically well-founded approach to IT security. Moreover, the existence of compositionality results makes information-flow properties promising candidates for end-to-end security guarantees for complex software systems, i.e., for security in the large. The conceptual complexity of concurrent systems makes it particularly desirable to obtain reliable security guarantees. However, securing the information flow in concurrent systems has proven to be non-trivial. Existing program-analysis techniques do not cover the full spectrum of relevant concurrency features. Moreover, information-flow analyses for concurrent programs are usually less satisfactory wrt. precision, adequacy or efficiency than their counterparts for sequential programs. RSCP will address the current problems with information-flow security in concurrent systems. It aims at a novel framework for adequately characterising security aspects by noninterference-like information-flow properties as well as for analysing and certifying the security of concurrent programs based on well-founded semantics. In the first period of RS3, the focus shall be on improving the coverage of concurrency features, of security policies, and of run-time environments.
Modern multi-core processors support weak memory models to permit the effective use of optimizations. That is, they provide relaxed consistency guarantees compared to sequential consistency. We studied the effects of weak memory models on possibilistic noninterference.
For our research, we developed an execution model that is parametric in the relaxations of sequential consistency that a memory model provides and instantiated this framework for the four memory models sequential consistency, IBM 370, total store order, and partial store order.
Based on these four instantiations we showed that a program that satisfies possibilistic noninterference under one of these four memory models does not necessarily satisfy possibilistic noninterference under the other three memory models. This result suggests that research on information-flow security should pay more attention to the concrete hardware on which programs run.
We also developed a security type system that inserts fences into a program to soundly enforce noninterference under all four memory models. Unlike other fence insertion techniques, our security type system does not enforce sequentially consistent behavior. Hence, the resulting program can still benefit from performance gains due to permitted relaxations of a weak memory model.
We developed a novel style for verifying information-flow security in a compositional manner. Our approach [MSS11] draws inspiration from rely-guarantee-style reasoning, which is popular for verifying conventional system properties. To our knowledge, this is the first time that this style of reasoning could be adapted to an information-flow analysis for concurrent programs.
Our approach to rely-guarantee-style reasoning allows one to exploit information about the synchronisation between threads to improve the precision of an information-flow analysis. A distinctive feature of this approach is that it does not prescribe the use of particular synchronisation primitives. This makes our approach compatible with different languages and different styles of concurrent programming.
We also provide a completely machine-checked formalization in the interactive theorem prover Isabelle/HOL of our rely-guarantee-style reasoning:
An Isabelle/HOL Formalization of Assumptions and Guarantees for Compositional Noninterference
The controlled declassification of secrets has received much attention in research, though mostly for sequential programs. In [LMP12], we propose a novel security property WHAT&WHERE that aims at controlling what secrets may be declassified where in a multi-threaded program. This is non-trivial, since further, subtle information leaks can occur. In particular, information can be leaked via scheduling. We show that WHAT&WHERE adequately characterizes controlled declassification of secrets independent of the scheduler under which a program is executed and present a security type system that enforces the property.
We also provide a completely machine-checked formalization in the interactive theorem prover Isabelle/HOL of parts of [LMP12]:
An Isabelle/HOL Formalization of Declassification with WHAT&WHERE security
Modern Android smartphones are often entrusted with various private data of their user, such as contact information, appointments, passwords, and more. To protect such data, the Android operating system provides a mechanism for restricting access to it: the Android permission system. An app may only access a specific source of private information if it was granted the appropriate permission at the time of the app's installation. Yet, once an app has legitimate access to private sources and to untrusted sinks of information, it remains concealed whether the app respects the privacy of entrusted information or whether the app leaks the information to untrusted information sinks.
Cassandra [LMSBS14] aims at increasing the transparency of how private information flows through Android apps and, thus, supporting the user of Android mobile devices to install apps only if they adhere to their personal information-flow requirements.
The functionality of Cassandra resembles that of regular app stores for Android with respect to browsing and installing apps. Beyond this functionality, Cassandra allows its user to specify information-flow requirements and to analyze whether selected apps adhere to these requirements prior to their installation. As result of the analysis, Cassandra offers its user detailed reports about potential information leaks that violate the specified information-flow requirements. Thus, Cassandra allows its user to make an informed decision on whether to install an app or not.
The analysis method employed by Cassandra as well as a proof of its soundness with respect to a declarative information-flow property is presented in [LMSW2014]. Sources and sinks of private information that are relevant for the speficiation of information-flow requirements are explained in the paper [MS12]. The video below shows the application of Cassandra at the example of the app "Minute Man", which reveals a leak of private information in the app.