Linux Driver Verification

h1. LDV Validator

LDV Validator is a tool for validating LDV Tools verification system, in particular its back ends, i.e. verifiers like "BLAST":http://forge.ispras.ru/projects/blast/ or "CPAchecker":http://cpachecker.sosy-lab.org/. An approach, implemented in LDV Validator, is that LDV Tools are tried to find some known bugs in programs. If known bugs can be found using appropriate "specifications":http://forge.ispras.ru/projects/ldv-rules, then we prove that LDV Tools and corresponding verifiers work good. Otherwise we can miss bugs during verification in production. So we have reasons to revise LDV Tools or/and verifiers (sometimes we can have bugs in specifications as well).

h2. Sources of programs with known bugs

One of the simplest approaches to get programs with bugs is to introduce these bugs by ourselves. We used this approach very widely in preparing "test cases":http://forge.ispras.ru/projects/ldv/repository/revisions/master/show/ldv-tests/rule-models/drivers for LDV tools specifications. Obviously, we can''t cover all possible situations with these test cases. Thus we need other sources of programs with known bugs for validating LDV Tools.

We found out that programs with known nonartificial bugs can be efficiently obtained on the basis of the Linux kernel repositories. We have analyzed about 3 thousand commits made to "stable branches of the Linux kernel":http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/ since 26-10-2010 till 26-10-2011 [1]. This allowed us to find about 200 bugs related with Linux kernel API misuse - exactly those bugs which can be found with help of LDV Tools. Information on those bugs (commit hashes, module names, specification identifiers, etc.) was put to a configuration file.

[1] Khoroshilov A.V., Mutilin V.S., Novikov E.M. Analysis of typical faults in Linux operating system drivers. Proceedings of the Institute for System Programming of RAS, volume 22, 2012, pp. 349-374.

h2. LDV Validator workflow

LDV Validator gets a configuration file as input and automatically launches LDV Tools with specified verifier, obtains verification results and generates a report where one can find summary information as well as details on whether a particular bug was detected or not. Besides LDV Validator automatically checks Linux kernel modules after fixing bugs. This aids to understand whether LDV Tools or/and a verifier did find a bug fixed in corresponding commit.