Below are ideas for projects in DSLAB, loosely organized by topic. All projects could be adapted to a semester project (Bachelor, Master or PhD) or a Master thesis. Don’t worry if you don’t know the names of some of the tools or languages we mention, as long as you’re willing to learn.

We enthusiastically welcome students’ own ideas; please contact George Candea if you have one.

(Last updated in April 2018)

Verified Data Structures

The Vigor project combines verified data structures with symbolic execution to formally verify network functions. We have a few verified structures, but can always use more, especially if they’re radically different, such as:

Either use VeriFast, or propose your own method.

Contact: Arseniy Zaostrovnykh

Full-Stack Verification of Network Functions

The Vigor project currently provides verified network functions including verification of the framework used by the network function (DPDK) and its driver for a network card. Future directions to expand this include:

  • Port DPDK to a verified OS, such as SeL4, and prove the result;
  • Include the C library in the verified code, or even parts of the Linux kernel;
  • Improve the toolchain to reduce the trusted base, such as by using a certified compiler;
  • Integrate with work on other parts of the stack, such as Vale, HACL*, …

Contact: Solal Pirelli

Extending Vigor

The Vigor project introduced a new approach to proving the correctness of network functions. Extend the toolchain to prove other properties, different kinds of software, other programming languages…

Contact: Arseniy Zaostrovnykh

Formalization of RFCs

RFCs are specifications for protocols such as HTTP (web), SMTP (mail), NAT (network address translation), etc. They are written primarily for humans, and cannot be consumed as-is by a tool. This project would entail formalizing RFCs so that they can be consumed by program verifiers in order to prove the correctness of an implementation.

Another approach would be to go bottom-up and express existing RFCs using existing primitives in some domains, such as expressing network-related RFCs in terms of NetBricks primitives.

Contact: Rishabh Iyer

Performance verification of NetBricks primitives

NetBricks introduces primitives that they claim can represent any network function. To bound the worst-case packet-processing time of a network function, one could model those primitives in terms of performance contracts and prove that they meet their goals.

Contact: Rishabh Iyer

Performance verifier

Develop an automated tool, similar to VeriFast for correctness, that will automatically prove that a piece of code meets specific performance requirements. This may include modelling specific hardware details, such as the CPU caches.

Contact: Rishabh Iyer