软件验证有助于发现漏洞、防止黑客攻击。

在华盛顿大学的医学中心内，放射治疗系统将高能辐射光束射入到病人头中，以治疗患者舌头和食道内的肿瘤。系统中的任何软件都不允许出现错误，任何错误都将是致命的，因此，医学中心的工程师和科学家们进行合作，以确保系统不会失效。一旦规定的配置超出允许范围，高能辐射光束将被立即关闭。

这是通过一种被称为软件验证(software verification)的方法实现的。验证关键系统，例如放射治疗装置，正是扎卡里·塔特洛克(Zachary Tatlock)热衷的事情。三年前，塔特洛克作为一名博士生在华盛顿大学对他毕业论文课题中关于程序验证的研究作了报告。医学中心放射治疗团队的首席工程师在听众席中询问，如何将验证方法应用到他们的系统中。塔特洛克回想这件事时说到：“这可能帮助我找到了一份工作。”如今，他已成为华盛顿大学计算机科学领域的一名助理教授。他一直与华盛顿大学的其他同事及学生一起，与医学中心的团队开展合作。

软件验证在上述放射治疗系统上应用的挑战在于，该系统由多种语言开发，因此须采用不同的技术来完整地验证软件。整个系统由十多个组件构成，每个组件又有不同的关键等级。

塔特洛克解释说，事件日志软件的关键等级要比辐射功率控制软件的低得多。他认为，“我们希望确保所有模块的可靠性，并确保不存在影响关键部件的软件缺陷。其中有两三个组件是系统的核心，保证它们的正确性显得尤为重要”。

放射治疗系统团队使用了多种验证方法，包括从自动定理证明工具到手工编写，再到经证明辅助工具检查的手工证明等各种有力的验证方法。其中，证明辅助工具是一种检查证明正确性的程序，证明来自某种表达力丰富的逻辑。

防止软件攻击

通常计算机代码的开发不经过任何形式化过程，并且测试代码的主要指标是简单地运行程序，看其是否工作。这种测试，既不能保证覆盖到运行时发生的所有情况，也不能够防止恶意攻击者通过研读程序，设计巧妙的方法对软件进行破坏。形式化软件验证(formal software verification)依赖数学定理和推理，并且使用演绎方法检查系统最关键的部分。支持者相信使用这种技术，可以开发出防止黑客攻击的软件。

“攻击者控制机器和互联网上程序的很多方法是利用安全漏洞，而安全语言对于其中很多类型的漏洞是免疫的，如缓冲区溢出漏洞。”普林斯顿大学计算机科学教授、程序验证领域的专家安德鲁·阿佩尔(Andrew Appel)解释道。

形式化软件验证采用的方法不依赖于程序的运行。它通过分析程序文本来证明在任何可能的输入的情况下程序行为的性质。阿佩尔说，“即使使用所谓的‘安全’语言（如Java）编写程序也不一定保证它们就是正确的。它们仍然可能有漏洞并且出错，只是没有什么灾难性的后果。”他强调，安全始终是重要的，但对于系统的关键基础组件，正确性变得至关重要。

此前，安全性已被证明是关键系统的重要问题，并已在多个案例中危及患者的生命。1982年，加拿大原子能有限公司(AECL)生产了Therac-25型放射治疗机。1985~1987年间发生的至少6起事故都与该系统有关。在这些事故中，患者遭受了过量的辐射——有时候比正常值高出数百倍，从而导致患者死亡或者遭受严重伤害。

Therac-25事故的调查结果显示，AECL公司既没有独立审查软件代码，也没有在医院组装系统之前测试系统的软硬件。

“如果要确保程序的正确性，而不仅仅是安全，就需要证明程序是根据某种规约执行的。”阿佩尔说，“必须根据程序输入/输出的相关性，使用形式化方法定义程序的正确性，即规约，然后必须找到一种方法来保证对于任何可能的输入，程序的输出都满足该规约。”

阿佩尔是DeepSpec¹研究项目的成员。他在该项目中的职责是检查软件应用程序和硬件的完全功能正确性(full functional correctness)，使程序按照预定的方式运行。为了达到该目的，DeepSpec项目正在构建一系列工具，用于验证程序是否符合深度规约（基于形式逻辑和数学给出的细粒度、精确的软件行为的描述），同时验证软件组件（例如操作系统内核）是否符合其深度规约。

软件验证有助于发现漏洞、防止黑客攻击。

在华盛顿大学的医学中心内，放射治疗系统将高能辐射光束射入到病人头中，以治疗患者舌头和食道内的肿瘤。系统中的任何软件都不允许出现错误，任何错误都将是致命的，因此，医学中心的工程师和科学家们进行合作，以确保系统不会失效。一旦规定的配置超出允许范围，高能辐射光束将被立即关闭。

