16-Jan-2015: Version 0.7 of LDV Tools released
Submitted by admin on Fri, 16/01/2015 - 06:21
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 in Linux kernel 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.