Research On Analysis And Verification Techniques For Heap-Manipulating Programs

Heap memory has gained flexible and powerful support for modern computer software. In order to manipulate heap memory, recursive data structures are widely used by programmers of C-like programming languages. List is one of the most frequently adopted data structures especially in OS kernel and drivers. However, the shape of the recursive data structures including lists and trees are complex and mutable. Also, the pointers pointing to these data structures can be used in various ways. The result is that heap operations become one of the most important sources of program errors. Formal analysis and verification, which aim to eliminate errors and construct trustworthy software, are especially important for safety-critical software used in aeronautics, astronautics, national defense, military, finace, tranffic, etc. However, the broad usage of recursive data structures brings many challenges for the analysis and verification of heap-manipulating programs. The abstract model for these recursive data structures plays an important role for analyzing and verifying heap-mainpulating programs.This thesis focuses on abstract models for recursive data structures and the analysis and verification techniques of heap-manipulating programs, taking list as an example. Major contributions of this thesis are listed as follows.1) We present a new abstract model for list. The new model enjoys low space overhead by storing the edges between nodes in a list implicitly and representing the list states in a compact manner. It also enjoys high precision by maintaining the length of lists automatically. Specifically, we introduce a so-called Variable Reachability Vector Set with Counters and use it as an abstract model for each list state. After introducing a so-called"cut"operation and the labelling bit for cycle extension, our approach could model all singly-linked lists including cyclic cases. By maintaining one Variable Reachability Vector Set with Counters for each list field, our approach can also model well-founded doubly-linked list. At last, we carry out experiments in a symbolic execution framework using the newly presented abstract model. The experimental results show that the new abstract model can be used to analyze various kinds of trustworthy properties of heap-manipulating programs.2) We present a symbolic numeric abstraction framework to verify quantitative properties of recursive data structures. The framework transforms heap-manipulating programs into pure numeric programs while keeping its quantitative properties. We take list manipulating programs as an example to explain how to instantiate the framework for complex data structures and to exhibit its practicability. Quantitative shape analysis process is designed and implemented based on symbolic execution to generate a so-called Abstract State Transition Graph, which is the core intermediate representation in the framework. The numeric abstraction process is designed and implemented based programm slicing to get a pure numeric program, which is then inputted into existing numeric reasoning tools to verify the desired property. We have implemented a prototype tool for this framework and use it to verify some non-trivial list manipulating programs. Experimental results show the effectiveness and practicality of the framework.3) We present a so-called List Shape Quantitative abstact domain based on the newly presented abstract model. The new abstract domain can be used to generate program invariants describing both shape properties and quantitative properties of recursive data structures, which are especially useful for verifying heap-manipulating programs. We define the domain representation and the domain operations by combining interval abstract domain and affine equality abstract domain. Transfer functions for basic list operations are also presented accordingly. The analyzing results for actual programs show that the invariants found using this new abstract domain are very powerful, and can be usned to verify various kinds of properties of heap-manipulating programs.4) We design and implement two prototype tools for analyzing heap bounds. Firstly, a heap bound analyzer for list manipulating programs is designed and implemented based on the newly presented symbolic numeric abstraction framework. By instrumenting heap usage modelling statements in the abstract state transition graph, and then obtaining the corresponding numeric abstraction, the problem of finding heap bounds is transformed into the maximum problem in a pure numeric program. Secondly, a practical heap bound analyzer is designed and implemented based on KLEE, a powerful symbolic execution tool. Loop strategy is also introduced based on the characteristics of the problem of heap bounds, and heap allocation cases with symbolic parameters and the loops with symbolic iteration number can then be handled. Experimental results show that these two prototype tools can be used to find fairly precise heap bounds for many non-trivial and practical programs.