这是通过一种被称为软件验证(software verification)的方法实现的。验证关键系统，例如放射治疗装置，正是扎卡里·塔特洛克(Zachary Tatlock)热衷的事情。三年前，塔特洛克作为一名博士生在华盛顿大学对他毕业论文课题中关于程序验证的研究作了报告。医学中心放射治疗团队的首席工程师在听众席中询问，如何将验证方法应用到他们的系统中。塔特洛克回想这件事时说到：“这可能帮助我找到了一份工作。”如今，他已成为华盛顿大学计算机科学领域的一名助理教授。他一直与华盛顿大学的其他同事及学生一起，与医学中心的团队开展合作。

软件验证在上述放射治疗系统上应用的挑战在于，该系统由多种语言开发，因此须采用不同的技术来完整地验证软件。整个系统由十多个组件构成，每个组件又有不同的关键等级。

塔特洛克解释说，事件日志软件的关键等级要比辐射功率控制软件的低得多。他认为，“我们希望确保所有模块的可靠性，并确保不存在影响关键部件的软件缺陷。其中有两三个组件是系统的核心，保证它们的正确性显得尤为重要”。

放射治疗系统团队使用了多种验证方法，包括从自动定理证明工具到手工编写，再到经证明辅助工具检查的手工证明等各种有力的验证方法。其中，证明辅助工具是一种检查证明正确性的程序，证明来自某种表达力丰富的逻辑。

防止软件攻击

通常计算机代码的开发不经过任何形式化过程，并且测试代码的主要指标是简单地运行程序，看其是否工作。这种测试，既不能保证覆盖到运行时发生的所有情况，也不能够防止恶意攻击者通过研读程序，设计巧妙的方法对软件进行破坏。形式化软件验证(formal software verification)依赖数学定理和推理，并且使用演绎方法检查系统最关键的部分。支持者相信使用这种技术，可以开发出防止黑客攻击的软件。

“攻击者控制机器和互联网上程序的很多方法是利用安全漏洞，而安全语言对于其中很多类型的漏洞是免疫的，如缓冲区溢出漏洞。”普林斯顿大学计算机科学教授、程序验证领域的专家安德鲁·阿佩尔(Andrew Appel)解释道。

形式化软件验证采用的方法不依赖于程序的运行。它通过分析程序文本来证明在任何可能的输入的情况下程序行为的性质。阿佩尔说，“即使使用所谓的‘安全’语言（如Java）编写程序也不一定保证它们就是正确的。它们仍然可能有漏洞并且出错，只是没有什么灾难性的后果。”他强调，安全始终是重要的，但对于系统的关键基础组件，正确性变得至关重要。

此前，安全性已被证明是关键系统的重要问题，并已在多个案例中危及患者的生命。1982年，加拿大原子能有限公司(AECL)生产了Therac-25型放射治疗机。1985~1987年间发生的至少6起事故都与该系统有关。在这些事故中，患者遭受了过量的辐射——有时候比正常值高出数百倍，从而导致患者死亡或者遭受严重伤害。

Therac-25事故的调查结果显示，AECL公司既没有独立审查软件代码，也没有在医院组装系统之前测试系统的软硬件。

“如果要确保程序的正确性，而不仅仅是安全，就需要证明程序是根据某种规约执行的。”阿佩尔说，“必须根据程序输入/输出的相关性，使用形式化方法定义程序的正确性，即规约，然后必须找到一种方法来保证对于任何可能的输入，程序的输出都满足该规约。”

阿佩尔是DeepSpec¹研究项目的成员。他在该项目中的职责是检查软件应用程序和硬件的完全功能正确性(full functional correctness)，使程序按照预定的方式运行。为了达到该目的，DeepSpec项目正在构建一系列工具，用于验证程序是否符合深度规约（基于形式逻辑和数学给出的细粒度、精确的软件行为的描述），同时验证软件组件（例如操作系统内核）是否符合其深度规约。

DeepSpec项目组的另一位成员是耶鲁大学计算机科学教授邵中。他与其团队一起开发了CertiKOS操作系统。他们使用形式化软件验证来确保代码的行为与预期完全一致。 “如果代码与规约不匹配，则存在缺陷或漏洞。”邵中解释说，“而经过验证的操作系统可保证没有这种漏洞，在所有情况下，代码的运行与其规约完全一致。”这样可以保证操作系统无法被黑客利用。

邵中说，除了验证以外，CertiKOS与其他操作系统的区别在于，它包括一个可扩展的操作系统内核，意味着它可以方便地进行定制，可以扩展更多的功能，以适应许多不同的场景。CertiKOS支持多CPU核上的多线程执行，即所谓的并发性。

普渡大学计算机科学教授苏雷什·贾甘纳森(Suresh Jagannathan)注意到，CertiKOS和其他类似的系统面临的主要问题与“语义工程”有关，即通过定义规约和证明方法使得重新验证的成本最小化。

他说：“我认为这不是这些系统和形式验证的限制。随着使用各种验证和证明辅助工具的经验越来越丰富，并且使用这些工具来验证真实系统的成功案例越来越多，形式化验证会变得更为重要。”贾甘纳坦补充道，关键是确定采用何种过程和方法，使得在规约和实现演变时证明系统更具鲁棒性。

DeepSpec和其他原理

