基于下推系统的并行模型检测技术研究

发布时间：2018-03-02 14:08

本文选题：下推系统　切入点：可达性检测　出处：《华东师范大学》2017年硕士论文　论文类型：学位论文

【摘要】：模型检测技术自上世纪80年代被提出后,得到了迅速的发展,目前已经成为一种不可或缺的验证技术,在航空、航天和军工等诸多领域得到了广泛的应用。传统的测试方法只能验证程序中的某些而不是全部的执行路径,因此无法检测出所有的Bug,很多现实中的例子也证明了这一点。而模型检测方法可以构建出完整的系统运行状态空间(State Space),从而对程序进行全方位的验证,是一种十分可靠的方式。但是随着计算机软件系统变得日益复杂,对其进行模型检测也变得越来越困难,其中主要原因便是状态爆炸(State Explosion)问题。状态爆炸指的是为了刻画一个复杂系统的行为,需要生成海量的状态,由于状态的数量过于庞大使得模型检测效率降低,变得难以实现。随着并行计算技术的发展,大数据处理集群已经变得十分常见,这使得人们有条件利用分布式集群的运算能力和存储能力来应对这一问题。在模型检测问题中,可达性分析是最基础也是最重要的问题,解决了可达性分析问题,就可以进一步的解决诸如LTL,CTL等复杂的时态逻辑检测问题。本文基于数据分布的思想和饱和式可达性分析方法,提出了一种新型的基于下推系统的并行可达性分析方法 SPRADP(SAturation Procedure for Reachability Analysis base on Data Parallelism)、本文论证了 SPRADP方法的可行性和正确性,并将此方法运用到线性时态逻辑检测中实现了并行模型检测方法。该方法能充分利用分布式集群的性能来解决大规模模型检测问题。在SPRADP方法的指导下,本文实现了一套基于分布式集群的并行模型检测工具,并围绕该工具进行了一系列的可达性检测和时态逻辑检测实验,结果表明,SPRADP方法能很好的利用分布式集群的计算能力,进行正确且高效的模型检测工作。模型检测除了能对系统进行验证之外,还能用于恶意代码识别。本文基于控制流图(CFG),提出一种从二进制代码中生成下推模型的方法,该方法能够对二进制代码的行为进行精确及完整的刻画。随后,利用时态逻辑公式来描述恶意行为,结合上文提出的SPRADP并行方法完成了对恶意代码的识别工作。根据上述过程,本文初步实现了二进制代码恶意性检测过程,并进行了一系列的实验,取得了较好的效果。
[Abstract]:Model detection technology has been developed rapidly since it was proposed in -20s. It has become an indispensable verification technology in aviation. Many fields such as aerospace and military industry have been widely used. Traditional testing methods can only verify some, not all, of the execution paths in the program. So it's impossible to detect all of the Bugs, as many real-world examples have shown, and the model checking method can build a complete system running state space, so that the program can be fully validated. Is a very reliable way. But as computer software systems become more and more complex, it becomes more and more difficult to do model checking. The main reason is the state explosion problem. State explosion is to describe the behavior of a complex system, it needs to generate a large number of states, because the number of states is too large to reduce the efficiency of model detection. With the development of parallel computing technology, it has become very common for big data to deal with clusters, which makes it possible for people to take advantage of the computing and storage capabilities of distributed clusters to deal with this problem. Reachability analysis is the most basic and important problem. If we solve the reachability analysis problem, we can further solve the complex temporal logic detection problem such as LTL CTL. This paper based on the idea of data distribution and saturated reachability analysis method, In this paper, a new parallel reachability analysis method, SPRADP(SAturation Procedure for Reachability Analysis base on Data parallel is presented, and the feasibility and correctness of SPRADP method are proved. This method is applied to linear temporal logic detection to realize parallel model detection. This method can make full use of the performance of distributed cluster to solve the problem of large-scale model detection. Under the guidance of SPRADP method, A set of parallel model checking tools based on distributed cluster is implemented in this paper, and a series of experiments on reachability detection and temporal logic detection are carried out around the tool. The results show that the SPRADP method can make good use of the computing power of distributed cluster. Model checking can be used for malicious code recognition besides verifying the system. This paper presents a method to generate a push-down model from binary code based on the control flow diagram (CFG). This method can describe the behavior of binary code accurately and completely. Then, using temporal logic formula to describe malicious behavior, combining with the SPRADP parallel method proposed above, the identification of malicious code is completed. In this paper, the malicious detection process of binary code is preliminarily realized, and a series of experiments are carried out, and good results are obtained.
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.53

【参考文献】