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.
We developed a novel style for verifying information-flow security in a compositional manner. Our approach  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.
The controlled declassification of secrets has received much attention in research, though mostly for sequential programs. In , 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 see information-flow analysis as a promising technology to
solve real-world security problems, and by that improve
trustworthiness of real-world systems. Leaks of users' private
information on modern smartphones is a popular, emerging
example of such problems. We applied techniques for static
information-flow analysis to identify privacy leaks in Android
We crafted a type-based framework which checks
prior to app installation whether the Dalvik bytecode of this app
analyzed the Android API for possible sources and sinks of
private data and identified exemplary privacy policies based on
This demo shows how our framework is applied to detect a
leak of private location data.
Prof. Dr. Bernhard Beckert,
Prof. Dr. Peter H. Schmitt, Karlsruhe Institute of Technology,
DeduSec: Program-level Specification and Deductive Verification of Security Properties
Prof. Dr. Markus Müller-Olm, WWU Münster,
IFC for Mobile Components: Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs
Prof. Tobias Nipkow, Ph.D., TU München, Secure Type Systems and Deduction
Prof. Dr. Arnd Poetzsch-Heffter, TU Kaiserslautern, MoVeSPAcI: Modular Verification of Security Properties in Actor Implementations
11th International Conference on Mathematics of Program Construction (MPC).
Alexander Lux, Heiko Mantel and Matthias Perner. Springer, 2012. (to appear)
[ BibTeX entry | PDF | Proofs ]
A Framework for Static Detection of Privacy Leaks in Android Applications.
27th Symposium on Applied Computing (SAC): Computer Security Track.
Christopher Mann and Artem Starostin. 2012.
[ BibTeX entry | PDF | ACM ]
Assumptions and Guarantees for Compositional Noninterference.
24th IEEE Computer Security Foundations Symposium (CSF).
Heiko Mantel, David Sands and Henning Sudbrock. pages 218-232. IEEE Computer Society, 2011.
RS3 best-paper award (category: theory)
[ BibTeX entry | PDF | Proofs and Addendum ]
 A Static Framework for Privacy Analysis of Android Applications (Bachelor Thesis).
Christopher Mann. TU Darmstadt, 2011.
[ BibTeX entry ]
 Report on the RS3 Topic Workshop "Security Properties in Software Engineering".
Martin Ochoa, Sebastian Pape, Thomas Ruhroth, Barbara Sprick, Kurt Stenzel and Henning Sudbrock. TU Darmstadt, Technical Report 2012-02, Universität Augsburg, 2012.
[ PDF ]