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:

  •  improve the quality of Linux device drivers
  •  develop an integrated platform for device drivers verification
  •  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

Forge of the LDV project is here:
http://forge.ispras.ru/projects/ldv

Build instructions are here:
http://forge.ispras.ru/projects/ldv/wiki/Downloading_and_Building_LDV

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

Results

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

This outcome proves to be interesting for verification community as well. The international research group developing static analysis CPAchecker tool has adopted most of the drivers, in which we found bugs, as regression tests for their framework.

The LDV Team

  • Vladimir Gratinskiy
  • Alexey Khoroshilov
  • Mikhail Mandrykin
  • Vitaliy Mordan
  • Vadim Mutilin
  • Eugene Novikov
  • Ilya Shchepetkov
  • Ilya Zakharov

Many thanks to the former members of our team:

  • Oleg Strikov
  • Alexander Strakh
  • Pavel Shved
  • Marina Makienko