Linux Driver Verification

Linux Driver Verification (LDV) program is aimed to meet increased demand for large-scale verification tools applicable to high profile software. The goals of the program are:
  •  to improve the quality of Linux kernel modules
  •  to develop an integrated platform for device drivers verification
  •  to adopt latest research outcome to enhance quality of verification tools

The quality improvement involves garnering and systematizing problems that occur in device drivers and actually finding their instances (bugs) in the source code.  Based on analysis of error reports to LKML, a number of frequently encountered problems was encapsulated into a rule database.  The rules are formalized, categorized, and supplied with machine-readable patterns that show how to verify them.

The integrated platform aims to mediate smoothly between driver's source packages, brand new, fresh kernels from kernel.org, rule database and general-purpose verification tools, given that all these are constantly developed.  This platform provides analysis of the drivers supplied in automatically deployed and generated environments, which are based on vanilla kernel sources and rule database mentioned earlier.

The verification process is backed with open-source verification tools for C language.  The modular architecture of the integrated platform, and a large amount of ready-to-check source code provides extensive basis for audit of quality of different verification tools.  The tools are constantly improved (based on research, both adopted and carried on by our group) and evaluated to provide the most precise verification.

We invite all interested parties to become a partner of the program.

Project Infrastructure

KLEVER Framework, the second generation of the tools developed within the project, is available here:
https://forge.ispras.ru/projects/klever

Development mailing list of LDV project is here: http://linuxtesting.org/cgi-bin/mailman/listinfo/ldv-project

The first generation of our tools called LDV Tools is available here: http://forge.ispras.ru/projects/ldv

Results

Of course, the numerous hours of computing power spent testing our tools were not wasted. More than 400 problems were found in Linux device drivers, and they have been already fixed in upstream. The list of problems found is constantly growing as the tools used are improved.

We have uploaded error traces for some of the problems found. You can investigate how LDV Tools results look like on these examples:

This outcome proves to be interesting for verification community as well. Verification tasks generated by LDV Tools are included into SV-COMP verification benchmarks and it has been adopted as regression tests for CPAchecker verification framework.

Publications

The basic architecture of the LDV Tools is described in the following paper:

Other papers are collected on the Publications page.

The LDV Team

  • Pavel Andrianov
  • Vladimir Gratinskiy
  • Alexey Khoroshilov
  • Mikhail Mandrykin
  • Vitaliy Mordan
  • Vadim Mutilin
  • Anton Vasilyev

Many thanks to the former members of our team:

  • Eugene Novikov
  • Ilya Shchepetkov
  • Ilya Zakharov
  • Oleg Strikov
  • Alexander Strakh
  • Pavel Shved
  • Marina Makienko

»