Key Research On Symbolic Verification

As the size and complexity of software increase,more and more software vulnerabilities are reported.How to improve the reliability of software has become a significant research question in software engineering.Program verification is widely used for improving the reliability of software,and existing work can be divided into two catergories:static verification and dynamic verification.Static verification soundly abstracts the program for verification,which usually achieves high code coverage,but suffers from false alarms,manual effort or poor scalability.Dynamic verification runs the program and performs analysis based on the runtime information.Hence,dynamic verification can ensure the completeness of analysis,but may miss input-related program errors.Symbolic execution based verification achieves a tradeoff between static and dynamic verification.Compared with static verification and dynamic verification,symbolic execution based verification can achieve better precision and coverage,respectively.However,considering the number of program paths increases exponentially w.r.t.the number of branches,path explosion problem has become the bottleneck of symbolic execution.The problem becomes even more severe when analyzing parallel programs,because of parallel execution.How to improve the scalability of symbolic execution based verification is a challenging problem.This thesis makes the following three main contributions:1.In software engineering,regular properties are widely used for property specification.We propose a symbolic execution based verification framework,called SRV,for verifying regular properties.SRV integrates regular property oriented path slicing with regular property guided dynamic symbolic execution.Specifically,we propose a regular property oriented path slicing method to prune redundant paths,and use regular property guided dynamic symbolic execution to find counterexample paths as soon as possible.We have implemented SRV and applied it to verify real world Java programs(totally 259 K lines of code)w.r.t.regular properties.Compared with dynamic symbolic execution(DSE),regular property guided DSE,and DSE with path slicing,SRV achieves average speedups of more than 8.4X,8.6X,and 7X,respectively.2.Message Passing Interface(MPI)is the standard paradigm of programming in high performance computing.MPI programs are error-prone because of complex program features,such as non-determinism and asynchrony.We propose MPI symbolic verifier(MPI-SV)for automatically verifying MPI programs that communications do not depend on the message contents.MPI-SV supports both non-blocking and non-deterministic communication operations.MPI-SV integrates symbolic execution with model checking: symbolic execution automatically extracts path-level models for model checking,and model checking can prune redundant paths of symbolic execution and enlarge the scope of verifiable properties of symbolic execution.We have implemented MPI-SV and applied it to verify 12 real-world MPI programs,totaling 47 K lines of code,w.r.t.the deadlock freedom property and temporal safety properties.The results demonstrate the effectiveness of MPI-SV:(1)for all the 102 deadlock freedom verification tasks,MPI-SV can complete 90 tasks within one hour,while pure symbolic execution can complete 52 tasks;(2)compared with pure symbolic execution,MPI-SV achieves,on average,7.6X speedup on verifying deadlock freedom and 4.96 X speedup on finding a deadlock;(3)MPI-SV can detect counterexamples when verifying temporal safety properties,while pure symbolic execution fails.3.To improve MPI program's performance,Master-Slave pattern has been widely used to achieve load balancing among parallel processes.Due to the high nondeterminism,dynamic scheduling MPI programs are error-prone.We propose a symbolic verification technique for programs using Master-Slave pattern.More precisely,we enhance MPI-SV to support Master-Slave pattern:(1)recognize MasterSlave pattern automatically during symbolic execution;(2)use path-level models to simulate the dynamic scheduling features,i.e.,a path-level model can represent all the possible schedules under the same input.We have implemented our technique in a prototype,and evaluated it on verifying real-world MPI programs(totaling 13.9K lines of code)using Master-Slave pattern w.r.t.deadlock freedom.The results show that our method achieves an average 21.24 X speedup over symbolic execution.