Student projects

On this page, you'll find a list of all the Semester-/Diplom(Master)arbeit projects we have open at the moment. This is what we've got. What about you? Got an idea for a cool project? Excellent! We're always open to ideas from motivated students, so why not email one of the contact people listed below?

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

We propose two master-thesis projects for finite-state model checking. In particular, the translation from the IEEE standardized specification language PSL to automata should be implemented.

1. Symbolic Implementation of PastPSL
2. PastPSL for the SPIN Model Checker

If you are interested in automatic verification, temporal logics, and automata theory then do not hesitate to contact us.

Contact: Felix Klaedtke

Projects in the context of Model Driven Security (MDS) are available on the MDS homepage

Contact: Lukas Brügger

We have several available Semester and Master Projects in the area of security protocol analysis.

Using recently developed techniques that involve fine-grained adversary models, we aim to investigate existing security protocols from a new angle. The available projects include topics such as attack finding, tool development, and formal modeling.

• Example project: Parallel Compromise Analysis of the Clark-Jacob protocols.
  In this project, the student will use the BRUTUS cluster at ETH to perform a large-scale compromise analysis of a set of protocols. This will provide new insights into the security of the protocols and may reveal new attacks.
  For more details read the project description.

More information can be found here.

Contact: Cas Cremers

Refinement can be used to develop security protocols that are correct by construction. Such developments starts with the abstract specification of the protocol's essential security properties, pass through abstract versions of the protocol without communication channels or using abstract channels with security properties, and end with a full-fledged protocol communicating over insecure channels resisting attacks of an active intruder. Different kinds of student projects are possible in this context: development of (families of) protocols using Isabelle/HOL or Rodin/Event-B with or without extensions of the underlying theories.

Contact: Christoph Sprenger

Isabelle is a generic theorem proving environment of the LCF prover family; as such, it can be used formalizing mathematical proofs as well as an implementation basis for programs performing symbolic computations. Isabelle/HOL is the instance of Isabelle with Church's Higher-order Logic; it provides typed set-theory, data types, recursive higher-order functions and can thus be viewed as a "functional programming language with quantifiers". Isabelle/HOL is a powerful basis for analysing and proving functional properties as such, or in connection with concrete programming languages or software architectures.

Contact: Lukas Brügger

Event-B is a formal method targetting system-level modelling and reasoning. The central notion to the method is abstraction and (step-wise) refinement, where mathematical proofs are required to verify the consistency between different levels of abstraction. The final system is correct-by-construction with the Event-B approach. The Rodin Platform is an Eclipse-based IDE for Event-B including supports for mathematical proofs. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
There are several student (semester/master) projects available within the context of Event-B and the Rodin Platform, in particular in the areas of automated theorem proving and code generation. We are looking for motivated students who are interested in formal modelling and how to make it practical with tool support.

Contact: Thai Son Hoang, Matthias Schmalz, Andreas Fürst

From XML to SSL, from Java to .NET, research in our group spans all aspects of information security. Below you'll find project proposals dealing with other topics in security, ones that don't really fit in the above categories. Do you have a project idea that doesn't seem to fit anywhere? Never fear, it fits here!

• "Usage Control" in a Secure Messaging Environment (pdf)
• "Information Flow Control" in World-Wide, Multi-Party Secure Messaging Systems (pdf)

Contact: any of the InfSec group members