Linux Driver Verification

LDV Tools 0.8 comes with the following improvements:

• Update the CPAchecker verification tool to the new version 1.4.
• LDV Tools are now available as Docker images, so you can avoid installation of all dependencies on your machine.
• Improvements in 13 existing rule specifications:
  • Driver becomes not available for unloading permanently.
  • Locking a mutex twice or unlocking without prior locking.
  • Usage of spin lock and unlock functions.
  • Usb alloc/free urb.
  • Possible TTY NULL dereference.
  • Atomic allocation in interrupt context.
  • Memory allocation inside spinlocks.
  • NOIO allocation under usb_lock.
  • Initialization of completion.
  • Error handling in probe().
  • All obtained blk requests should be put after all.
  • Calling find_next_zero_bit() with arguments in the right order.
  • Usb device reference counting with usb_get_dev/usb_put_dev and interface_to_usbdev.
• Adding 3 new rule specifications:
  • Correct usage of sysfs groups.
  • Correct usage of IO memory mappings.
  • Correct allocation of identifiers using IDR layer.

Results of validation of LDV Tools 0.8 and LDV Tools 0.7 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

		LDV Tools 0.8		LDV Tools 0.7
		BLAST	CPAchecker	BLAST	CPAchecker
Found bugs		19	18	19	15
Missed bugs	Due to bugs in verification tools	3	2	3	2
	Out of memory (63 gigabytes)	2	0	1	2
	Timeouts (50 minutes)	0	5	0	6
	Due to other reasons	17	16	18	16

The new version of CPAchecker was able to find three more reference bugs in Linux kernel thanks to improvements described here.

The source code repository can be browsed by v0.8 tag. To get and to install LDV Tools see instructions. If you want to use prebuilt LDV Tools, please follow our LDV Tools in Docker instructions.

LDV Tools 0.7 comes with quite a lot improvements and bug fixes:

• Compatibility with Linux kernel 3.17-3.19.
• Improvements in 12 existing rule specifications:
  • sysfs_attr_init() call before device_create_file() call.
  • usb_deregister()/usb_serial_deregister().
  • Usb alloc/free urb.
  • Possible TTY NULL dereference.
  • Atomic allocation in interrupt context.
  • Memory allocation inside spinlocks.
  • NOIO allocation under usb_lock.
  • Initialization of completion.
  • Locking and unlocking SDIO bus.
  • Underflow in call copy_from_user() etc.
  • All allocated socket buffers should be freed.
  • Error handling in probe().
• Verification on a remote host using BLAST in a Docker container.
• Verification in the CPAchecker cloud.
• Support of Public Pool of Bugs.
• Many bug fixes and several new features in Rule Instumentor and CIF - LDV Tools components used to weave specifications into source code under verification.
• Numerous improvements and bug fixes in components for uploading and visualizing verification results.

Results of validation of LDV Tools 0.7 and LDV Tools 0.6 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

		LDV Tools 0.7		LDV Tools 0.6
		BLAST	CPAchecker	BLAST	CPAchecker
Found bugs		19	15	17	13
Missed bugs	Due to bugs in verification tools	3	2	3	2
	Out of memory (63 gigabytes)	1	2	1	2
	Timeouts (50 minutes)	0	6	0	6
	Due to other reasons	18	16	20	18

Both BLAST and CPAchecker were able to find two more reference bugs thanks to improvements in rule specifications sysfs_attr_init() call before device_create_file() call and usb_deregister()/usb_serial_deregister().

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

Vitaly Mordan successfully finished Google Summer of Code 2014 project Public Pool of Bugs in Linux Kernel Modules under Evgeny Novikov supervision.

In summer of code Vitaly made the following:

• Wrote a comprehensive specification of Public Pool of Bugs in which all requirements of LDV Tools developers for that project were considered.
• Extended linuxtesting.org in order to present LDV Tools verification results beyond the ISP RAS. New web pages were developed to represent full information about found bugs/false alarms (for the Linux kernel developers) and to edit information (for the LDV Tools developers).
• Extended LDV Knowledge Base and LDV Analytics Center in order to make it possible to publish verification results (such as kernel version, module, corresponding error trace, verdict, etc) to linuxtesting.org and to synchronize them later.
• Developed an authorization module for LDV Analytics Center to exclude an accidental publishing of unnecessary data, so only authorized users could publish verification results.

All changes to LDV Tools components were merged to master in 363f810.

Completing this project made possible to share any new found potential bugs in Linux kernel modules with its full description with the Linux kernel developers. In future this project will increase the number of found bugs in Linux kernel modules with the help of LDV Tools.

Ilja Zakharov successfully finished Google Summer of Code 2014 project Parallel Verification of Linux Kernel Modules under Evgeny Novikov supervision.

During the project Ilja made an overview of available technologies of cloud and distributed computing which are suitable for software verification tools deployment - the actual task since such tools are characterized by high time and memory consumption. Working in touch with other LDV developers he also contributed to the new perspective version of LDV Tools which is still under development. As a result he improved performance of verification task generation and proceeded with a solution of an infrastructure for establishing distributed Docker-based verification. As a part of the project Ilja also implemented verification on a remote host using BLAST in a Docker container and CPAchecker cloud web-interface task submitting. The latter was merged to master in 960e64e.

