Linux Driver Verification

The major feature of this release is a control groups based resource manager aimed to limit and to count resource consumption of verifiers. Linux control groups allow to perform very accurate measurements without any noticeable overhead. Other important changes are as follows:

• Support for automatic verification of modules of the Linux kernel in user-defined configurations, including different computer architectures.
• Addition of the new rule specification Locking and unlocking SDIO bus.
• Improvements in existing rule specifications: Module get/put and Block requests.
• Fixing all known segmentation faults in Aspectator.
• Switch to 2.7.2 version of BLAST verifier.
• Support of CBMC verifier as one of LDV Tools' back ends.
• Introducing a standalone error trace visualization tool.

Validation of LDV Tools 0.5 with different verifiers on 37 known bugs in the Linux kernel showed that:

• BLAST is able to detect 13 of them.
• CPAchecker is able to detect 11 of them.

In comparison with LDV Tools 0.4 6 known bugs were removed from the validation benchmark since they do not fit existing rule specifications, while 5 new known bugs were added to the benchmark (3 due to support of user-defined configurations, 1 due to addition of the new rule specification and 1 due to determining of an appropriate environment model). LDV Tools can detect two of those new bugs with help of BLAST verifier.

The source code repository can be browsed by v0.5 tag. To get and to install LDV Tools see instructions.