20-Apr-2015: BLAST 2.7.3 at SV-COMP'2015
BLAST 2.7.3 was presented at the 4rd International Competition on Software Verification (SV-COMP) held at TACAS 2015 in London, United Kingdom. This year BLAST has won the gold medal in the DeviceDrivers64 category.
BLAST is a classic software model checking tool based on predicate abstractions and CEGAR. It is maintained by ISPRAS as long as it is actively used within Linux Driver Verification (LDV) project.
This year we contributed to SV-COMP-2015 new benchmark tasks originated from the LDV project with more complex rule specifications. The contribution includes the following packages:
- ldv-linux-3.12-rc1 - Various tasks from Linux kernel 3.12-rc1 (including rule 144_2a, which requires accurate pointer tracking)
- ldv-linux-3.16-rc1 - Various tasks from Linux kernel 3.16-rc1 (including rule 205_9a requiring accurate arrays handling and rule 43_2a requiring bitvector support)
- ldv-validator-v0.6 - A set of tasks aimed to find actual bugs in Linux kernel that were originally detected in production use and that were fixed in stable releases of Linux kernel.
As we can see from the results the static verification tools do not work good on the new benchmarks. There were many false positives, false negatives and unknowns.
The following table presents the results for top 3 verification tools BLAST, Seahorn and CPAchecker in DeviceDrivers64 category on the new benchmarks:
| ldv-linux-3.12-rc1 (pointer tracking) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Total tasks | 40 | ||
| Correct results | 25 | 11 | 25 |
| False negatives | 0 | 0 | 0 |
| False positives | 2 | 1 | 0 |
| ldv-linux-3.16-rc1 (arrays) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Total tasks | 65 | ||
| Correct results | 33 | 19 | 14 |
| False negatives | 7 | 2 | 8 |
| False positives | 3 | 4 | 1 |
| ldv-linux-3.16-rc1 (bitvector) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Total tasks | 94 | ||
| Correct results | 73 | 56 | 70 |
| False negatives | 0 | 1 | 2 |
| False positives | 0 | 0 | 0 |
| ldv-validator-v0.6 (real bugs) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Total tasks | 22 | ||
| Correct results | 16 | 13 | 12 |
| False negatives | 0 | 0 | 0 |
| False positives | 0 | 0 | 0 |
We hope that there will be progress next year here, so we will be able to verify Linux kernel against more complex rule specifications.
We are very welcome the innovation in the SV-COMP rules requiring each tool to accompany each unsafe with an error trace in Common Error Trace (Witness) format. It allows us to visualize and analyze results for any static verification tool participating in the competition. For example, we have made experiments with the new tool Seahorn and we was able to analyze its error traces. This is a big step forward in comparison with earlier competitions where most of the tools were unusable for us without extra efforts!
Nevertheless, there is still a place to improve witness related rules of competition. First of all, the competition results show that there are many witness checking timeouts. It means that verification tools are penalized because of witness checkers are not able to verify witness quickly enough. According to the spirit of the competition verification tools should benefit from finding complicated bugs, while currently it is limited by abilities of witness checkers. To avoid the problem, we suggest to significantly increase time limits for witness checkers. At the same time, witness checkers tend to start guessing and reexploring state space when the witness is not precise enough and the checker does not know where to go next. As long as we do not want a witness checker to repeat verification, we could try to specifically limit time spent by witness checker in such situations.
