

Completed projects
InformationFlow Security

 Research in InformationFlow 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 socalled 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 programminglanguage based methods for information flow analysis.
Formal Testing Techniques

 Today, essentially two software verification techniques are used: formal software verification and software testing. Whereas formal verification is rarely used in "largescale'' software developments, testing is widely used, but often in an adhoc 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, specificationbased testing techniques with respect to securitycritical computer systems, for example firewalls or accesscontrol mechanisms of webservices.
 Specificationbased 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 specificationbased firewall testing methodology. The phrase "specificationbased" 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.
Modelling and Verification in HOLZ

 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 ISOstandardized 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 HOLZ 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 componentbased, objectoriented 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 preconditions, postconditions and invariants to classdiagrams. In this project we are developing (on top of Isabelle/HOL) the interactive theorem prover environment HOLOCL that supports formal reasoning over UML/OCL specifications.
AutomataTheoretic Verification Methods

 AutoBaSys (funded by the SNF): The last 25 years have witnessed the successful development and deployment of methods for the computersupported verification of finitestate and infinitestate systems. Automata theory has emerged as a powerful tool to design and implement such methods. The objective of AutoBaSys is to develop automatabased methods that advance the stateoftheart in the automatic verification of finitestate and infinitestate systems.
The automatatheoretic approach to finitestate model checking utilizes automata as a means to describe system properties and system behaviors, i.e., sets of traces. Analogously, in the verification of infinitestate systems, automata can be used to represent sets of reachable system states. In particular, automata can be used to represent and compute with firstorder definable sets in the linear arithmetic over the reals, which in turn can represent the sets of reachable states of infinitestate systems.
In AutoBaSys, we analyze such automatabased 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
Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne
graphische Elemente dargestellt. Die Funktionalität der
Website ist aber trotzdem gewährleistet. Wenn Sie diese
Website regelmässig benutzen, empfehlen wir Ihnen, auf
Ihrem Computer einen aktuellen Browser zu installieren. Weitere
Informationen finden Sie auf
folgender
Seite.
Important Note:
The content in this site is accessible to any browser or
Internet device, however, some graphics will display correctly
only in the newer versions of Netscape. To get the most out of
our site we suggest you upgrade to a newer browser.
More
information