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

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

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