SPP 1496: Reliably Secure Software Systems

Basic data for this project

Description

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.