Linux Driver Verification

In Google Summer of Code 2012 Ph.D. student Denis Efremov managed by mentor Alexey Khoroshilov has successfully developed a project titled Formalization of Correct Usage of Kernel Core API for The Linux Foundation.

Denis implemented 12 formal models for safety rules that help him to find a lot of bugs in Linux kernel drivers:

1. Enabling interrupts while in an interrupt handler (commits 1, acked 1)
2. might_sleep functions in interrupt context (found the same results as less general variants of the given rule)
3. Spinlocks acquisition in process and interrupt contexts (5 suspicious drivers)
4. local_irq_enable/disable and local_irq_save/restore order (commits 1, 2)
5. rcu_dereference() outside of rcu_read_lock/unlock (commits 1, 2, 3, 4)
6. might_sleep functions with disabled interrupts (7 suspicious drivers)
7. Inlined functions marked with EXPORT_SYMBOL (commits 1)
8. might_sleep functions in spinlock context (verification results need to be carefully analyzed)
9. might_sleep functions in rcu_read_lock/unlock (verification results need to be carefully analyzed)
10. Requesting a threaded interrupt without a primary handler and without IRQF_ONESHOT (needs more accurate driver environment)
11. Initialization functions marked with EXPORT_SYMBOL (found bugs seems not to be critical)
12. BUG like macros in interrupt context (rule highly depends on user purposes, thus it was rejected)

To develop 5 of these rule models Denis has suggested a new approach of an automatic construction of a Linux kernel core model. This approach is based on a suggestion if some program interface may invoke directly or indirectly some specific program interface (like might_sleep macro) then it can be marked respectively (e.g. as might_sleep interface). The approach was implemented in the following way:

1. Creates list of program interfaces used by some Linux kernel module, in particular by a driver.
2. Linux kernel source code is analyzed with help of cscope tool.
3. On the basis of a generated cscope base a call graph containing program interfaces of interest (e.g. might_sleep macro) is created.
4. Intersects lists of program interfaces obtained at 1st and 3rd steps. Thus obtains a list of program interfaces that can, say, sleep, and that are used by the module.
5. Constructs a rule model on the basis of the list obtained at 4th step. For instance, checks a specific context for program interfaces from the given list.

Several rule models were merged to the master branch of the Linux Driver Verification project. To merge other rule models we need to integrate tools developed by Denis with LDV tools.