Challenges and applications of assembly level software model checking

Abstract

This thesis addresses the application of a formal method called Model Checking to the domain of software verification. Here, exploration algorithms are used to search for errors in a program. In contrast to the majority of other approaches, we claim that the search should be applied to the actual source code of the program, rather than to some formal model. There are several challenges that need to be overcome to build such a model checker. First, the tool must be capable to handle the full semantics of the underlying programming language. This implies a considerable amount of additional work unless the interpretation of the program is done by some existing infrastructure. The second challenge lies in the increased memory requirements needed to memorize entire program configurations. This additionally aggravates the problem of large state spaces that every model checker faces anyway. As a remedy to the first problem, the thesis proposes to use an existing virtual machine to interpret the program. This takes the burden off the developer, who can fully concentrate on the model checking algorithms. To address the problem of large program states, we call attention to the fact that most transitions in a program only change small fractions of the entire program state. Based on this observation, we devise an incremental storing of states which considerably lowers the memory requirements of program exploration. To further alleviate the per-state memory requirement, we apply state reconstruction, where states are no longer memorized explicitly but through their generating path. Another problem that results from the large state description of a program lies in the computational effort of hashing, which is exceptionally high for the used approach. Based on the same observation as used for the incremental storing of states, we devise an incremental hash function which only needs to process the changed parts of the program’s state. Due to the dynamic nature of computer programs, this is not a trivial task and constitutes a considerable part of the overall thesis. Moreover, the thesis addresses a more general problem of model checking - the state explosion, which says that the number of reachable states grows exponentially in the number of state components. To minimize the number of states to be memorized, the thesis concentrates on the use of heuristic search. It turns out that only a fraction of all reachable states needs to be visited to find a specific error in the program. Heuristics can greatly help to direct the search forwards the error state. As another effective way to reduce the number of memorized states, the thesis proposes a technique that skips intermediate states that do not affect shared resources of the program. By merging several consecutive state transitions to a single transition, the technique may considerably truncate the search tree. The proposed approach is realized in StEAM, a model checker for concurrent C++ programs, which was developed in the course of the thesis. Building on an existing virtual machine, the tool provides a set of blind and directed search algorithms for the detection of errors in the actual C++ implementation of a program. StEAM implements all of the aforesaid techniques, whose effectiveness is experimentally evaluated at the end of the thesis. Moreover, we exploit the relation between model checking and planning. The claim is, that the two fields of research have great similarities and that technical advances in one fields can easily carry over to the other. The claim is supported by a case study where StEAM is used as a planner for concurrent multi-agent systems. The thesis also contains a user manual for StEAM and technical details that facilitate understanding the engineering process of the tool.