Below are possible semester project topics in DSLAB. All projects can be adapted to the level of a Bachelor, Master or PhD project, 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.
In order to apply for a project or just ask any questions, please contact us at firstname.lastname@example.org. We enthusiastically welcome students’ own ideas, as long as they’re about improving the security and reliability of computer systems.
(Last updated in September 2018)
Control-flow hijack protection for Web browsers
Web browsers are typically written using memory-unsafe languages like C/C++, leaving them open to memory safety bugs that can lead to control flow hijack vulnerabilities. Use code-pointer integrity to secure real browsers like Chrome or Firefox against control-flow hijacks.
Secure home router
Identify what we need to do to verify a complete modern home router (its network functions, GUI configuration, etc.), most likely using the Vigor project as a base, and then pick one of the sub-projects for execution. Possible results from this work may include:
- An analysis of the work required for a fully verified home router
- Tooling to verify additional components of a home router beyond a NAT
- Experimental evaluation of the newly verified component(s)
Verifying NF performance contracts
Network functions are increasingly more at the heart of critical IT infrastructure, yet operators have no good way to predict the latency, jitter, and bandwidth of a network function faced with various possible scenarios. 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.
Automated incident analysis and response
When an attacker breaks into a system, they may leave clues that indicate that that system was compromised. Extend execution synthesis to work on arbitrary machine code and on the whole system, as opposed to just a single program. For example it could be possible to determine how a virtual machine was breached by simply looking at a snapshot of its state. The S2E platform could be a good starting point since it can symbolically execute an entire software stack, including the kernel and the system libraries.
S2E Python scripting API
S2E’s power is best harnessed through scripts, but the current Lua interface is very basic and only exposes a fraction of the engine’s functionality. A Python API is in the works but it currently only allows to write somewhat basic plugins, and interacting with existing C++ plugins is hard. Refine the Python API and bring it to feature parity with the existing C++ API.
Spectre-class side channel defense for CPUs
Identify what it would take to secure an open processor design (such as the RISC-V BOOM) by removing any possibility of Spectre-class side channel attacks. Determine the changes needed to allow speculation for performance while avoiding the microarchitectural state changes that leads to side channels. Explore ways to verify that they are gone.
Rusty Vigor: Verifiable NFs that are easy to write
When writing network functions in C/C++ meant to be verified by Vigor, the developer must think quite hard about how to separate state from stateless code. Writing network functions in Rust makes it more natural and obvious to achieve this separation, and makes verification easier and more efficient. Extend or modify the Vigor toolchain to verify network functions written in Rust: the new toolchain should take advantage of Rust’s language features (e.g., pointer ownership, borrow checker) to statically ensure as much of the Vigor discipline as possible.
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:
- a Longest Prefix Match table;
- a circular buffer;
- other standard structures we have not yet implemented, such as stacks, queues, lists, heaps, …
Either use VeriFast, or propose your own method.
Full-Stack verification of NFs
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*, …
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…
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.
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.