Looking for Bachelor or Master projects, or a Master thesis? Below are some project ideas.
Looking for a Ph.D. semester project? Email George.

Our projects are about investigating new ways to build systems and analyze them.
Don’t worry if you don’t know some of the concepts we mention, as long as you’re willing to learn.

The following list is for Fall 2020.
If you’re interested, or if you have any questions, e-mail us at projects@dslab.org.

Formally verify a bootloader

DSLAB has developed a minimal OS for network programs such as routers or network address translators. This OS has been formally verified to be correct … except for the bootloader. Can the bootloader also be verified?

In this project, you will:

  • Investigate how to verify a bootloader written in assembly mixed with C
  • Either verify the existing bootloader, possibly modifying it, or integrate with an existing verified bootloader

You will learn:

  • Formal verification techniques
  • Low-level hardware initialization details

Formally verify network functions

Network functions are programs that deal with network packets to implement some network functionality, such as routing, filtering or caching. DSLAB has developed the Vigor technique to verify network functions, and has verified a few implementations already, but there are many more that could be verified by extending Vigor. For instance, one could verify a VPN, a DNS server, or an intrusion detection system.

In this project, you will:

  • Pick a network function to verify
  • Write a specification for it, based on existing work
  • Write an implementation of the network function
  • Formally verify it with the Vigor technique, extending Vigor if needed

You will learn:

  • Formal verification techniques
  • Networking details

Implement a fast driver for a 100 Gb/s network card

DSLAB has designed a new network card driver model, which is faster than existing drivers because it is less flexible. We have an implementation for a 10 Gb/s server network card, the Intel 82599. How fast could a driver in this model be using a 100 Gb/s card, such as the Mellanox ConnectX-5?

In this project, you will:

  • Implement a driver for a Mellanox ConnectX-5 card
  • Evaluate its performance compared to Mellanox’s own driver

You will learn:

  • Low-level network card driver details
  • Explore new ideas in driver architecture

Investigate the performance of modern OS networking APIs

Traditional network APIs in operating systems, such as “sockets”, were invented where the network was slow. Modern networking is much faster: modern Ethernet links can reach 100 Gb/s! To handle this speed, modern networking frameworks bypass the operating system, which is fast but loses all isolation. However, modern operating systems have added faster APIs, such as Windows’s “RIO” and Linux’s “io_uring”, which are designed to increase performance by avoiding most of the current overheads at the cost of a more complex API; are they fast enough?

In this project, you will:

  • Write a program that forwards packets using Linux’s io_uring API
  • Benchmark and optimize its throughput and latency
  • Do the same with a port of a more realistic program, such as DSLAB’s formally verified NAT

You will learn:

  • Advanced Linux networking
  • Profiling and benchmarking techniques

Improve the performance of symbolic execution

Symbolic execution is a program analysis technique in which a tool automatically unfurls a program into its different possible execution paths, to either find a path that contains a bug or to prove that none of the paths have bugs. A standard piece of modern symbolic execution is “symbolic models” of the environment in which the analyzed program runs (e.g., models of the C standard library). These models are abstractions of the modeled code that are simpler than that code but still good enough for symbolic execution. This project is about automatically generating efficient symbolic models based on several research insights we gained over years of using symbolic execution.

In this project, you will:

  • Pick several programs that currently take too long to symbolically execute with standard models
  • Isolate the environment interactions that cause this
  • Implement several ideas for how to simplify the environment models and how to automate this simplification

You will learn:

  • Symbolic execution

Your own idea

Do you have a project idea related to DSLAB’s interests, such as dependability or practical formal verification?
Feel free to contact us!

In this project, you will:

  • Work on your own idea with our guidance
  • Discover something new, small or large

You will learn:

  • Something you don’t know already