Go back to the main GSoC Linux Foundation page

Mailing list: lsb-discuss at lists dot linux-foundation dot org

IRC: #lsb on irc.freenode.net

Workgroup Resources

Code License: GPL/BSD, specs: GNU FDL

Mentors: Alexey Khoroshilov (alexey dot khoroshilov at gmail dot com), Jeff Licquia, Vladimir Rubanov, Denis Silakov (dsilakov at gmail dot com).

Linux Driver Verification (LDV) program is devoted to developing an integrated framework for device drivers verification and adopting leading edge research results to enhance quality of verification tools. Currently LDV tools are used to check Linux device drivers against several safety rule specifications, each of them formally defines what is correct usage of a particular part of kernel core API. Another way of looking at the safety rules is that a rule represents one or more typical misuse of kernel core API.

By the moment, the framework contains around 30 rule specifications that has already helped to find and fix more than 250 issues in device drivers of vanilla Linux kernel.

This project (or several ones) is aimed at extending number of rules supported by the framework.

We have a collection of several dozens rules written in informal way, but other rules can be used as well. Formalization process usually includes the following steps:

• identification of all elements of kernel core API relevant to the rule;
• writing a rule specification that consists of
  
  • model state (one or more C variables);
  • transitions between states linked to appropriate events in device driver (usually calls of kernel core API);
  • a set of assertions (that represents misuse of kernel core API);
• writing unit tests covering all the interfaces;
• checking all drivers against the rule, analyzing results, reporting bugs and fixing the rule specification.

Rule specifications are written in a mix of C code and AspectJ-like notation that allows to merge the model code with original source code of device driver.

More than one application can be approved. Formalization of ~5 rules is expected from each student.

Desired knowledge: C, aspect-oriented programming, Linux kernel space API
Mentors: Alexey Khoroshilov, Vadim Mutilin, Eugeny Novikov