Linux Driver Verification Program

Linux Driver Verification (LDV) Linux Driver Verification (LDV) program was announced in 2009 to meet increased demand for large-scale verification tools applicable to high profile software. The goals of the program are:

  • improve 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, categotized, 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.

Current Status

A research concerning common problems encountered in Linux device drivers was held in 2008. At the beginning of 2009 a generic approach to checking drivers was developed.

During the rest of 2009 the integrated verification system was prototyped. One of the core components of the approach, a feature-rich tool to support aspect-oriented programming for C language, was developed. We also improved BLAST static source code checker to handle large amounts of code faster.

Having started in March 2010, we are now developing a ready-to-use version of the integrated platform and getting it ready to be exposed as an online service at linuxtesting.org in August 2010. Stay tuned!

Results

Of course, the numerous hours of computing power spent testing our tools were not wasted. A number of problems was found in Linux 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

  • Vadim Mutilin
  • Eugene Novikov
  • Alexander Strakh
  • Pavel Shved
  • Alexey Khoroshilov