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 DriversFormal 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 DescriptionThe 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
ContactPlease send your application with current CV and transcript of records to: Johannes Wiesböck Patrick Herter Fraunhofer Institute for Applied and Integrated Security (AISEC) Publication Date: 04.04.2024 |