Linux Driver Verification

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.