Linux Driver Verification

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.