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?

Fuzz-testing Security Protocols

Fuzz-testing addresses the problem of checking how a system handles unexpected inputs: the system is executed using the inputs that are not anticipated by the specification, and then the system's behavior is checked for failures. We have developed a prototype tool for fuzz testing security protocols, dubbed SecFuzz. SecFuzz uses a concrete implementation of the protocol as a black-box for generating valid inputs, which are then mutated using a set of fuzz operators. In a preliminary experiment, the tool revealed 3 previously unknown vulnerabilities (e.g. CVE-2011-4073) in two implementations of the Internet Key Exchange protocol. We are looking for a motivated master student to extend SecFuzz for testing popular protocols such as OAuth.

Contact: Petar Tsankov, Mohammad Torabi Dashti

Automatic verification techniques

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

Protocol analysis

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.

More information can be found here.

Contact: Cas Cremers

Development of security protocols by refinement

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

Modeling and verification in Isabelle/HOL

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: Christoph Sprenger

System development with Event-B and the Rodin platform

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, Andreas Fürst

Miscellaneous offerings

From XML to SSL, from Java to .NET, research in our group spans all aspects of information security. Do you have a project idea that doesn't seem to fit anywhere? Never fear, it fits here!

Contact: any of the InfSec group members