17-Apr-2014: BLAST 2.7.2 at SV-COMP'2014 and LDV experiments

BLAST 2.7.2 was presented at the 3rd International Competition on Software Verification held at TACAS 2014 in Grenoble, France. This year BLAST won the gold medal in the DeviceDrivers64 category.

Since we look at the competition results from the perspective of the Linux Driver Verification project, we conducted several experiments with the best tools in the DeviceDrivers64 category, namely BLAST, UFO, FrankenBit and CPAchecker, We checked correctness of mutexes usage on about four and a half thousand drivers from Linux kernel 3.12-rc1.

We have taken competition versions and configurations of all the tools except CPAchecker, for which we used the default configuration from LDV Tools, because the competition one gave much more false unsafes. One of the causes is that the LDV Tools configuration disables conservative handling of function pointers that are actively used in Linux device drivers.

An interesting result of the analysis is that CPAchecker and BLAST found the same number of bugs, but these bugs were different. Both tools have found 53 bugs, while 12 bugs were different. For CPAchecker one unsafe of 54 was false. UFO and FrankenBit reported less unsafes (20 and 31) and they also were different. But as far as we faced problems with analysis of error traces produced by UFO and FrankenBit, we could not tell how many unsafes represent actual bugs. Experiments showed that UFO is the fastest tool. It operated 1,5 times faster than BLAST, 3 times faster than FrankenBit and 3,5 times faster than CPAchecker.

The main conclusion is that as far as the tools report different bugs, it makes sense to use them in a complementary way.

We also found that an error trace produced for each unsafe is crucial for understanding whether it is a false alarm or not. At least, it should be possible to analyze error traces without knowing implementation details of a verification tool. A common representation of error traces required by the competition rules would ease usage of tools for driver verification, since error traces from different tools could be converted in the same way for uniform visualization and analysis with the help of LDV Tools.