基于模型檢測(cè)的軟件安全分析研究.pdf

1、目前計(jì)算機(jī)系統(tǒng)和網(wǎng)絡(luò)的安全性越來越受到軟件質(zhì)量和安全性的影響，并且軟件安全性問題有越來越嚴(yán)重的趨勢(shì)。軟件安全的研究在世界范圍逐漸受到重視，但目前并沒有較成熟和實(shí)用的方法。模型檢測(cè)是一種形式化驗(yàn)證技術(shù)，該技術(shù)在時(shí)序電路設(shè)計(jì)和通信協(xié)議設(shè)計(jì)的驗(yàn)證領(lǐng)域得到了廣泛應(yīng)用。但將模型檢測(cè)技術(shù)應(yīng)用于軟件的驗(yàn)證和安全性分析正處于研究階段。模型檢測(cè)技術(shù)能夠高效、自動(dòng)化并且完全地對(duì)軟件進(jìn)行安全性分析，模型檢測(cè)技術(shù)在軟件的安全性分析方面有著良好的發(fā)展前景。本文分

2、析了軟件安全問題越來越嚴(yán)重的原因以及軟件漏洞與軟件安全性之間的聯(lián)系。軟件發(fā)展的互連性、可擴(kuò)展性和復(fù)雜性趨勢(shì)對(duì)軟件安全問題產(chǎn)生了重大影響。而隨著軟件漏洞的增加，軟件的安全性問題也必將增加。 本文介紹了模型檢測(cè)的基本概念、發(fā)展情況。針對(duì)模型檢測(cè)的流程，介紹了模型檢測(cè)過程中三個(gè)重要的步驟——系統(tǒng)建模、屬性建模和模型檢測(cè)算法——中所應(yīng)用的技術(shù)。針對(duì)軟件模型檢測(cè)的特點(diǎn)，介紹了一些解決狀態(tài)空間爆炸問題的技術(shù)和方法。分析了MOPS的形式化方法