题目：软件保密安全性举证方法研究

随着计算机技术和信息化技术的飞速发展，软件已在航空、航天、公共交通、文化娱乐、电子商务等生产、生活领域得到了普及和应用，并在涉及国家安全、民众人身安全、用户财产安全的诸多关键系统中占据了核心地位。为了保证这些软件产品稳定、可靠、安全地正常工作，人们投入大量的人力、物力和财力对软件的可靠性、防危性（safety）等质量属性进行了深入研究并取得了一定的成果。然而，随着互联网应用范围的进一步扩大及物联网时代的到来，软件产品除了要应对自身缺陷所带来的失效风险外，还不得不去面对智能攻击者们的恶意进攻。软件系统的不确定性和不可控性进一步增加，系统也随之更加脆弱，威胁和漏洞所带来的灾难性事故、财产被盗及信息泄露等非预期的不良事件不胜枚举，影响深远。这就是所谓的“软件安全性注1”（security）问题，目前已引起国内外学术界、大型软件开发商及工程领域等多方面的广泛关注。

目前，关于软件安全性的研究风生水起，但大多都集中在对某一个具体的确定漏洞的微观研究上，如何利用宏观的论证技术来对软件的安全属性进行证明，是目前国际研究的一个重要方向。国内外学者围绕软件安全性论证问题，提出了软件安全性生命周期保证模型，遵照模型中规定性的方法可生成相应的证据，用于表征软件能够达到相应的安全性水平。但这种当下流行的主流论证方法还十分松散，论证的系统性、全面性和有序性不足，削弱了论证结果的可信性。近年来，系统防危性研究领域逐步兴起了一种基于目标的举证方法，愈加引人瞩目。该方法以系统要满足的目标为中心，证据为基础、论证为纽带，通过系统化的、明确的论证建立目标与所提供证据之间的联系，来表明软件系统满足了其属性目标的要求。在欧洲，这种基于目标的方法已在军事、石油、铁路、核能、海洋等工业中得到了广泛的应用，但主要还是集中于证明关键系统的防危性。

本文借鉴基于目标的举证思路，以图尔敏模型和贝叶斯网等理论为基础，沿着软件安全性举证开发的过程周期，即“1）项目计划编制→2）项目人员介入→3）安全性举证开发（过程循环）→4）安全性举证评估”，重点对该过程周期中3）、4）阶段的关键技术进行了研究突破，部分研究内容覆盖安全性举证开发过程的第1）阶段，全面实现了软件安全性举证方法研究对“举证”开发周期关键阶段和核心技术要点的全面覆盖。同时，本文通过对主要研究成果的实例化应用，演示验证了本方法的可行性，能够有效地指导软件的安全性论证工作。本文的主要创新研究工作包括：

1．软件安全性概念框架研究

首先探讨了软件安全与计算机安全的关系。针对当前软件安全性定义众多、内容不统一的现状，分析各定义的特征并提出一个综合的软件安全性定义。为进一步把握软件安全性本质，分别从保密性、完整性、可用性、认责性四个角度深入研究了软件安全性的内涵，从理论和实践等方面全面分析了软件安全性与软件防危性、软件可靠性的关系，并按照软件安全性举证开发过程详述了本文研究内容的覆盖范围和彼此关系。

2．本体化论证建模语言研究

为了解决软件安全性举证的语义唯一性问题，实现知识的共享、重用和推理，本文以GSN语言为背景，构建了一套本体化的软件安全性论证建模语言，详细定义了该论证建模语言的概念、概念层次、关联关系和约束集，并明确提出了本体导向的安全性举证的开发构建原语及一般方法步骤。在此基础上，以IM服务器软件为例，对前述的本体研究成果进行了实例化的演示说明。

3．软件安全性论证框架研究

软件安全性论证框架涵盖了软件安全性举证开发的核心技术和方法。首先，本文通过开发核心要素结构模型，研究基于产品和过程的论证原理，为提出的论证框架奠定了理论基础。其次，开展前述理论的应用研究。基于模式思想，利用第2项研究内容中的本体化论证建模语言，构建了软件安全性论证结构的25个主要论证模式，并提出了相应的论证应用方法，从而形成了软件安全性论证的方法体系。第三，以某即时通讯软件（IM）服务器端的软件模块为例，示例验证了本项研究成果的可行性和实施方案。

4．软件安全性举证信心评定方法研究

软件安全性举证信心评定是举证开发周期中，实施迭代分析和过程循环的依据。本项研究内容以图尔敏模型的论证评价标准和贝叶斯网为理论基础，提出了定性评价和定量评价相结合的综合评定方法的一般步骤。在此基础上，利用反驳论证、前提（目标）分类、贝叶斯评价方法改进等技术手段，对现行技术中存在的主要问题进行了重点研究和关键技术突破，并给出了相应的技术解决方案。最后，以“基于CC的系统是安全的”的GSN论证图为例，对本文提出的评定方法进行了示范演示应用和验证。

本文通过研究软件安全性举证开发周期所涉及的主要问题，按照理论研究、方法构建、实例应用的工作思路，提出了一套完备的软件安全性举证方法的技术体系。不仅能够有效指导工程人员完成软件安全性举证的开发，实施软件安全性论证，同时，通过提供关键技术的解决途径，还完成了论证建模语言的形式化，实现了论证建模语言的语义唯一性，形成了论证知识的共享、重用和推理体系，提高了软件安全性举证的开发效率，减少了开发过程中的不确定性，完善了举证评价方法的全面性和合理性。

综上所述，本文提出了一种新的软件安全性论证方法，能够从宏观层面对软件涉及的带有攻击性质的威胁、漏洞和缺陷等固有问题的影响进行整体评判，是对现有微观层面的漏洞分析等技术的有效补充。