ELISA Webinar #2: Linux Driver Verification & KLEVER: Applying formal methods on the Linux kernel for various years

Lukas Bulwahn

Linux Driver Verification & KLEVER: Applying formal methods on the Linux kernel for various years
Presenter: Evgeny Novikov, ISPRAS

Date: 2019-05-27
Time: 22:00 JST; 21:00 CST; 16:00 MSK; 15:00 CEST; 06:00 PDT   
Formal methods help to ensure the highest level of software quality that can contribute to the activities for safety and security-related projects. But as a rule they are successfully applied just for small, specially prepared programs (a dozen KLOC at most). The Linux kernel represents a huge, rapidly developed, legacy software. Researchers and developers constantly try to leverage formal methods to various parts of the Linux kernel. I would like to introduce you software verification framework Klever [1] that we have been developing more than 10 years at the Linux Verification Center [2] within the Linux Driver Verification (LDV) [3] program.
Klever allows automated checking of Linux kernel loadable modules and subsystems against a variety of safety and security requirements using software verification tools implementing such methods of thorough static analysis as Bounded Model Checking [4] and Counterexample-Guided Abstraction Refinement [5]. Klever can complement traditional software quality assurance tools for code review, testing and static analysis. In contrast to various kinds of testing the framework treats all execution paths and checks for requirements according to provided specifications. Unlike static analysis tools, it proves formal correctness of programs checked against particular requirements under certain assumptions. Altogether this enables revealing tricky faults in software including crucial ones. Concerning verification of the Linux kernel, this framework already demonstrated an ability to detect faults [6], many of which can be hardly found out by other techniques.
Potentially, Klever is able to detect much more if one invests in developing specifications, conducting verification, analysis of verification results and reporting bugs. We consider possible directions for further development of Klever that can contribute verification of the Linux kernel in some way in this document:
Everything related with verification of the Linux kernel in Klever is open source [7].
Online Meeting will either use the previous Skype setup or Linux Foundation Goto Meeting setup.