@phdthesis{Frank2024,
  author    = {Frank, Mario},
  title     = {On synthesising Linux kernel module components from Coq formalisations},
  doi       = {10.25932/publishup-64255},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-642558},
  school      = {Universit{\"a}t Potsdam},
  pages     = {IX, 78},
  year      = {2024},
  abstract  = {This thesis presents an attempt to use source code synthesised from Coq formalisations of device drivers for existing (micro)kernel operating systems, with a particular focus on the Linux Kernel. In the first part, the technical background and related work are described. The focus is here on the possible approaches to synthesising certified software with Coq, namely the extraction to functional languages using the Coq extraction plugin and the extraction to Clight code using the CertiCoq plugin. It is noted that the implementation of CertiCoq is verified, whereas this is not the case for the Coq extraction plugin. Consequently, there is a correctness guarantee for the generated Clight code which does not hold for the code being generated by the Coq extraction plugin. Furthermore, the differences between user space and kernel space software are discussed in relation to Linux device drivers. It is elaborated that it is not possible to generate working Linux kernel module components using the Coq extraction plugin without significant modifications. In contrast, it is possible to produce working user space drivers both with the Coq extraction plugin and CertiCoq. The subsequent parts describe the main contributions of the thesis. In the second part, it is demonstrated how to extend the Coq extraction plugin to synthesise foreign function calls between the functional language OCaml and the imperative language C. This approach has the potential to improve the type-safety of user space drivers. Furthermore, it is shown that the code being synthesised by CertiCoq cannot be used in kernel space without modifications to the necessary runtime. Consequently, the necessary modifications to the runtimes of CertiCoq and VeriFFI are introduced, resulting in the runtimes becoming compatible components of a Linux kernel module. Furthermore, justifications for the transformations are provided and possible further extensions to both plugins and solutions to failing garbage collection calls in kernel space are discussed. The third part presents a proof of concept device driver for the Linux Kernel. To achieve this, the event handler of the original PC Speaker driver is partially formalised in Coq. Furthermore, some relevant formal properties of the formalised functionality are discussed. Subsequently, a kernel module is defined, utilising the modified variants of CertiCoq and VeriFFI to compile a working device driver. It is furthermore shown that it is possible to compile the synthesised code with CompCert, thereby extending the guarantee of correctness to the assembly layer. This is followed by a performance evaluation that compares a naive formalisation of the PC speaker functionality with the original PC Speaker driver pointing out the weaknesses in the formalisation and possible improvements. The part closes with a summary of the results, their implications and open questions being raised. The last part lists all used sources, separated into scientific literature, documentations or reference manuals and artifacts, i.e. source code.},
  language  = {en}
}
@misc{FrankKreitz2018,
  author    = {Frank, Mario and Kreitz, Christoph},
  title     = {A theorem prover for scientific and educational purposes},
  series = {Electronic proceedings in theoretical computer science},
  journal   = {Electronic proceedings in theoretical computer science},
  number    = {267},
  publisher = {Open Publishing Association},
  address   = {Sydney},
  issn      = {2075-2180},
  doi       = {10.4204/EPTCS.267.4},
  pages     = {59 -- 69},
  year      = {2018},
  abstract  = {We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.},
  language  = {en}
}
@book{FuhrmannSchubarthSchulzeReicheltetal.2019,
  author    = {Fuhrmann, Michaela and Schubarth, Wilfried and Schulze-Reichelt, Friederike and Mauermeister, Sylvi and Seidel, Andreas and Hartmann, Nina and Erdmann, Melinda and Apostolow, Benjamin and Wagner, Laura and Berndt, Sarah and Wippermann, Melanie and Ratzlaff, Olaf and Lumpe, Matthias and Kirjuchina, Ljuba and Rost, Sophia and Zurek, Peter Paul and Faaß, Marcel and Schellhorn, Sebastian and Frank, Mario and Kreitz, Christoph and Wagner, Nelli and Jenneck, Julia and Kleemann, Katrin and Vock, Miriam and Schr{\"o}der, Christian and Erdmann, Kathrin and Koziol, Matthias and Meißner, Marlen and Dibiasi, Anna and Unger, Martin and Piskunova, Elena V. and Bahmutskiy, Andrey E. and Bessonova, Ekatarina A. and Borovik, Ludmila K.},
  title     = {Alles auf Anfang!},
  series = {Potsdamer Beitr{\"a}ge zur Hochschulforschung},
  journal   = {Potsdamer Beitr{\"a}ge zur Hochschulforschung},
  number    = {4},
  editor    = {Schubarth, Wilfried and Mauermeister, Sylvi and Schulze-Reichelt, Friederike and Seidel, Andreas},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-452-4},
  issn      = {2192-1075},
  doi       = {10.25932/publishup-42296},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-422965},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {373},
  year      = {2019},
  abstract  = {Im Zuge der Bologna-Reform ist an Hochschulen vieles in Bewegung gekommen. Studium und Lehre sind st{\"a}rker ins Blickfeld ger{\"u}ckt. Dabei kommt der Studieneingangsphase besondere Bedeutung zu, werden doch hier die Weichen f{\"u}r ein erfolgreiches Studium gestellt. Deshalb ist es verst{\"a}ndlich, dass die Hauptanstrengungen der Hochschulen auf den Studieneingang gerichtet sind - ganz nach dem Motto: „Auf den Anfang kommt es an!". Konsens herrscht dahingehend, dass der Studieneingang neu zu gestalten ist, doch beim „Wie?" gibt es unterschiedliche Antworten. Zugleich wird immer deutlicher, dass eine wirksame Neugestaltung der Eingangsphase nur mit einer umfassenden Reform des Studiums gelingen kann. Ziel des vierten Bandes der Potsdamer Beitr{\"a}ge zur Hochschulforschung ist es, eine Zwischenbilanz der Debatte zum Studieneingang zu ziehen. Auf der Basis empirischer Studien werden unterschiedliche Perspektiven auf den Studieneingang eingenommen und Empfehlungen zur Optimierung des Studieneingangs abgeleitet. Die zahlreichen Untersuchungsergebnisse Potsdamer Forschergruppen werden durch weitere nationale sowie internationale Perspektiven erg{\"a}nzt. Der Band richtet sich an alle, die sich f{\"u}r die Entwicklung an Hochschulen interessieren.},
  language  = {de}
}
@article{SchellhornFrankKreitz2019,
  author    = {Schellhorn, Sebastian and Frank, Mario and Kreitz, Christoph},
  title     = {Br{\"u}ckenkurse f{\"u}r mathematische und informatiknahe Studieng{\"a}nge},
  series = {Alles auf Anfang! Befunde und Perspektiven zum Studieneingang},
  journal   = {Alles auf Anfang! Befunde und Perspektiven zum Studieneingang},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-452-4},
  issn      = {2192-1075},
  doi       = {10.25932/publishup-42853},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-428538},
  pages     = {257 -- 271},
  year      = {2019},
  language  = {de}
}