SPP 1496:  Reliably Secure Software Systems

• Subject Area: Computer Science, Systems and Electrical Engineering
• Term: from 2010 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 130928089

The view of IT security has traditionally been dominated by the border between a supposedly trustworthy inner world and a potentially hostile outer world. Consequently, many classical security mechanisms, e.g. firewalls, access controls and cryptography, focus on securing these borders, and trust in artefacts is established mainly based on their identity and origin. However, the border between the “inner” and the “outer” world is blurred by aspects like networking, mobility and dynamic extensibility. Hence, a more sophisticated view of security is needed. The Priority Programme, thus, aims at a new conceptual and technical framework for IT security.
The goal is to support the certification of security guarantees based on well-founded semantics of programmes and of security aspects. The first guiding theme of the Priority Programme is the development of precisely defined (and, thus, verifiable) security properties. This shall enable a perspective on security that, on the one hand, abstracts from technical details of implementations and, on the other hand, permits one to model the manifold security requirements and guarantees in an adequate and precise way. The second guiding theme is the development of analysis methods and tools that target the reliable verification of security properties of systems. This will create the basis for a semantically substantiated (and, thus, reliable) certification of security guarantees for computer programmes. 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.
The research programme requires the combination of ideas and technologies from different areas of computer science. It shall facilitate interdisciplinary cooperation between scientists working in the areas of IT security, programme analysis and formal verification, and shall provide an environment that enables a paradigm shift in IT security. The ultimate goal is a fundamental improvement of how security is addressed in software systems, including both, a more adequate assurance of security requirements and a better automation of security-relevant decisions.

• DFG Programme: Priority Programmes

Projects

• Coordination Funds (Applicant Mantel, Heiko )
• Developing Systems with Secure Information Flow (Applicant Reif, Wolfgang )
• Fully Automatic Logic-Based Information Flow Analysis (Applicant Bubel, Richard )
• Hybrid static/dynamic inter-application data-flow analysis (Applicant Hähnle, Reiner )
• Implementation-Level Analysis of E-Voting Systems (Applicant Küsters, Ralf )
• Information Flow Control for Browser Clients (Applicants Garg, Ph.D., Deepak ;  Hammer, Christian )
• Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs (Applicants Müller-Olm, Markus ;  Snelting, Gregor )
• Modular Modeling of Delegation Security in Software Development (MoDelSec) (Applicant Jürjens, Jan )
• Modular verification of security properties in actor implementations (Applicant Poetzsch-Heffter, Arnd )
• Program-level Specification and Deductive Verification of Security Properties (Applicant Beckert, Bernhard )
• Reliable Security for Concurrent Programs (Applicant Mantel, Heiko )
• Scalable Large-Scale Precise System-Wide Data-Driven Usage Control Across Layers of Abstraction and Across Machines (Applicant Pretschner, Alexander )
• Secrecy and Information Flow in Shared Document Bases (Applicants Finkbeiner, Bernd ;  Seidl, Helmut )
• Security Type Systems and Deduction (Applicant Nipkow, Ph.D., Tobias )
• Transfer and enhancement of information-flow control techniques to develop secure systems using the example of workflow systems (MORES2) (Applicant Hutter, Dieter )
• Type-based gradual enforcement of security policies for concurrent programs (Applicant Thiemann, Peter )
• User-centric, Secure Information Flow Management in Enterprise Systems (USIFES) (Applicants Atkinson, Colin ;  Freiling, Felix ;  Mädche, Alexander )
• WS4Dsec - Reliably Secure Web Services for Devices (Applicants Timmermann, Dirk ;  Wolf, Karsten )

• Spokesperson: Professor Dr.-Ing. Heiko Mantel