本文選題：下推系統(tǒng)　切入點(diǎn)：可達(dá)性檢測(cè)　出處：《華東師范大學(xué)》2017年碩士論文　論文類型：學(xué)位論文

【摘要】：模型檢測(cè)技術(shù)自上世紀(jì)80年代被提出后,得到了迅速的發(fā)展,目前已經(jīng)成為一種不可或缺的驗(yàn)證技術(shù),在航空、航天和軍工等諸多領(lǐng)域得到了廣泛的應(yīng)用。傳統(tǒng)的測(cè)試方法只能驗(yàn)證程序中的某些而不是全部的執(zhí)行路徑,因此無(wú)法檢測(cè)出所有的Bug,很多現(xiàn)實(shí)中的例子也證明了這一點(diǎn)。而模型檢測(cè)方法可以構(gòu)建出完整的系統(tǒng)運(yùn)行狀態(tài)空間(State Space),從而對(duì)程序進(jìn)行全方位的驗(yàn)證,是一種十分可靠的方式。但是隨著計(jì)算機(jī)軟件系統(tǒng)變得日益復(fù)雜,對(duì)其進(jìn)行模型檢測(cè)也變得越來(lái)越困難,其中主要原因便是狀態(tài)爆炸(State Explosion)問(wèn)題。狀態(tài)爆炸指的是為了刻畫(huà)一個(gè)復(fù)雜系統(tǒng)的行為,需要生成海量的狀態(tài),由于狀態(tài)的數(shù)量過(guò)于龐大使得模型檢測(cè)效率降低,變得難以實(shí)現(xiàn)。隨著并行計(jì)算技術(shù)的發(fā)展,大數(shù)據(jù)處理集群已經(jīng)變得十分常見(jiàn),這使得人們有條件利用分布式集群的運(yùn)算能力和存儲(chǔ)能力來(lái)應(yīng)對(duì)這一問(wèn)題。在模型檢測(cè)問(wèn)題中,可達(dá)性分析是最基礎(chǔ)也是最重要的問(wèn)題,解決了可達(dá)性分析問(wèn)題,就可以進(jìn)一步的解決諸如LTL,CTL等復(fù)雜的時(shí)態(tài)邏輯檢測(cè)問(wèn)題。本文基于數(shù)據(jù)分布的思想和飽和式可達(dá)性分析方法,提出了一種新型的基于下推系統(tǒng)的并行可達(dá)性分析方法 SPRADP(SAturation Procedure for Reachability Analysis base on Data Parallelism)、本文論證了 SPRADP方法的可行性和正確性,并將此方法運(yùn)用到線性時(shí)態(tài)邏輯檢測(cè)中實(shí)現(xiàn)了并行模型檢測(cè)方法。該方法能充分利用分布式集群的性能來(lái)解決大規(guī)模模型檢測(cè)問(wèn)題。在SPRADP方法的指導(dǎo)下,本文實(shí)現(xiàn)了一套基于分布式集群的并行模型檢測(cè)工具,并圍繞該工具進(jìn)行了一系列的可達(dá)性檢測(cè)和時(shí)態(tài)邏輯檢測(cè)實(shí)驗(yàn),結(jié)果表明,SPRADP方法能很好的利用分布式集群的計(jì)算能力,進(jìn)行正確且高效的模型檢測(cè)工作。模型檢測(cè)除了能對(duì)系統(tǒng)進(jìn)行驗(yàn)證之外,還能用于惡意代碼識(shí)別。本文基于控制流圖(CFG),提出一種從二進(jìn)制代碼中生成下推模型的方法,該方法能夠?qū)ΧM(jìn)制代碼的行為進(jìn)行精確及完整的刻畫(huà)。隨后,利用時(shí)態(tài)邏輯公式來(lái)描述惡意行為,結(jié)合上文提出的SPRADP并行方法完成了對(duì)惡意代碼的識(shí)別工作。根據(jù)上述過(guò)程,本文初步實(shí)現(xiàn)了二進(jìn)制代碼惡意性檢測(cè)過(guò)程,并進(jìn)行了一系列的實(shí)驗(yàn),取得了較好的效果。
[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.
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP311.53

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 吳丹飛;王春剛;郝興偉;;惡意代碼的變形技術(shù)研究[J];計(jì)算機(jī)應(yīng)用與軟件;2012年03期

相關(guān)博士學(xué)位論文 前1條

1 張一弛;程序惡意行為識(shí)別及其惡意性判定研究[D];解放軍信息工程大學(xué);2012年

，

本文編號(hào)：1556839