From hardware verification to software verification: Re-use and re-learn

With the growing maturity in hardware verification methods, there has been great interest in applying them to verification of software programs. Aside from issues of scale and complexity, there are many differences between the two domains in the underlying problem of searching for bugs. In this talk, I will describe our experiences with this transition, with emphasis on methods that worked and those that did not. Verification methods based on Boolean Satisfiability (SAT) have emerged as a promising alternative to BDD-based symbolic model checking methods [8]. We have developed an efficient platform for SAT-based model checking [4], called VERISOL, which has been used successfully in industry practice to verify large hardware designs. It uses an efficient circuit representation with on-the-fly simplification algorithms, an incremental hybrid SAT solver, and utilizes several SAT-based engines for finding bugs (bounded model checking) and proofs (proof-based abstraction, SAT-based induction). Inspired by its success on hardware designs, we attempted to re-use VERISOL for performing model checking in the back-end of F-SOFT [6], which is targeted for verifying C programs. We first derive a control flow graph (CFG) representation of the program, use static code analyses (program slicing, range analysis, constant folding) to simplify and reduce the CFG, and then derive a symbolic circuit model (under assumptions of finite data and finite recursion). The resulting bit-accurate circuit model of the program is then verified by VERISOL. Our direct attempt at using hardware verification methods for verifying software models did not lead immediately to success. The two main problems were that the number of variables was too high, and BMC needed to go too deep. We therefore proposed several customized SAT-based heuristics to exploit the high-level structure in CFG models, which greatly improve SAT solver performance [5]. We have also proposed path balancing transformations on the CFG model, which enable additional onthe- fly simplification during BMC to improve performance [3]. To reduce the burden on the model checker, we use program analysis methods for static invariant generation [9] to find proofs more cheaply for array buffer overflow and pointer dereference errors. In our experience, a combination of these methods with SAT-based BMC works much better than predicate abstraction refinement for these checks, since the number of predicates and the number of refinement iterations tend to blow up. To address the problem of bugs being too deep (when starting from the main function in a C program), we start verification from some intermediate function by considering a default abstract environment at its interface. This re-uses the idea of a localization reduction [7]. A counterexample reported by the model checker may be spurious due to missing environment information.We use these counterexamples to guide environment refinement (CEGER). This is similar to standard CEGAR [2] or predicate abstraction refinement [1], except that we use it to refine only the environment, not the model of the program. The CEGER loop is not completely automated - we require help from the user to identify the spurious behavior and guide the refinement. However, the model checker assists the user by providing a concrete error trace, and a weakest precondition as a suggestion for the interface constraint. In practice, users find it much easier to modify a suggested constraint, than to create one. With these techniques to scale up and supplement model checking for software programs, the F-SOFT platform has recently been used to start an in-house verification service within NEC. To date, it has found more than 450 likely bugs (many confirmed by developers) in four projects totalling 1.1 MLOC (with one 600 kLOC project).