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

Research in RS3

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

  • Information security
  • Programming languages
  • Formal methods

The programme aimed 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 had three main guiding themes which built on top of each other:

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

RS3 was divided into three phases, each of which was two years long. The three guiding themes were in line with these three phases: The first phase focused on the first guiding theme, and then each subsequent phase added 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 was the development of precisely defined (and, thus, verifiable) security properties. This was to 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 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.

 Security in the large

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.

RS3 research structures

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