随着软件的在关键领域如电子商务、银行、航空等的广泛应用,其可信性已经越来越多的获得人们的关注,据报道,2000年到2006年基于WEB的攻击从25%上涨到61%。然而,目前的软件工程方法无法有效的保障软件的可信性,针对软件成品的测试能够一定程度的保证软件的安全性、可靠性,但该过程依赖于测试人员的能力、经验、状态等一系列不确定因素,同时,对于设计阶段引入的缺陷,其缓和成本过高。CWE网站对目前已知的软件安全缺陷进行了总结与整理,然而其描述是基于自然语言的,缺乏足够的语义信息,计算机不能够自动识别并处理。本毕设对软件设计阶段引入的安全缺陷进行了总结、抽象、形式化,并通过Z语言对其进行了形式化的描述,建模了软件安全缺陷发生的本质及可能的缓和方案。基于上述结构,构建了基于本体的软件安全缺陷知识库,作为软件安全专家系统的核心部分,为缺陷的形式化验证、软件的安全性评估及其他相关工具的开发奠定了坚实的基础。最后,通过网上银行案例,验证了上述理论的正确性及有效性,同时,结合统一软件模型,实现了基于定理证明的软件安全性形式化验证。综上所述,本毕设实现了软件可信工程中,设计阶段的软件安全性验证,同时,软件安全缺陷知识库为其他研究组织提供了结构定义完善的软件安全缺陷信息。