TUM Logo

SoK: Developing Formally Verified Device Drivers

SoK: Developing Formally Verified Device Drivers

Supervisor(s): Johannes Wiesboeck, Patrick Herter
Status: open
Topic: Others
Type of Thesis: Bachelorthesis
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching

Description

Bachelor’s thesis in cooperation with Fraunhofer AISEC

SoK: Developing Formally Verified Device Drivers

Formal software verification is an extensively researched approach used to ensure the correctness and reliability of software. The seL4 microkernel was one of the first larger projects that demonstrated that verification can establish strong security guarantees.Yet, due to the high effort required for writing formally verified software, adoption is still limited to a small, selected set of projects (e.g. seL4) and special industries (e.g. aerospace).

We seek to enable efficient formal verification of device drivers, the next important set of system components after the kernel. While the security impact of malfunctioning device drivers can be limited by using a microkernel design, one major security goal is left untouched by this design choice: availability. Furthermore, embedded systems lacking support for virtual memory may not be capable of running a microkernel-based operating system. Device drivers also play a (security-)critical role in virtualized environments where virtual device drivers are part of the interface between virtual machine and hypervisor.

Task Description

The goal of this thesis is to research state-of-the-art approaches for developing formally verified device drivers. These approaches can range from manual verification using proof assistants to model checking and automatic synthesis of verified code. One promising approach shall be selected and a proof-of-concept driver shall be implemented for a device and operating system of choice (e.g. Linux userspace, Linux kernel, seL4, VirtIO).

Requirements

  • Interest in writing high-assurance, formally verified systems software
  • Fundamentals of Linux and low-level systems programming (from IN0009)
  • Fundamentals of functional verification (from IN0003)
  • Proficiency with a proof assistant such as Isabelle/HOL or Coq may be beneficial but is not mandatory

Contact

Please send your application with current CV and transcript of records to:

Johannes Wiesböck
Secure Operating Systems
Mail: johannes.wiesboeck@aisec.fraunhofer.de
Phone: +49 89 322 9986-1046

Patrick Herter
Secure Operating Systems
Mail: patrick.herter@aisec.fraunhofer.de
Phone: +49 89 322 9986-1058

Fraunhofer Institute for Applied and Integrated Security (AISEC)
Lichtenbergstr. 11, 85748 Garching near Munich

Publication Date: 04.04.2024