Validating Model Verification Tools Via Fuzzing Techniques

Model verification is an important verification technique.Given a software or hardware model and corresponding safety properties,model verification technique can report the safety of the system automatically.Since this technique was proposed,it has been widely noticed.Industry companies have been using model verification technique in their hardware design and software development process,and the corresponding model verification tools have also been proposed continuously.However,except the large companies are willing to develop model verification tools for their special requirements,in ordinary software development and hardware design process,people are not willing to apply model verification technique.It is due to several reasons,one of the most important reason is the model verification tools are not mature enough to be applied.In practice,the users of open-sourced model verification tools usually encounter many problems,such as,soundness bugs,crashes and usability issues.It is due to the lack of the systematic,dedicated and effective testing techniques for model verification tools.So far,the developers only use limited number of test cases to validate the reliability of the model verification tools,obviously,it is far from enough.Towards this problem,this thesis systematically proposes a group of fuzzing techniques for testing model verification tools,which improves the reliability of the tools and pushes forward the application of model verification techniques.Fuzzing is an automatic methodology for generating test cases,it has been successful on testing various kinds of software.However,applying fuzzing on testing model verification is still challenging.The challenges are as follows: First,how to automatically generate test inputs that satisfy the input standards of model checker tools.Second,how to automatically obtain the test oracles.Third,which is the most important,how to find real bugs in model checker tools.Towards these three challenges,this thesis proposes the following fuzzing techniques and corresponding tools:·Circuit Structure Mutation:Hardware model checkers are the model verification tools for hardware,while circuit structure mutation is an fuzzing approach for hardware model checkers.The key idea is to mutate the existing circuit graph by manipulating the relations among the components while preserving the validity of mutants.Based on circuit structure mutation,we implemented a tool named AIGMutator,it found 9 unique bugs in three state-of-the-art hardware model checkers.·Reachability Query:Software model checkers are the model verification tools for software programs,while Reachability Query is an fuzzing approach for testing software model checkers.The key idea is to actually execute the program to obtain the reachability of the branches,and synthesis the safety properties by the known reachabilities,then use the safety properties along with the program to test software model checkers.Based on reachability query,we implemented a tool named MCFuzz,it found 62 unique bugs in three state-of-the-art software model checkers.·Semantic Fusion:SMT solvers are the core components of model checkers,while Semantic Fusion is an fuzzing approach for SMT solvers.The key idea of this approach is to fuse two SMT formulas that have the same satisfiability to a new formula while preserving the satisfiability,then use the new formula to test SMT solvers.Based on semantic fusion,we implemented a tool named Yin Yang,it found45 unique bugs in two state-of-the-art SMT solvers.·Type-aware Mutation:Type-aware Mutation is also an fuzzing approach for SMT solvers.The key idea of this approach is to mutate the operator of the SMT formula to another well-typed operator for generating new formula,then use the new formula to test SMT solvers.Based on type-aware mutation,we implemented a tool named Op Fuzz,it found 1092 bugs in two state-of-the-art SMT solvers.The approaches proposed in this thesis not only solved the challenges of testing model verification tools,but also provided new ideas for software testing community.Besides,the testing tools we implemented not only are effective on testing model verification tools,but also can be widely used for other domains and purposes.