Student projects

Runtime Policy Monitoring and Enforcement

Monitoring is a lightweight approach to formal verification. A monitor checks whether observed system behaviour is compliant with a given policy. The observations are usually provided as log files or event streams. Policies describe desired properties such as functional correctness, access control, or compliance with regulations like the GDPR.

We develop techniques and monitoring tools that are expressive and efficient. We are also interested in policy enforcement, that is, preventing policy violations instead of only detecting them. Possible topics include algorithmic improvements, verification of our tools, and practical applications of monitoring.

For further information, potential projects and whom to contact see: link.
 

Formal Verification with the Tamarin Prover

The Tamarin prover is a powerful tool for modeling and analyzing security protocols. Tamarin provides a language to model security protocols and to define the desired properties. Those properties can then be automatically or manually analyzed on the protocol model.

Thesis topics can range from using Tamarin to find attacks and proof properties of security protocols to tool development.

For further information, potential projects and whom to contact see: link.

Analyzing Website Compliance with Privacy Regulations (GDPR and ePrivacy)

European regulations such as GDPR have potential to protect users' privacy, yet we see websites' compliance lagging behind. In this project, we help legal scholars to understand this lack of compliance by automating the process of detecting privacy violations. When possible, we also enforce privacy for users.

Thesis range from extending crawling capabilities to ML classification of violations.

For further information, potential projects and whom to contact see: link.

Design, Verification, and Implementation of Cloud Database Systems

Modern web applications are typically layered on top of a high-​performance cloud database running in a partitioned, geo-​replicated environment for system scalability, data availability, and fault tolerance.

We are interested in designing provably correct and predictably high-​performance cloud database transaction systems, as well as the pass from those designs to the actual system implementations. We are also interested in verifying and optimizing existing distributed transaction systems from both qualitative and quantitative aspects.

For further information, potential projects and whom to contact see: link.

Modeling and Verification of Distributed Systems

Distributed systems, including secure networking protocols, security protocols, distributed database systems, and replication algorithms are interesting targets for formal modeling and verification. We propose to use stepwise refinement to derive distributed systems that are correct-by-construction. The modeling and proving is carried out in the Isabelle/HOL proof assistant. Here, HOL stands for higher-order logic, which can be paraphrased as “functional programming plus quantifiers”. Some thesis topics may also involve ML programming to extend Isabelle/HOL's functionality or improve its proof automation.

For further information, potential projects and whom to contact see: link.

Model-driven Security and Privacy

Security and privacy requirements are often neglected is the design phase. We aim at building software that is secure and privacy-aware by design. This requires: (1) integrating security and privacy into the software models; (2) implementing appropriate model transformations to generate policy enforcement mechanisms that prevent noncompliant system executions; and (3) assigning formal semantics to the models to facilitate precise documentation and automatic analysis of security and privacy policies. Main idea is to move security and privacy out of developers' way as much as possible by (re-)generating the corresponding code.

For further information, potential projects and whom to contact see: link.