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

Research in RS3

The priority programme RS3 builds on the state of the art in three different research disciplines:

  • Information security
  • Programming languages
  • Formal methods

The programme aims at bringing together researchers from all three areas in order to work together towards supporting the reliable certification of useful, system-wide security guarantees based on a well-founded understanding of programs and of security aspects.

RS3 Guiding Themes and Phases

To achieve this research goal, the priority programme has three main guiding themes which build on top of each other:

  1. Property-centric view of security
  2. Semantically-justified certification of security
  3. Security in the large

RS3 is divided into three phases, each of which is too years long. The three guiding themes are in line with these three phases: The first phase focuses on the first guiding theme, and then each subsequent phase adds the next guiding theme to the research focus building on the achievements of the previous phase:

Phases of the priority programme

 Property-centric view of security

The first guiding theme is the development of precisely defined (and, thus, verifiable) security properties. This shall enable 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.

 Semantically-justified certification of security

The second guiding theme is the development of program analysis methods and tools that target the verification of security properties in a sound, precise, scalable, and usable way. This will create the basis for a semantically substantiated (and, thus, reliable) certification of security guarantees for software systems. Verification tools will be employed to establish security properties of programs as well as to ensure the soundness of security analysis tools.

 Security in the large

The third guiding theme is the development of concepts for understanding and certifying security aspects even in complex software systems (hence, for security in-the-large). This requires the adaptation of established techniques for abstraction, decomposition and step-wise refinement to the field of security. In particular, it shall 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.

RS3 research structures

Within RS3, there are two different ways of structuring the individual research projects. These structures are designed to foster collaborations and to advance research within RS3 towards specific common research goals. The first structure groups the projects into Project Clusters. A project cluster constitutes a discussion platform for projects who work within the same specific research area. The second structure groups projects into Reference Scenarios. The reference scenarios shall demonstrate the applicability of various research results achieved within different research areas within a concrete practical scenario. Both of these structures serve as guidelines and also as a means to structure common working sessions during RS3 meetings.