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).