Linux Driver Verification

After more then 2 years of active development we are happy to announce that we released version 0.4 of LDV Tools. This version includes a lot of improvements and many bug fixes. In total it consists of about 900 commits that were made just in the LDV Tools repository not including submodules. The most significant changes are:

• Improvements in existing rule models: Module get/put, Atomic allocation in interrupt context, Mutex lock/unlock, Memory allocation under spinlocks, NOIO allocation under USB lock.
• Support of 25 new rule models: Possible TTY NULL dereference, Block requests, Usage of msleep(), USB gadget driver (de)registration, Initialization of spinlocks, Integer underflow in calling copy_from_user(), copy_to_user(), etc., Usage of spin_lock_irq*(), Usage of local_irq_*(), RW locks lock/unlock, probe() return values, Arguments of find_next_zero_bit(), Initialization of sysfs attributes, USB reference counting, Double kfree_skb(), Error handling in probe(), usb_deregister() and usb_serial_deregister(), netif_napi_add()/netif_napi_del(), napi_enable()/napi_disable(), register_netdev()/unregister_netdev(), alloc_netdev()/free_netdev(), Usage of mod_timer(), Usage of semaphores, Work with clocks, RCU read sections nesting, RCU update operations inside read sections, Initialization of completions.
• Fixing patterns for several driver callback structures to generate correct environment models.
• Introducing C Instrumentation Framework - a user-friendly interface for Aspectator.
• Supporting reusable blocks of aspect files and corresponding rearranging all existing rule models.
• Added ability to make source code querying with help of Aspectator, which is used in construction of rule models on the basis of instrumented source code (see corresponding news) and in generation of environment models.
• Support of a more user-friendly interface for reachability C verifiers.
• Switch to 2.7.1 version of BLAST - a default verifier of LDV Tools.
• Better integration with CPAchecker verifier that was included as submodule of LDV Tools.
• Integration with UFO verifier.
• Introducing a common format of error traces and improving visualization of error traces of different verifiers.
• Knowledge Base support for automatic marking unsafe verdicts of verifiers.
• Support for an automatic validation of LDV Tools and verifiers on known bugs in the Linux kernel.
• Coverage generation for debugging LDV Tools and different analyses of CPAchecker verifier.

Validation of LDV Tools 0.4 with different verifiers on 38 known bugs in the Linux kernel showed that:

• BLAST is able to detect 15 of them.
• CPAchecker is able to detect 13 of them.

The source code repository may be browsed by v0.4 tag. To get and to install LDV Tools see instructions.