Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496

The Priority Programme at a Glance

Motivation

This Priority Programme assumed that a paradigm shift in IT-security is necessary in order to reliably guarantee the security of complex software systems. The current trust-based and mechanism-centric approaches to IT-security were to be complemented by property-oriented solutions. This paradigm shift was to enable a trustworthy certification of system-wide, technical security guarantees that adequately respects the semantics of programs and of security requirements. Bridging the gap from security in-the-small to security in-the-large involved the improvement of conceptual foundations, the development of analysis and engineering tools, and their migration into practice. Collaborations between multiple sub-disciplines of Computer Science, primarily formal methods, IT-security, and programming languages, were necessary to achieve the objectives of the programme.

The three RS3 Guiding Themes

  1. The first guiding theme was the development of precisely defined (and, thus, verifiable) security properties. This enabled a property-oriented perspective on security that, on the one hand side, abstracts from technical details of implementations and, on the other hand side, permits one to model the manifold security requirements and guarantees in an adequate and precise way.
  2. The second guiding theme was the development of program analysis methods and tools that target the verification of security properties in a sound, precise, scalable, and usable way. This created the basis for a semantically substantiated (and, thus, reliable) certification of security guarantees for software systems. Verification tools were employed to establish security properties of programs as well as to ensure the soundness of security analysis tools.
  3. The third guiding theme was the development of concepts for understanding and certifying security aspects even in complex software systems (hence, for security in-the-large). This required the adaptation of established techniques for abstraction, decomposition and step-wise refinement to the field of security. In particular, it was to become possible to derive abstract security guarantees (e.g., need-to-know or separation-of-duty) from the low-level properties that are typically guaranteed by security mechanisms.

The overall goal of the programme was to support the reliable certification of useful, system-wide security guarantees based on a well-founded understanding of programs and of security aspects. It ran from 2010 to 2017.