塔特洛克说，华盛顿大学研究团队使用DeepSpec原理来检查放射治疗系统中担负重要任务的组件，并为系统中的次关键组件进行评估，用轻量级技术来确保正确性。这样做，对这些组件的保证虽然不是很强，但在工程上，这是更好的一种折中方式。这是因为DeepSpec原理通常要求训练有素的人去证明功能的正确性，这种方式通常要付出更多的努力，但也得到了更强大的保证。

这里提出了一个问题：如果DeepSpec技术可以绝对地、万无一失地保证软件的验证，那么，为什么我们不一直使用该技术来避免所有系统中的崩溃和错误呢？塔特洛克说，之所以不都用，原因是成本太高。华盛顿大学医学中心放射治疗团队只将DeepSpec技术用于最关键组件的验证系统也是因为此。因为，使用DeepSpec技术，需要一个专家坐在计算机前，手工编写出证明，这样计算机才能对系统的每一个版本的证明进行检查。

这是耗时且低效的。塔特洛克说：“理想情况下，如果你证明了一个版本并做了一点小的改动，那么你只需对证明做一点小的改动，但这不是软件验证的工作方式。”他补充道，每当软件代码发生小的变化时，“可能会产生很大的影响”，导致需要对证明做很大的改动。这可能导致其他所有证明所依赖的事实被改变。

塔特洛克说，其他技术不那么强大，例如有界模型检测(bounded model checking)。它是一种穷举测试形式。这种方法考虑某个组件，并保证在有界步骤内每种可能的执行路径都是正确的。“所以，我可以确保日志系统在100个执行步骤内不会崩溃。我通过自动测试每一个执行路径直到第100步，就可以得到该结果。”然而，塔特洛克重申，这种方式的保证不强，检查100步的有界模型检测不会给出第101步的结果。

塔特洛克和他的同事已经建立了一套工具，可以融入常规的软件开发过程中。该工具包括一个检查器，它能够让研究人员将整个放射治疗系统形式化地描述出来，并确保每个关键组件的正确性。研究人员正在针对上述组件开发一种经过验证的替代品。塔特洛克说，当所有这些单独的系统组件放在一起时，本质上能确保它们能通过顶层安全验证。

放射治疗系统每天都被检查，塔特洛克说：“因为我们希望确保团队工程师编写的代码在出现问题的情况下，能够正确关闭光束。”这项工作类似于DeepSpec项目，只是关注的自动化程度不同。

他还指出，虽然CertiKOS能防止一个应用程序错误地读取另一个应用程序的内存，但是，华盛顿大学的团队没有使用它，因为CertiKOS是一种传统的Unix操作系统，用于运行Unix风格的应用程序，而放射治疗系统中的主要组件都是嵌入式系统，直接在硬件上运行代码。

和塔特洛克的观点一样，阿佩尔和邵中强调只有某些类型的关键软件需要验证。阿佩尔指出，一些验证工具在商业上是可推广的。例如，法国的一个C语言的优化编译器CompCert，正由空中客车公司(Airbus)和欧洲认证机构进行评估，用于编译空中客车喷气客机的飞行线控软件。

阿佩尔说：“相比于空中客车正在使用的编译器，CompCert的优势在于它已经被证明是正确的，无论编译的是什么程序。”

其他航空机构也开始使用形式化验证工具。根据美国国家航空航天局(NASA)兰利研究中心2017年发布的报告，形式化验证工具“已经被证明可以有效地发现安全关键数字系统（包括航空电子系统）中的缺陷” 。同时，美国联邦航空管理局(FAA)已经发布了指南，允许使用形式化方法工具来替换用于“认证信用”的工具。

NASA承认这将是一个缓慢的过程，而且“在形式化验证工具被运用到数字航空电子系统的设计过程中之前，还有许多问题需要解决。”NASA的报告指出，“航空系统的大多数开发人员甚至不了解形式化验证的基本概念，更不用说搞清楚不同的问题领域最适合使用哪些工具了”。有效掌握这些工具既需要技巧，也需要专业知识。

美国国防部高级研究计划署(DARPA)已经开发了一个名为“高可信网络军事系统” (HACMS)的项目。该项目采用一种“从零开始、基于形式化方法的方案，可以从可执行的形式规约中半自动地合成代码”。该方案保证了一个防止黑客攻击的系统，并且“显示我们现在可以将这类系统部署到真实的有关键任务的环境中”，贾甘纳森解释说。

近年来，汽车行业已经意识到汽车是极易受到攻击的。“他们正在迫切地向安全研究人员和验证研究人员寻求解决方法。”阿佩尔认为，在未来十年，将会有更多的行业使用软件验证，并且可以购买更多已经被验证过的软件。

为了使软件验证变得普及，必须有可信的编译器来翻译这些形式化软件验证方法，因为它们是用高级语言编写的。这方面技术正在发展，当可信编译器随处可用时，防黑客软件可能不再仅仅是令人企盼的概念，而会成为一个具体的现实。       ■

注释：

^* 本文译自Communications of the ACM, “Hacker-Proof Coding”, 2017, 60(8):12~14一文。

¹ DeepSpec是美国国家科学基金会(NSF)资助的计算探险项目(Expeditions in Computing)之一。——译者注