Provable Security for Complex IT Systems

Model-based Plausibility Check

The classical error- and attack-detection in energy networks analyzes the information technology system for untrustworthy communication flows. In doing so, only local manipulations of the energy network are detected. This leads to an increase in the risk of inter-island attacks and inter-island dependency in decentralised energy networks.

The modelling of the island networks contains not only the information technology system, but also the energy, material and heat flows (complete network). The plausibility check based on the models can now reveal discrepancies between the exchanged data and the resulting changes in the behaviour of the energy network and, depending on the hazard assessment, report or sound the alarm.

Provable Security for Complex IT-Systems

Absolute security can only be achieved for a system, if the domain-specific security properties are developed at a level, where it is possible to ensure, that the specified and verified security properties are compatible with each other.

The systems are not completely redeveloped, but are based on existing systems and functionalities. Therefore, the integration of different development phases poses a special challenge. It is also necessary to consider the security of a system over its entire lifecycle. This requires sound risk- and security-management based on a fundamental system theory, consisting of analyses of hazards of protected goods, adversarial models and suitable protection processes, -concepts and -mechanisms.

The research groups involved are the Institute for Theoretical Computer Science (ITI) and the Institute for Program Structures and Data Organization (IPD).

Composable Security

Absolute security is difficult to prove, since only those cases can be covered, that one can imagine. In order to make the concept of security comprehensible, security models are developed which formally describe the possibilities of an adversary. Furthermore, it defines exactly what it means to break a given procedure. A given cryptographic method is sufficiently secure for a security model if the adversary can only break it with a negligible probability.

At KASTEL, research is conducted into the aspects of composable security. This involves examining the extent to which the assembly of individual, proven components leads to a safe overall system. Furthermore, we are working on aggregate signature procedures. These are procedures to convert the signatures and several messages into a single signature, thus saving bandwidth during transport.

The research group involved is the Institute for Theoretical Computer Science (ITI).

System Theory

At KASTEL, a fundamental system theory is being researched, which enables a comprehensive and integrated security assessment from hazard analysis to the creation of requirements and verification of the integrated mechanisms at implementation level. A special focus of the legal perspective is on the integration of preliminary legal considerations in the event of value conflicts, for example with regard to the valuation of protected goods. This contributes to ensuring legal conformity in weighing processes, which was previously the sole domain of computer science. A wide variety of research disciplines work together to find interdisciplinary solutions.

The research groups involved are the Centre for Applied Law (ZAR) and the Fraunhofer IOSB.

Tool-Support for the Development Process

Within the context of KASTEL, a model-driven specification procedure for the collection and documentation of security requirements for systems is being developed.

It is investigated how these security requirements from the model level can be distributed to subsystems in a semantically correct way and thus be mapped to concrete implementations. In this way, their security can be verified directly in the implementation. Based on this, KASTEL develops tools and methods for the analysis, verification and integration of source and byte code in order to unite the strengths of different approaches as profitably as possible. Three tools are combined here: Palladio is an architectural tool that allows the creation of software with certain quality characteristics. JOANA examines Java programs for sequential and probabilistic leaks in information flows. Using key, it is possible to formally verify that a Java program fulfils certain properties.

The research groups involved are the Chair of Programming Paradigms (IPD) and the Institute for Theoretical Computer Science (ITI).