基于Z規(guī)格的軟件缺陷形式化方法.pdf

1、基于Z規(guī)格的軟件缺陷形式化方法FormalizingSoftwareWeaknessesBasedOnZSpecification學(xué)科專業(yè)：計(jì)算機(jī)應(yīng)用技術(shù)研究生：HamzaIBangura指導(dǎo)教師：李曉紅教授f▲I■摘要隨著軟件的在關(guān)鍵領(lǐng)域如電子商務(wù)、銀行、航空等的廣泛應(yīng)用，其可信性已經(jīng)越來越多的獲得人們的關(guān)注，據(jù)報(bào)道，2000年至U2006年基于WEB的攻擊從25％上漲到61％。然而，目前的軟件工程方法無法有效的保障軟件的可信性，針對

2、軟件成品的測試能夠一定程度的保證軟件的安全性、可靠性，但該過程依賴于測試人員的能力、經(jīng)驗(yàn)、狀態(tài)等一系列不確定因素，同時(shí)，對于設(shè)計(jì)階段引入的缺陷，其緩和成本過高。CWE網(wǎng)站對目前已知的軟件安全缺陷進(jìn)行了總結(jié)與整理，然而其描述是基于自然語言的，缺乏足夠的語義信息，計(jì)算機(jī)不能夠自動(dòng)識別并處理。本畢設(shè)對軟件設(shè)計(jì)階段引入的安全缺陷進(jìn)行了總結(jié)、抽象、形式化，并通過Z語言對其進(jìn)行了形式化的描述，建模了軟件安全缺陷發(fā)生的本質(zhì)及可能的緩和方案?；谏鲜鼋Y(jié)

3、構(gòu)，構(gòu)建了基于本體的軟件安全缺陷知識庫，作為軟件安全專家系統(tǒng)的核心部分，為缺陷的形式化驗(yàn)證、軟件的安全性評估及其他相關(guān)工具的開發(fā)奠定了堅(jiān)實(shí)的基礎(chǔ)。最后，通過網(wǎng)上銀行案例，驗(yàn)證了上述理論的正確性及有效性，同時(shí)，結(jié)合統(tǒng)一軟件模型，實(shí)現(xiàn)了基于定理證明的軟件安全性形式化驗(yàn)證。綜上所述，本畢設(shè)實(shí)現(xiàn)了軟件可信工程中，設(shè)計(jì)階段的軟件安全性驗(yàn)證，同時(shí)，軟件安全缺陷知識庫為其他研究組織提供了結(jié)構(gòu)定義完善的軟件安全缺陷信息。關(guān)鍵字：軟件安全缺陷；z規(guī)格；知