DFG project "Formal Methods for Security Engineering"


Project Description Research List of Publications



Project Description

Project Lead: Prof. Dr. Heiko Mantel

In addition to functional requirements, one needs to consider aspects like confidentiality, integrity, and availability during the development of security-critical systems. Such security aspects are not properly addressed during system development so far. This is one of the main reasons why we are facing so many security problems in current IT systems.

Our aim in the project FM-SecEng (funded by the German Research Foundation - DFG) is to develop a formally justified basis for respecting security aspects throughout the software development process and for a global, i.e. system-wide, consideration of security requirements. We develop methods, techniques, and tools that can be applied in a security engineering process in order to improve the security of the resulting IT systems.

A software engineer faces several problems when applying a security engineering process. For instance, the following questions arise when security requirements are considered throughout the development process:

  • Which security requirements are critical for the system under development and how can these requirements be formally specified in an adequate way?
  • Which architecture should be chosen and which security mechanisms should be employed in order to simplify the treatment of security during further system development or for simplifying a formal verification of the system?
  • Which is the most efficient way of verifying a given system against its requirements?

For instance, the following questions arise in a system-wide consideration of security requirements:

  • How does a given system component or a given security mechanism contribute to the security (or insecurity) of the overall system?
  • What is the significance of the results from the analysis of an abstract system model for the actual system?



Research

Security Properties Security Engineering Security Analysis



Security Properties

During early phases of the software engineering process software engineers are confronted with the problem of security requirement specification. Information-flow properties can be used to specify confidentiality and integrity requirements. Such properties pose particular problems as they cannot be expressed as a property of single system runs, but only as properties of the set of all possible system runs. We want to develop methods to integrate the specification of information-flow properties into the software development process, and to support software engineers by providing support for the choice of adequate characterisations of information-flow security.

Publications:

  • Dieter Hutter, Heiko Mantel, Ina Schaefer and Axel Schairer. Security of Multiagent Systems: A Case Study on Comparison Shopping. In Journal of Applied Logic, 2007.
    [ BibTeX entry ]

Based on:


Stepwise Development of Secure Systems

When designing secure systems, one needs to know to which extent the use of concrete security mechanisms contributes to the overall system security. Consider, e.g., the problem of covert channels. Covert channels allow the transmission of information, although they are not intended for this purpose. Covert channels arise when resources are shared between entities, like, e.g., physical memory or the CPU shared by processes. While many covert channels can, in principle, be eliminated by assigning fixed quotas of resource usage to entities (a method named 'quotation'), interrupt-related covert channels cannot be eliminated by this method.
We formally modeled and analyzed interrupt-related covert channels in an information-theoretic framework. The framework allows to compare different mechanisms that can be applied to mitigate such covert channels. There are, e.g., mechanisms, whose original purpose is not the elimination of covert channels, but which mitigate such channels nevertheless. We employed our model to assess how effective such mechanisms mitigate interrupt-related covert channels.

Publications:

  • Sylvia Grüner. Formale Spezifikation von Sicherheitsanforderungen mit MAKS in Isabelle/HOL (Bachelor Thesis). TU Darmstadt, 2010.
    [ BibTeX entry ]
  • Serge Autexier and Heiko Mantel. Verify'06: Verification Workshop. In FLoC, 2006.
    workshop in connection with Federated Logic Conference, FLoC'06
    [ BibTeX entry | URL ]


Security Analysis

If one entrusts a program with confidential information, one needs to ensure that the program is trustworthy in the sense that it does not leak the confidential information. We develop sound static analysis techniques for information-flow security, where the focus is on the declassification of confidential information, the automatic correction of insecure programs, the sound combination of different analysis techniques, and the analysis of multi-threaded programs.

Publications:

  • Heiko Mantel and Henning Sudbrock. Types vs. PDGs in Information Flow Analysis. In Pre-Proceedings of the 22nd International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2012, 2012.
    [ BibTeX entry ]

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang