Software verification with VeriFast: Industrial case studies

In this article, we present a series of four industrial case studies in software verification. We applied VeriFast, a sound and modular software verifier based on separation logic, to two Java Card smart card applets, a Linux device driver, and an embedded Linux network management component, the latter two written in C. Our case studies have been carefully selected so as to evaluate the industrial applicability of VeriFast. We focus on proving the absence of safety violations, e.g., that the programs do not perform illegal operations such as dividing by zero or illegal memory accesses. Yet, given the sensitive application environment of our case studies, these safety properties typically have security implications. In this article we give a detailed description of the VeriFast approach to software verification based on two of the above case studies, one in Java and one in C. Finally, we draw conclusions on the overall feasibility of using VeriFast to verify software components in industrial domains that have stringent requirements on reliability and security.

► We have verified 4 industrial case studies (Java Card and C code) using the VeriFast software verifier.
► We report on the findings (i.e. number of bugs found, time needed to annotate, verification time, etc.).
► We conclude that verification of industrial code is feasible.
► We give guidance on how to approach similar verification projects with VeriFast.