Google Summer of Code 2012 project was merged to master
"Advanced Source Code Instrumentation" project developed during Google Summer of Code 2012 was merged to master of the Linux Driver Verification project.
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.
Comments