Mario Frank successfully defended his dissertation on May 31 on the topic "On Synthesising Linux Kernel Module Components from Coq Formalisations".
The topic was at the intersection of Theoretical Computer Science, Software Engineering and Operating Systems. The thesis supervisors were Prof. Dr. Christoph Kreitz and Prof. Dr. Anna-Lena Lamprecht. The group of reviewers, which included the supervisors, was completed by Prof. Andrew Appel, PhD from the Princeton University.
In his dissertation, he evaluated the possibility of generating working, i.e. compilable, Linux device drivers from a functional model in the Proof Assistant Coq. He found that such a functional model can be used by the verified CertiCoq Plugin to generate C (Clight) code, but that the code is not usable as a part of a kernel module since CertiCoq's runtime, which is needed for compilation, is not compatible with kernel space. However, he was able to demonstrate that the runtime of CertiCoq can be adapted in a schematic way to make it compatible. With these modifications, he was able to demonstrate that the C code generated from a functional model of the Linux PC Speaker driver can be compiled as part of a Linux kernel module. Furthermore, he was able to demonstrate that the compilation toolchain for the kernel module can be adapted to use the verified C compiler CompCert for the generated code and the GCC for the rest. Consequently, he was able to demonstrate that if the functional model is correct, a Linux device driver can be built whose generated parts are correct by construction up to the assembly layer. However, he also found that there is still room for improvement in terms of the generated code's performance, which could be enhanced by optimising the functional model and the code generation.