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

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

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

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