LDV Tools 0.6 includes the following most important changes:

• Compatibility with Linux kernel 3.14-3.16.
• Improvements in 5 existing rule specifications:
  • Initialization of sysfs attributes.
  • Possible TTY NULL dereference.
  • Initialization of spinlocks.
  • SKB allocation in pm_runtime context.
  • RW locks lock/unlock (more precise implementation).
• Adding 11 new rule specifications:
  • Memory releasing in the USB subsystem.
  • RCU critical section for rcu_dereference().
  • Initialization of USB request blocks.
  • SCSI DMA (un)mapping.
  • PCI DMA (un)mapping.
  • Memory regions allocation/releasing.
  • Memory caches allocation/releasing.
  • DMA pools allocation/releasing.
  • SKB allocation/releasing.
  • IRQ request/free.
  • Kernel threads creation/stop.
• Update the CPAchecker verification tool to version 1.3.4 (r12604).
• Fixing most of memory-related issues, especially memory leaks, in Aspectator and C-backend of the CIF component (now they consume up to 1000 times less memory on large aspect files).
• Optimization of Aspectator that reduces instrumentation time in about 25 times on specific large aspect files.
• Alternative implementation of the script uploading LDV verification reports into databases that operates several dozen times faster.

Results of validation of LDV Tools 0.6 and LDV Tools 0.5 with different verification tools on 41 known bugs in the Linux kernel* are presented in the table below.

		LDV Tools 0.6		LDV Tools 0.5
		BLAST	CPAchecker	BLAST	CPAchecker
Found bugs		17	13	15	14
Missed bugs	Bugs in verification tools	3	2	3	3
	Out of memory (63 gigabytes)	1	2	1	0
	Timeouts (50 minutes)	0	6	0	4
	Unsupported rule specifications	0	0	7	7
	Others	20	18	15	13

Both BLAST and CPAchecker were able to find one more bug thanks to improvements in rule specification SKB allocation in pm_runtime context. Additionally BLAST has found a new bug with one of the new rule specifications. CPAchecker has lost ability to detect 3 bugs due to degradation in analysis time, while it has found a bug that led to an exception before.

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

* This validation benchmark has many differences from the one used earlier for validating LDV Tools 0.5.

The major feature of this release is a control groups based resource manager aimed to limit and to count resource consumption of verifiers. Linux control groups allow to perform very accurate measurements without any noticeable overhead. Other important changes are as follows:

• Support for automatic verification of modules of the Linux kernel in user-defined configurations, including different computer architectures.
• Addition of the new rule specification Locking and unlocking SDIO bus.
• Improvements in existing rule specifications: Module get/put and Block requests.
• Fixing all known segmentation faults in Aspectator.
• Switch to 2.7.2 version of BLAST verifier.
• Support of CBMC verifier as one of LDV Tools' back ends.
• Introducing a standalone error trace visualization tool.

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

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

In comparison with LDV Tools 0.4 6 known bugs were removed from the validation benchmark since they do not fit existing rule specifications, while 5 new known bugs were added to the benchmark (3 due to support of user-defined configurations, 1 due to addition of the new rule specification and 1 due to determining of an appropriate environment model). LDV Tools can detect two of those new bugs with help of BLAST verifier.

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

Master's student Ilja Zakharov under Vadim Mutilin supervision successfully finished Google Summer of Code 2013 project Generation of Environment Model for Verification of Multi-module Device Drivers for The Linux Foundation.

Ilja worked in the following directions:

1. Experiments with extraction of interconnected Linux kernel modules.
2. New implementation for a Linux-related stack of components of the LDV Tools.

Ilja developed a new approach for extracting a graph of all interconnected Linux kernel modules and a new method for a graph clusterization specific for verification purposes. Obtained groups of modules rarely exceed 5 modules in size. Further research for generating environment model and study of corner cases lie ahead.

Kernel Manager, Build Command Extractor and Command Stream Divider components of the LDV Tools were completely redesigned. The most notable features that they support now include an adjustment on the basis of an extendable common configuration, a results caching, various strategies of module extraction and an extracting of the Linux kernel modules for the ARM architecture. Also a new architecture of these components allow to avoid all old bugs like this. Integration of the components with LDV Tools is ongoing.

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.

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.

In Google Summer of Code 2012 Ph.D. student Mikhail Mandrykin managed by mentor Alexey Khoroshilov has successfully developed a project titled Formalization of Correct Usage of Kernel Core API for The Linux Foundation. A corresponding branch was merged to the master branch of the Linux Driver Verification project in 5ee5b4e.

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

1. Possible TTY NULL dereference (commits 1, 2)
2. The gadget driver (de)registration (commits 1, 2, 3, 4, 5)
3. Refcounting with usb_get_dev()/usb_put_dev() (24 suspicious drivers)
4. Don't call kfree_skb twice (no actual problems were found)
5. Error handling in probe() (commits 1 and 5 suspicious drivers)