使软件更安全、更可靠：深入探讨证明分数

在软件工程领域之中呢，至关重要的是，要确保系统行为的正确性与可靠性。尤其是对于像在线银行、电子商务以及实时系统这类关键系统而言，这一要求，格外突出。有一种颇具前途的、用于验证这些系统属性的技术，也就是所谓的证明评分，它采用了一种名为术语重写的方法。证明评分，由声明以及重写所构成，要是所有组件都能按照预期进行评估的话，那么问题就能够得到解决。这种方法呀，在自动化和人工努力之间达成了一种平衡：机器负责处理像替换、简化以及归约这类常规任务，而人类呢，则着重专注于最为有趣的任务，例如决定证明策略。此外呢，即便只是部分完成的证明，也能够提供有价值的反馈，通常会指示下一步该尝试些什么。

该技术已经通过代数规格化语言得到了实现，特别是OBJ家族，如OBJ3、CafeOBJ和Maude，这些语言被设计为可以通过术语重写来执行。证明分数的一个关键优势是，它们使用与用于规格化系统的语言相同的语法和评估机制，这使得验证过程顺畅且紧密集成。

该技术已广泛应用于多种系统和协议之中。尽管如此，它亦存在不足，主要限于学术领域。为了探究这一现状，日本先进科学技术研究院（JAIST）的Kazuhiro Ogata教授与Duong Dinh Tran助理教授带领的研究团队对证明分数的历史、现状与未来进行了深入研究。奥谷达教授与陈助理教授指出：“证明分数已被证实能够验证系统是否符合其设计，包括我们日常所依赖的系统。”他们的研究成果发表在《ACM计算综述》期刊上。

证明分数最初由Joseph A. Goguen在1990年代提出，并已在多个OBJ语言中实现。研究团队探讨了其理论基础，并分析了在OBJ语言中的具体应用。

研究团队还考察了证明分数在多个领域的成功应用案例，如通信、认证和电子商务协议、实时系统、现代加密协议以及后量子加密协议，后者旨在抵御未来强大量子计算机的威胁。分析揭示了证明分数的优势，其中最显著的是，用于指定系统的语法也可用于证明其属性。与传统高度抽象的定理证明方法不同，证明分数的这一特性确保了每一步证明都基于系统的正式定义，从而提高了证明的透明度和易理解性。此外，证明分数作为程序编写，与程序一样灵活。

然而，研究也揭示了证明分数的主要弱点：它们由人类编程，必须确保所有可能的情况都被考虑，因此容易产生人为错误。过去的实现方式并未提醒用户是否遗漏了某种情况，这对于大型证明尤为成问题。这是证明分数未能更广泛采用的主要原因之一。尽管已开发出证明辅助工具来克服这一缺点，但它们通常会削弱证明分数的优势。不过，CiMPG这一证明辅助工具，专为CafeOBJ设计，可能是一个例外。该研究在保留证明分数优势的同时，也进行了设计。研究团队还指出了若干尚未解决的问题，如需开发更易于人类理解的证明，以便不仅研究人员能够使用，而且公共图书馆也能应用。为解决这些开放性问题，研究人员提议现代系统应提供类似流行编程语言的集成开发环境，以提供图形化、交互式的支持来编写和管理证明分数。他们还建议研究Maude的最新功能。研究人员强调：“证明分数对于新兴的安全关键系统至关重要，这些系统将塑造我们的未来社会。”他们补充说：“从网上银行和电子商务的通信协议，到区块链和后量子密码学，证明分数在构建可靠系统方面的潜力是巨大的。”
总体来看，这项研究不仅凸显了证明分数的重要性，还为其更广泛的实践性和普及性指明了路径。