Reliable Security for Concurrent Programs (RSCP)

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

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.

Results/Some Highlights

Noninterference under Weak Memory Models

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.

Based on these results published in [MPS14], we are currently extending the results to an ARM-inspired memory model.

Rely and Guarantee

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

Building on this framework, we have developed a purely static as well as a hybrid analysis to verify whether a concurrent program has secure information flow.

The static analysis published in [MMPW15] combines a security type system with a reachability analysis based on dynamic pushdown automata for analyzing programs with lock-based synchronization. The security type system analyzes a thread for secure information flow under assumptions about the environment. The DPN-based analysis verifies that the assumptions about the environment of each thread are satisfied in a given multi-threaded program.

The hybrid analysis published in [ACM15] combines static analysis with monitoring on two levels to analyze systems with barrier-based synchronization. The monitoring is split into a thread-local and a global monitoring to avoid unnecessary synchronization between concurrent threads.

Scheduler-Independent Declassification

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

Cassandra

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 [LMS+14] 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 [LMSW14]. 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. More information on Cassandra, including a downloadable version of the app and the source code, can be obtained on the page about Cassandra.

 

Collaborations of the MAIS Group during RS3

Conference Publications with Results from RSCP

Master and Bachelor Theses on RSCP topics

  • Maximilian Scheid. Effects of Processor Optimizations in a Raspberry Pi on Possible Results of Multi-threaded Programs. Bachelor's thesis, TU Darmstadt, 2017.
    BibTeX entry ]
  • David Schneider. An Object-Sensitive Type-Based Information-Flow Analysis for Android Applications. Master Thesis, TU Darmstadt, 2014.
    BibTeX entry ]
  • Alexandra Weber. Comparison of an Operational and an Axiomatic Model of Execution for Multi-threaded Programs. Master Thesis, TU Darmstadt, 2014.
    BibTeX entry ]
  • Pascal Wittmann. Confidentiality for Multithreaded Dalvik Programs by SIFUM Security. Bachelor Thesis, TU Darmstadt, 2013.
    BibTeX entry ]
  • Sylvia Grewe. Toward a Framework for Soundness Proofs of Type Systems in Language-based Information-flow Security. Master Thesis, TU Darmstadt, 2012.
    BibTeX entry ]
  • Steffen Lortz. Robustness of Information Flow Security Under Refinement of Synchronization Primitives. Master Thesis, TU Darmstadt, 2012.
    BibTeX entry ]
  • Jens Sauer. Informationsflusssicherheit in Systemen mit zwei Prozessoren. Master Thesis, TU Darmstadt, 2012.
    BibTeX entry | PDF ]
  • David Schneider. Instance-Specific Security Domain Assignments in Sequential Programming Languages. Bachelor Thesis, TU Darmstadt, 2012.
    BibTeX entry ]
  • Daniel Schoepe. Compositionality of Information Flow Security with Assumptions and Guarantees in Isabelle/HOL. Bachelor Thesis, TU Darmstadt, 2012.
    BibTeX entry ]
  • Alexandra Weber. A Formal Model, a Noninterference Condition, and a Sound Type System for a Certifying Application Store. Bachelor Thesis, TU Darmstadt, 2012.
    BibTeX entry ]
  • Christopher Mann. A Static Framework for Privacy Analysis of Android Applications. Bachelor Thesis, TU Darmstadt, 2011.
    BibTeX entry ]
  • Matthias Perner. Controlled Declassification under Semantics with Schedulers. Master Thesis, TU Darmstadt, 2011.
    BibTeX entry | PDF ]

Further RS3 Publications by the MAIS Group

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang