A Research On Parallal Model-Checking Based On Pushdown System

The technology of model-checking was proposed on 1980s and experienced a rapid de-velopment since then.Nowadays model-checking is a fundamental technology and is widely used in various field like Aviation field,Space field and Military industry field.The normal test methods can only check a subset of the whole execution paths of a program.Thus they cannot find out all of the bugs,many cases have proved that already.As a comparasion,model?checking technology is able to build the complete state space of the program,and then verify the correctness on a mathematical basis,which is highly reliable.However,the programs have become more and more complex and as a result,the difficulty of conducting model-checking methods has become more and more great as well.The primary problem is state explosion.meaning that the state space of the system grows exponentially with the amount of memory used by it,which limits the practical applicability of model-checking.Fortunatly.with the de-velopment of parallel technology,it is possible to find a good solution by aid of distributed clusters.Reachability analysis is the foundation of the model-clhecking problem,based on reacha-bility analysis,properties represented by logic such as LTL,SCTPL can be checked success-fully.This dissertation proposed a new parallel approach to the reachability analysis of push-down systems based on data parallel.We named the approach SPRADP(SAturation Procedure for Reachability Analysis base on Data Parallelism).Then we proved the correctness and appli-cability of SPRADP.and implemented a set of parallel algorithms to solve LTL model-checking problems.These algorithms can make the best of distributed clusters.One of the typical application of model-checking is malware detection.The process is described as follows:(1)construct a mathematical model from the binary execution code.(2)use time-logic formula(usually LTL or CTL)to describe the malicious behavior.(3)use model-checking to find out whether the model have the properties described by time-logic formula.This dissertation proposed a new method for generating pushdown models from CFGs(Control Flow Graph),which can characterize the behavior of binary code precisely.After then we use LTL formula to describe malicious behavior and finish the work of malware identification with the help of SPRADP.Last but not least,this dissertation implemented a prototype tool for malware detection and model-checking with the combination of the approaches below.We carried out quite a bit of experiments and the results were encouraging.