Reliable Security for Concurrent Programs (RSCP)

The RSCP project is part of the DFG Priority Programme (Schwerpunktprogramm) 1496: "Reliably Secure Software Systems" (RS³).

Project Description

Project Lead: Prof. Dr. Heiko Mantel

Summary

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.

Results/Some Highlights

Rely and Guarantee

We developed a novel style for verifying information-flow security in a compositional manner. Our approach [3] 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.

Scheduler-Independent Declassification

The controlled declassification of secrets has received much attention in research, though mostly for sequential programs. In [1], 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.

A Prototype of a Certifiying App Installer

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 applications [2]. We crafted a type-based framework which checks prior to app installation whether the Dalvik bytecode of this app conforms to a specified privacy policy. We have carefully analyzed the Android API for possible sources and sinks of private data and identified exemplary privacy policies based on this. This demo shows how our framework is applied to detect a leak of private location data.

Ongoing Collaborations of the MAIS Group within RS³

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

Conference Publications with Results from RSCP

[1] Scheduler-Independent Declassification. 11th International Conference on Mathematics of Program Construction (MPC).
Alexander Lux, Heiko Mantel and Matthias Perner. Springer, 2012. (to appear)
[ BibTeX entry | PDF | Proofs ]

[2] 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 ]

[3] 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.
RS³ best-paper award (category: theory)
[ BibTeX entry | PDF | Proofs and Addendum ]

Master and Bachelor Theses on RSCP topics

[4] Toward a Framework for Soundness Proofs of Type Systems in Language-based Information-flow Security (Master Thesis).
Sylvia Grewe. TU Darmstadt. 2012
[ BibTeX entry ]

[5] Robustness of Information Flow Security Under Refinement of Synchronization Primitives (Master Thesis).
Steffen Lortz. TU Darmstadt. 2012
[ BibTeX entry ]

[6] Informationsflusssicherheit in Systemen mit zwei Prozessoren (Master Thesis).
Jens Sauer. TU Darmstadt. 2012
[ BibTeX entry ]

[7] A Static Framework for Privacy Analysis of Android Applications (Bachelor Thesis).
Christopher Mann. TU Darmstadt, 2011.
[ BibTeX entry ]

[8] Controlled Declassification under Semantics with Schedulers (Master Thesis).
Matthias Perner. TU Darmstadt, 2011.
[ BibTeX entry ]

Further RS³ Publications by the MAIS Group

[9] Scheduler-Independent Declassification.
Alexander Lux, Heiko Mantel and Matthias Perner. TU Darmstadt, Technical Report TUD-CS-2012-0061, 2012.
[ BibTeX entry | PDF ]

[10] Report on the RS³ 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 ]