Modular Semi-automatic Formal Verification of Critical Systems Software

In the first part of this thesis, we present a case study on successfully verifying the Linux USB BP keyboard driver. Our verification approach is (a) sound, (b) takes into account dynamic memory allocation, complex API rules and concurrency, and (c) is applied on a real kernel driver which was not written with verification in mind.  We employ VeriFast, a software verifier based on separation logic.  Besides showing that it is possible to verify this device driver, we identify the parts where the verification went smoothly and the parts where the verification approach requires further research to be carried out.

In the second part of this thesis, we present a program verification approach that uses an input/output style of reasoning. It can be applied both to programs that perform input/output, and programs that do not but instead manipulate memory. The approach is sound, modular, compositional (I/O actions can be defined on top of other actions) and supports concurrency. It uses Petri nets and separation logic. We have implemented the approach, both for programs that do and do not perform I/O, in the VeriFast verifier and sketched how it can be implemented in the Iris framework for programs that perform I/O.