Completed projects

• Research in Information-Flow Security is concerned with investigating secrecy and integrity properties. It goes beyond studying access control in that it is concerned with the propagation of information in a system, and not only with its release. Information may propogate in unintended ways due to hidden channels where observers may gain information by examining different aspects of system behavior. One example of this is a so-called timing leak, through which a system reveals a secret by showing characteristic timing behavior. For example, a careless implementation of a cryptographic algorithm may reveal a user's secret key to a malicious party, even if that party can only observe the algorithm's running time. We are developing methods for detecting, quantifying, and eliminating information leaks, with a particular focus on timing leaks. Active avenues of research include the analysis of synchronous hardware and programming-language based methods for information flow analysis.

• Today, essentially two software verification techniques are used: formal software verification and software testing. Whereas formal verification is rarely used in "large-scale'' software developments, testing is widely used, but often in an ad-hoc manner. Recent research aims to systematize the foundations of testing and combine it with formal verification techniques such as theorem proving or model checking. Of particular interest are formal, specification-based testing techniques with respect to security-critical computer systems, for example firewalls or access-control mechanisms of web-services.
• Specification-based Firewall Testing (project funded by armasuisse):
  Firewalls are a central component in network security. Nowadays everybody is using firewalls, unfortunately without having good means for determining if they are accomplishing their job correctly. The aim of this project is to develop a specification-based firewall testing methodology. The phrase "specification-based" is important here: firewalls in a bank have to accomplish a different goal than those in a university, thus we cannot use the same tests. Or said otherwise, for every environment we have to generate tests separately, based on the security policy of the respective environment.

• The increasing complexity of today's software systems makes modeling an important phase during the software development process, both, on the level of requirement analysis and the system design. The ISO-standardized specification language Z can be used for a formal underpinning of these activities. In particular, the Z Method allows for relating Requirements and System Designs via formal refinement notions. In this project we are developing (on top of Isabelle/HOL) the interactive theorem prover environment HOL-Z that supports formal reasoning over Z specifications and formal proof on refinements. The system achieved meanwhile a reasonable degree of automation such that several substantial case studies (CVS Server, DARMA funded by Hitachi) had been realized, involving both refinement as well as temporal reasoning.
• The increasing complexity of toda'ys software systems makes modeling an important phase during the software development process, both, on the level of requirement analysis and the system design. The Unified Modeling Language (UML) has meanwhile achieved a remarkable acceptance in industrial projects of component-based, object-oriented systems. Further, the Object Constraint Language (OCL) has been proposed as a formal extension. OCL allows one to constrain UML models, e.g. by adding pre-conditions, post-conditions and invariants to class-diagrams. In this project we are developing (on top of Isabelle/HOL) the interactive theorem prover environment HOL-OCL that supports formal reasoning over UML/OCL specifications.

• AutoBaSys (funded by the SNF): The last 25 years have witnessed the successful development and deployment of methods for the computer-supported verification of finite-state and infinite-state systems. Automata theory has emerged as a powerful tool to design and implement such methods. The objective of AutoBaSys is to develop automata-based methods that advance the state-of-the-art in the automatic verification of finite-state and infinite-state systems.
  The automata-theoretic approach to finite-state model checking utilizes automata as a means to describe system properties and system behaviors, i.e., sets of traces. Analogously, in the verification of infinite-state systems, automata can be used to represent sets of reachable system states. In particular, automata can be used to represent and compute with first-order definable sets in the linear arithmetic over the reals, which in turn can represent the sets of reachable states of infinite-state systems.
  In AutoBaSys, we analyze such automata-based representations of sets and the automata constructions for manipulating them, and we aim at optimizing them in order to accelerate automatic verification.
• Contact: Felix Klaedtke and Christian Dax