基于UML行為模型的軟件漏洞檢測(cè)形式方法研究.pdf

1、隨著計(jì)算機(jī)應(yīng)用的不斷發(fā)展,人們對(duì)軟件的高可靠性要求越來(lái)越高。形式化方法是基于數(shù)學(xué)和邏輯語(yǔ)言的精確性規(guī)格、驗(yàn)證,保證軟件高可靠性的重要方法。模型檢測(cè)是一種形式化的驗(yàn)證技術(shù),對(duì)該理論的研究和應(yīng)用成為國(guó)內(nèi)外近幾年的熱點(diǎn)問(wèn)題。在計(jì)算機(jī)硬件、安全協(xié)議驗(yàn)證等領(lǐng)域,模型檢測(cè)技術(shù)已經(jīng)取得了豐碩的成果。
　　 為了實(shí)現(xiàn)軟件的高可靠性,首先要對(duì)影響軟件可靠性的軟件漏洞進(jìn)行學(xué)習(xí)和研究。論文不僅介紹了軟件漏洞的分類而且對(duì)幾種具體的漏洞進(jìn)行了分析和定義。

2、時(shí)序邏輯語(yǔ)言是模型檢測(cè)的基礎(chǔ),為了掌握模型檢測(cè)技術(shù),對(duì)線性時(shí)序邏輯語(yǔ)言LTL進(jìn)行了詳細(xì)的描述,使用LTL對(duì)分析得到的漏洞定義進(jìn)行了描述,從而得到了LTL公式。并且詳細(xì)地介紹了模型檢測(cè)工具SPIN。通過(guò)對(duì)SET購(gòu)買過(guò)程協(xié)議使用SPIN進(jìn)行驗(yàn)證,更深入的了解了該模型檢測(cè)工具的建模語(yǔ)言promela以及屬性定義語(yǔ)言LTL。
　　 模型檢測(cè)技術(shù)應(yīng)用在軟件漏洞檢測(cè)領(lǐng)域主要包括對(duì)需求分析和設(shè)計(jì)階段的軟件模型進(jìn)行模型檢測(cè)和對(duì)目標(biāo)代碼的模型檢測(cè)

3、。本課題選擇了對(duì)軟件開發(fā)初期階段的設(shè)計(jì)模型進(jìn)行形式化驗(yàn)證,可以及早的規(guī)避軟件邏輯漏洞和安全漏洞,大大減少軟件開發(fā)成本,縮短軟件開發(fā)周期。并且對(duì)軟件設(shè)計(jì)模型的形式化驗(yàn)證基于UML行為模型。UML建模是目前軟件開發(fā)中最主要的可視化建模方法,而模型檢測(cè)等形式化方法在建模過(guò)程中存在可視化困難,因此,將兩種方法結(jié)合進(jìn)行軟件漏洞的檢測(cè),可以有效地減少形式化建模方面的難題。
　　 本課題主要研究在軟件開發(fā)初期,對(duì)UML行為模型進(jìn)行模型檢測(cè)。首