Role Mining

This project addresses an important practical problem in Information Security: developing and rationalizing access control infrastructures based on Role-Based Access Control (RBAC). RBAC is an approach for specifying user privileges for carrying out operations on system objects: Roles group together system privileges and users are assigned to roles, thereby granting them the associated privileges.
Although RBAC is conceptually simple, it is very difficult to configure RBAC systems in practice within large enterprises, i.e., to determine the appropriate roles and assign users to roles. This complexity leads to both high security administration costs and security weaknesses due to improperly implemented and administered security policies.

To tackle these problems, data mining techniques will be developed for both configuring RBAC systems and for assessing configurations. Data sets such as existing user privileges or job functions will be used for this analysis. The resulting configurations should satisfy various criteria such as minimizing the number of roles or minimizing the changes required when users are added to or removed from the system.

Read more on the project web page.

Usage Control in Ubiquitous Communication

The project started in 2009 and ended in 2011. It was carried out in collaboration with Nokia Research Center, Lausanne. Our objective in this project was to advance the state of the art in observing and controlling the usage of sensitive data in IT systems. We developed methods that monitor the use of data and ensure that usage is conform to the intended purposes for which the data was collected. Furthermore, based on these monitors, we designed and prototypically implemented architectures for pervasive computing applications that report on the misuse of sensitive data.

Read more on the project web page.

Authentication over Insecure Wireless Channels

This project deals with message authentication and integrity protection in wireless networks. The main focus of this project is authentication without pre-shared keys and/or credentials. Three proposals have so far emerged in this context: INTEGRITY-CODING, INTEGRITY-REGIONS and reliance on SHORT STRING COMPARISON. Particulary attention in this project was devoted to authentication through presence awarness (i-codes and i-regions).

Read more on the project web page.

Information-Flow Security

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.

Formal Testing Techniques

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.

Modelling and Verification in HOL-Z

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

Automata-Theoretic Verification Methods

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