Ivannikov Institute for System Programming of the RAS


Linux Driver Verification (LDV)

Start of project – 2009.

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.

Implementer

Software Engineering

Go to the list of projects