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.