During Google Summer of Code 2012 Ph.D. student Evgeny Novikov managed by mentor Alexey Khoroshilov has successfully developed a project titled Advanced Source Code Instrumentation for the Linux Driver Verification Project for The Linux Foundation. A corresponding branch was merged to the master branch of the Linux Driver Verification project in 0491d9a.
The main feature implemented within the given project was ability to construct formal models of safety rules on the basis of program source code in the way independent of static verifier used for checks of rule models. Using this feature the LDV team enhanced existing rule models (Mutex lock/unlock and Spinlocks lock/unlock) and developed 7 new ones. Verification of Linux kernel drivers against these rule models with help of BLAST and CPAchecker tools demonstrated considerably lower rate of false positives in comparison with results obtained earlier and helped to discover several critical bugs.
In future we are planning to integrate the suggested approach with other approaches of rule models construction, e.g. based on automatic analysis of the Linux kernel core.
In frames of Google Summer of Code 2011 Ph.D. student Evgeny Novikov has successfully developed a project "User-friendly Interface for Linux Driver Verification Tools" with help of his mentor Alexey Khoroshilov for The Linux Foundation.
Within the given project a Knowledge Base support was developed. The Knowledge Base infrastructure allows users to keep results of unsafes analysis directly through the Statistics Server Web interface. Then these stored results are automatically applied to new uploaded unsafes in depend on different chosen comparison criteria. This significantly simplifies and speed ups the whole verification results analysis and makes the Linux Driver Verification project more attractive for end-users.
Also several minor issues of the Statistics Server related with usability and speed of page generation were resolved during Google Summer of Code 2011. One can see them here: #570, #1168, #1205, #1265, #1363, #1364, #1537, #1538
A Knowledge Base branch was merged to the master branch of the Linux Driver Verification project. It was successfully integrated with other tools, so stable Knowledge Base functionality is available beginning from 4ca264d.
We're going to continue develop and extend Knowledge Base infrastructure further. Keep in touch!
The most significant changes include:
- Three kernel rules were brought to a good quality level, and they now find more bugs: spin lock/unlock, memory allocation inside spin locks, and alloc/free urb — in addition to the good old mutex lock/unlock
- New Aspectator (aspect-oriented programming tool for C) was integrated into the projects, and the structure and the variable names of a program processed now looks nearly as well as the original one
- Concurrent and distributed execution of driver verification
- Support of CPAchecker static analysis tool, as well as of BLAST
See the downloading instructions to get these tools.
The source code repository may be browsed by v0.3 tag.
In the summer 2010, a Google Summer of Code 2010 project titled "Linux Device Drivers Quality Inspector" was developed for The Linux Foundation. Its developer was Andrey Tretyakov, and it was mentored by Alexey Khoroshilov. Within this project, an infrastructure to track changes in Linux Kernel's Git repository was developed, and the code called LDV tools as a "black box". The project was successfully completed and stashed.
We're glad to announce that the code developed during the program was merged into the master (trunk) branch of our project, and is now integrated with the rest of our toolset. You may find this code in revision 51e0ca2, or browse the repository. The component is now named "LDV-Git", and the code is now maintained by the LDV team (see bugs in LDV-Git in our bug tracker).
We'd like to thank Google and Andrey for their support.