Linux Driver Verification
- 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.
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
Of course, the numerous hours of computing power spent testing our tools were not wasted. More than 260 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.
The basic architecture of the LDV Tools is described in the following paper:
- Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Alexander Petrenko, Ilya Zakharov
Configurable toolset for static verification of operating systems kernel modules
Programming and Computer Software, 2015, Volume 41, Number 1, pages 49-64.
Other papers are collected on the Publications page.
The LDV Team
- Pavel Andrianov
- Vladimir Gratinskiy
- Alexey Khoroshilov
- Mikhail Mandrykin
- Vitaliy Mordan
- Vadim Mutilin
- Eugene Novikov
- Ilya Shchepetkov
- Anton Vasilyev
- Ilya Zakharov
Many thanks to the former members of our team:
- Oleg Strikov
- Alexander Strakh
- Pavel Shved
- Marina Makienko