13-May-2015: Version 0.8 of LDV Tools released
Submitted by Vadim Mutilin on Wed, 13/05/2015 - 07:57
LDV Tools 0.8 comes with the following improvements:
- Update the CPAchecker verification tool to the new version 1.4 (r14998).
- 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:
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 build LDV Tools from sources see build instructions. If you want to use prebuilt LDV Tools, please follow LDV Tools in Docker instructions.