This paper reports on four case studies using VeriFast to verify real code for an absence of safety violations such as illegal memory accesses or data races.
The paper starts with a very nice overview of the features of VeriFast and then describes the four case studies
- eID (Java) The Belgian Electronic Identity Card.
- PEP (C) Embedded Linux Network Management Software.
- USB BP (C) The Linux USB BP Keyboard Driver (brief description because it has been described elsewhere)
- SECURECHANGE (Java) (brief description because it has been described elsewhere)
An interesting thing found in the SECURECHANGE study was that, despite previously having been verified using Why/Krakatoa/Caduceus bugs were found. They say “Clearly, the tool used earlier was not sound or was not used in a sound way.”
This kind of case study paper is really useful because it gives some insight into how to tackle an unverified piece of code.
- Start by adding pre/post-conditions of true/true to all functions. (This will gradually flush out some more realistic conditions.
- Create specifications of all the libraries used. One technique used was to use “gcc -E” to make a header file for all the system library imports and delete everything that is not used.
- Delay handling threads by initially specifying that “pthread_create” immediately calls its function argument and runs it until it terminates.
This was also useful because they document the amount of annotation required in each case.
Note that they also did some work on annotation inference and I don’t think all the data reflects those improvements. In the related work section, they suggest that other tools such as VCC would not need as much annotation but at the expense of less predictable search time.
Notes related to Software verification with VeriFast: Industrial case studies
Papers related to Software verification with VeriFast: Industrial case studies
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]