浙江天搜科技股份有限公司软件可信研究现状小结
在如何保证软件的可信性方面，形式化理论和软件验证技术获得了持续关注。例如，图灵奖得主霍尔提议将验证过的软件(Verified Software)作为计算机科学中的一个重大挑战性问题，希望能像人类基因组计划那样，通过国际合作取得重大进展。国际著名刊物(理论计算科学)的两辑之一就是关于程序设计理论的讨论，特别是形式语义、形式验证。图灵奖得主迪杰斯特拉、霍尔、米尔纳、伯努利等人都在程序设计领域采用各种形式化方法提高了程序的可靠性和安全性。例如，霍尔的顺序程序的公理化理论通过前后置断言，给出了顺序程序的部分正确性和完全正确性的形式推理系统。程序分析和验证技术在近几年取得了一些突破。
目前的可信软件研究是从软件正确性、可靠性、安全性、生存性等基础上发展起来的，软件形式化理论和验证技术、可靠性工程、网络信息安全等领域均有针对若干可信属性的研究。但是软件可信性不是正确性、可靠性、安全性和生存性等性质的简单相加。相应地，可信软件研究也不是对已有的各种软件属性研究进行简单的综合。首先，由于软件系统越来越复杂，软件可信意味着软件行为可信、环境可信性和使用可信等不同层次的可信要求，而局部的可信并不一定会导致全局的可信。系统的可信属于涌现类的性质，如何从整体上度量、获得并保证可信性将是非常困难的。其次，不同可信属性之间可能彼此冲突，并且不同层次之间也可能会冲突，如何最优化地协调与取舍也是一个关键问题。最后，当软件可信性成为研究目标之后，必然要针对“可信”性质建立分析、构造、度量、评价体系，使得可信性能够在软件生产活动中被有效地跟踪控制和验证实现，这也对现有的计算理论与技术体系提出了挑战。需要强调的是，要达到软件可信的目标，需要对软件系统开发的整个生命周期(需求分析、可信算法设计、软件设计与实现、测试与验证、运行维护等)的各个阶段进行全面而统一的研究。用户对软件可信性的认可还有一个积累和沉淀的过程，在软件运行过程中，软件可演化特征也是现有静态分析、测试技术无法应对的。
从研究方法上来看，已有的经验表明，若软件开发过程中过于依赖开发人员的知识和经验，则会有许多不规范之处;而软件动态行为的论述又难于验证。这就促使了许多软件工程研究人员开展实证软件工程(Empirical Software Engineering)研究，该研究旨在以数据和证据来验证关于软件的论断，但目前实证软件工程研究存在两方面的问题。①在案例研究和数据收集过程中仍然依赖于人的参与，软件开发过程和软件系统的动态行为往往不具有可重复性;②研究目标局限于技术层次，旨在验证某种技术的有效性，而忽视了软件开发过程和软件系统动态行为可能存在某种不以人的意志为转移的客观规律。
可信软件离不开可信环境。可信计算的基本思想是:首先构建一个信任根，再建立一条信任链，从信任根开始到硬件平台、到操作系统、再到应用，通过一级认证一级，一级信任一级，从而把这种信任扩展到整个计算系统，确保整个计算系统的可信。
