The overall research objective of MAIS is to increase the trustworthiness and reliability of software- based systems. The spectrum of research questions ranges from theoretical foundations over methods and tools to applications in the real world. The current research topics are grouped under the following four research areas:
When running a program that requires access to confidential data, one wants to be sure that no information about the confidential data is leaked to untrusted third parties. For instance, a banking application requires access to a user's login credentials, but no information about the login credentials must be leaked to the developers of the app even if they legitimately receive other information, e.g. usage statistics.
Such security requirements can be formally expressed with information-flow properties. Program analysis techniques, such as security type systems, can check automatically whether a program satisfies a given information-flow security property. In the scenario of the banking application, a positive result of the analysis combined with a so-called soundness result for the analysis technique guarantees that no information about the user's login credentials is leaked to the developers.
At MAIS, we develop and improve information-flow security properties, and sound analysis techniques for these properties on different platforms and layers. Furthermore, we develop methods and tools for the automatic verification of programs based on these analysis techniques and for designing secure systems. In this area, the topics we currently focus on include the following:
Contact People:
Dr.-Ing. Alexandra Weber
Prof. Dr.-Ing. Heiko Mantel
The security concerns that might arise when a program is used are not always completely understood and addressed during the development of the program. Even if security aspects have been addressed during program development, a user of the program might not be convinced that this has been done with sufficient rigor. Moreover, security requirements might arise from a particular use of a program, while being irrelevant for other uses.
In order to observe whether a program complies with a given security requirement, monitoring mechanisms can be applied. Examples of such requirements include, for instance, confidentiality, integrity and separation of duty. Monitoring mechanisms can be classified either as online mechanisms that are able to observe security violations at runtime, or as offline mechanisms that can identify security violations even after the program is terminated, e.g., inspecting log files. In order to not only observe security violations, but rather ensure that security requirements are satisfied, dynamic enforcement mechanisms can be applied.
At MAIS, we see dynamic enforcement as an encapsulation that protects a program from a malicious environment or, vice versa, the environment from a malicious program. In this area, our research addresses both theoretical aspects (e.g., which security properties are enforceable) and practical aspects (e.g., how to implement dynamic enforcement mechanisms effectively and efficiently). The topics we currently focus on include the following:
Contact People:
Dr.-Ing. Alexandra Weber
Prof. Dr.-Ing. Heiko Mantel
Side channels are unintended indirect flows of information revealed by execution characteristics of a computer program. Examples of side channels include program's running time, cache behavior, power consumption, electromagnetic radiation, etc. Such unintended flows of information may be correlated to secrets e.g., private cryptographic keys, and this makes side channels a severe security vulnerability. By exploiting such correlation, a hacker can recover the secrets, and this is known as a side-channel attack.
Side-channel vulnerabilities can be detected systematically with program analysis techniques. An example for program analysis techniques is type-based analysis. Such an analysis is based on a security type system, which specifies how information may be propagated through a program. Abstract interpretation is another analysis technique that, together with information theory, can be used to compute upper bounds on the information leakage. As a complement to analytical techniques, experimental techniques are used to collect possible attacker observations and determine how much information can be leaked via side channels.
By using above mentioned techniques, at MAIS, we develop methods and tools for sound detection of side channels, assessment of their seriousness, construction of attacks and design of proper countermeasures, mitigation and avoidance of side channels. In this area, the topics we currently focus on include:
Contact Persons:
Dr.-Ing. Alexandra Weber
Prof. Dr.-Ing. Heiko Mantel
Software-based systems already play a key role in industrial production, reliability of critical infrastructures and in the use of information and services. The functionality, efficiency and security of software are critical factors, each of which can make the difference between financial gain and loss, often even between life and death. The current paradigm shift in industrial production and in the processing of information together with rapid technological progress in hardware and middle-ware require the development of suitable software systems.
At MAIS, we focus on sound re-engineering and parallelization of software systems. We aim to make the verification of re-engineered programs scale. We work on reducing conceptual complexity by compositional reasoning. More specifically, we exploit design patterns introduced during the re-engineering process. We aim to develop a portfolio of compositionality results that allow one to deduce guarantees for a complex program from properties of its components. The topics we currently focus on in this area include:
Contact People:
Dr.-Ing. Alexandra Weber
Prof. Dr.-Ing. Heiko Mantel
Further information can be found in the Projects sections. You can access and read our publications here.