【编者按】数字化时代，核武器作为最苛刻的安全关键系统，如何测试其软件系统的功能性和安全性？如何挖掘软件及组件中的bug？软件开发和测试的标准方法对于这些系统来说是危险的。如果没有办法检查每一行代码以及软件可能产生的每一种可能的状态组合，有什么可以替代的方案？美国国防分析研究所Laura Epifanovskaya博士介绍了对数字化武器的形式化测试方法。测试设计可以通过要求在核武器中使用的所有软件中使用形式化的数学方法来解决软件复杂性的问题。形式化方法是用于对复杂软件系统进行数学建模的技术，使工程师能够“证明”一段代码的行为完全符合预期，就像数学家证明定理一样。虽然典型的软件开发周期侧重于主要的程序编写步骤，但程序作为稍后的单独步骤进行测试，形式化方法创建的代码从一开始就专门设计用于提交正式评估。为了在验证中真正发挥强大效能，需要在设计阶段应用形式化方法来生成可以使用数学方法进行分析的代码。除了形式化测试和验证过程之外，使用形式化方法的测试设计还显著降低了软件复杂性。

以下内容编译自Laura Epifanovskaya博士的论文。

如果对美国本土的下一次勒索软件攻击涉及核武器怎么办？正在采取什么措施来确保这个可怕的假设永远不会成为现实？

作为美国国家核安全局库存管理计划的组成部分，美国核武库中的武器经常进行飞行测试，以确保其安全性和可靠性。然而，武器设计正在发生变化，包括更多的数字组件和通信。传统武器在大多数操作中使用模拟信号和机械切换。数字武器依赖于软件，而当代码支撑生死机制时，标准的软件测试实践不足以防止故障。

软件测试无法满足武器安全性、安保性和可靠性的高标准——特别是Walske标准，它要求核武器在常规条件下产生意外当量的机会不超过十亿分之一，在异常环境中（例如，在火灾中）不超过百万分之一的机会）。因此，数字设计带来的新风险迫使改变武器设计和测试的基本方法。这需要对当前方法进行两个根本性的改变。首先，测试武器和真实武器应该几乎相同——这意味着设计武器系统时要包括嵌入式传感器等测试设备。其次，武器的设计应采用可数学分析的软件，以便能够进行比目前更严格和更详尽的数字测试。这两个建议合起来就是一个，核武器设计方法的根本变化：项目需要“为测试而设计”。如果没有为测试而设计的方法，带有嵌入式软件和固件的武器就无法满足Walske标准。

测试设计如何影响数字安全和安保？投资新方法可以使测试数字架构更加彻底，结果更加可靠。首先，我们必须了解为什么测试软件如此困难。这是因为软件很复杂，由一个巨大的“状态空间”组成——一个程序可以达到或最终进入的可能状态的数量。这个状态空间的庞大规模使得不可能对软件进行详尽的测试——也就是说，测试每一个可能的状态，即使是非常小的程序。Beat Fluri博士在他的在线软件测试研讨会上举例说明了一个非常简单的例子：一个有四个变量的程序有2的32次方种可能的输入组合，总共有4个2的32次方，共2的128次方个不同的值。以每秒1,000行的速度探索这个输入空间需要10的28次方年：10后有28个零比宇宙的年龄还要长。软件错误可能不会被发现，仅仅是因为测试每个可能的状态是不可行的。我们不能用整个宇宙的生命周期来测试一个小程序。

举一个由隐藏错误引起的意外软件行为的例子，回想一下导致丰田汽车在驾驶员松开油门踏板后继续加速的“油门粘滞”。它导致了多次碰撞和死亡，最初被归咎于踏板和垫子设计的机械问题。2013年，陪审团裁定，根据专家证词，该设计缺陷是由电子油门控制软件中的不可预见状态引起的。专家作证说，丰田源代码包含可能导致意外加速的错误，并且丰田工程师实施了糟糕的编码实践和安全架构。在安全关键型设计中，软件依赖于良好的实践和架构来影响安全性和可靠性，因为即使是最广泛的软件测试也不能指望发现导致危险问题出现的每个独特的状态组合。

核武器是最苛刻的安全关键系统，没有办法检查每一行代码以及核软件可能产生的每一种可能的状态组合。软件开发和测试的标准方法对于这些系统来说是危险的。

“这会做它应该做的吗？” 与“它不会做它不应该做的事吗？”

不过，还有另一种选择。最有效的软件测试是作为设计过程的一部分进行的，既消除了软件错误，又消除了在已开发软件中发现问题时可能进行的代价高昂的重新设计工作。测试设计可以通过要求在核武器中使用的所有软件中使用正式的数学方法来解决软件复杂性的问题。形式化方法是用于对复杂软件系统进行数学建模的技术，使工程师能够“证明”一段代码的行为完全符合预期，就像数学家证明定理一样。虽然典型的软件开发周期侧重于主要的程序编写步骤，但程序作为稍后的单独步骤进行测试，形式化方法创建的代码从一开始就专门设计用于提交正式评估。为了在验证中真正强大，需要在设计阶段应用形式化方法来生成可以使用数学方法进行分析的代码。除了形式化测试和验证过程之外，使用形式化方法的测试设计还显著降低了软件复杂性。

为了说明原因，想象一个执行简单功能的小程序，比如说一个恒温器，它读取温度，然后调节房子的供暖或制冷。首先想象用英语句子描述恒温器的功能，然后想象用方程式描述相同的功能。数学方程式提供了一种简短、易于检查的格式来表达与英语语句或软件编程语言中的语句相同的功能。这种方法还消除了错误设计的正确软件实现可能导致的错误（竞争条件，其中程序输出基于不受控制的事件序列而变化，有时是由于设计不当造成的）。核威胁倡议确定了需要“在预期行为边界之外进行探测，以试图发现核武器系统中的意外弱点”。模型检查，一种形式化方法中的技术，提供了一种方法来做到这一点。模型检查器用于以数学语言对软件程序和安全（或其他）规范进行建模，然后通过测试不希望的行为（例如违反安全条件）来证明软件符合规范。标准软件测试通常只确保满足期望的条件——要证明诸如安全违规之类的不期望的条件永远不会发生要困难得多。模型检查器有助于确保软件规范本身是正确的，并在编写一行代码之前产生所需的行为。亚马逊工程师认可正式的软件规范作为“防止严重但微小的错误进入生产环境”的一种方式。

对所有美国核武器施加的所谓“始终/从不”要求——这些武器在总统授权时将始终按预期工作，否则永远不会工作——要求对正式技术进行广泛授权。使用新技术应用旧的安全性、安保性和可靠性标准需要全面的新开发标准和方法。

让测试武器更像真正的武器

与软件复杂性相关的数字系统的另一个挑战是网络漏洞。由于软件的复杂性，漏洞可以被创建并且未被发现，漏洞仅被认为与软件“错误”不同，因为它们可能被故意利用以在程序中产生软件开发人员不希望的行为。恶意行为者可能通过软件更改重新编程核武器操作的可能性会产生明显的安全问题。如果先进的对手国家能够渗透到核武器的数字控制系统中，特别是如果他们能够在未被发现的情况下这样做，可能会产生严重的后果。形式化的方法在这里也有帮助：它们被用于国防高级研究计划局的高保证网络军事系统计划，旨在制造“不可破解”的车辆，例如四轴飞行器、直升机和汽车。然而，制造能够抵御网络威胁的武器系统涉及测试网络漏洞和已经通过供应链感染武器系统的恶意软件。

测试设计还可以通过将测试仪器（例如检测武器何时引爆的传感器）直接整合到弹头或炸弹体设计中来解决武器网络安全问题。为什么这会对武器网络安全产生影响？

首先，核武器由两个主要部件组成：炸弹或弹头，以及运载平台。美国使用称为联合测试组件的测试版本（其首字母缩写JTA更广为人知）测试其核武器的非核功能——引信和发射。联合测试组件是核武器主体——炸弹或弹头——移除了核爆炸物，配备了检测重要事件参数所需的传感和其他仪器，这些事件参数表征被测武器的引信和发射。作为能源部和国防部联合测试的一部分，它们在国防部拥有的武器运载平台（轰炸机，如 B-2、巡航导弹或弹道导弹）上飞行投送平台，因此得名“联合测试组件”。将测试仪器安装到核弹头或弹体中需要改变其内部配置，包括修改电气和数字电路。由于这些变化，每年测试的联合测试组件与库存中的核武器并不相同。由于联合测试组件设计与库存设计不同，国防部和能源部对高保真或“HI-FI”设计进行了一些额外的飞行测试。这些测试炸弹不包含联合测试组件所具有的内部数据收集传感器——它们在移除核爆炸物的情况下飞行战备级武器。进行高保真测试以确保武器按预期飞行并在飞行路径末端引爆，

这些测试，无论是仪器仪表还是高保真HI-FI，都非常昂贵，每次都需要重新利用直接从核武库中提取的价值数百万美元的武器。如果有一个测试同时执行联合测试组装和高保真HI-FI的功能，国防部和能源部将在每次测试中收集更多数据，每花费一美元收集更多数据。不仅如此，它们还可以显著改善美国核武器库存的网络安全。这可以通过测试设计来完成，将测试仪器直接设计到炸弹或弹头的主体中，使测试武器和战时武器相同。

以WannaCry为例，高保真为何重要！

直接将测试仪器纳入武器设计改善网络安全态势的原因可以通过WannaCry勒索软件病毒的例子来说明，WannaCry在2017年发起了一场全球网络攻击。该病毒加密了计算机用户数据，并要求以比特币加密货币付款来解密它。WannaCry hack在这里是相关的，因为如果在供应链中引入类似WannaCry的恶意软件，将不会在联合测试中检测到。原因很简单：该病毒被设计成能够判断它何时进入虚拟机环境并隐藏——即，什么都不做——因为虚拟机是大多数恶意软件测试发生的地方。然而，一旦进入真实世界的环境，病毒就会从隐藏中出来并执行它的任务。WannaCry通过ping 一个假的、未注册的域名的互联网地址巧妙地感知到测试环境的存在，哪些虚拟测试机被承认为真实域名（因为虚拟机被设计为对域名的真实性或不真实性无动于衷）。真正的互联网会将相同的域名识别为假域名——它无法解析域名。该病毒使用域名的解析或不解析作为隐藏或复活的信号。当安全研究人员发现这个触发器时，它被重新用作“终止开关”——他们注册了域名，导致病毒进入休眠状态。

以类似的方式，针对核武器系统的恶意软件可能会感知武器测试配置与其战时使用配置之间的差异，以确定是出现还是保持休眠状态，从而使其在测试期间保持隐藏状态。恶意软件只会在真正的任务场景中自我激活，导致武器失灵或更糟。

这种网络安全问题可以通过设计测试武器和战时武器来减轻，通过测试设计方法。例如，现代武器可以设计有嵌入式测试设备，这些设备可以执行典型的飞行测试任务，例如爆炸感应，但在战时也可以保留，而不会损害任务。至少自 2013 年以来，核武器工程师一直在讨论“仪器化高保真”测试物品的可能性——即，真正的战备武器，其制造的测试仪器永久保留在武器中，当时一个实验室工程师团队（包括作者）设计了一个原型嵌入式传感器，可用于仪表化的高保真武器。早在 2013年之前，促成这一设计的讨论就一直在进行。

如果数字升级如此冒险，为什么要进行？

为什么不坚持旧的、模拟的、网络安全的设计呢？核武器走向数字化有两个原因。主要原因是国防部的投送平台，如B-2和新的B-21 Raider飞机，被吹捧为“数字发展的奇迹”，通过数字接口进行通信，武器必须能够向这些数字平台发送和接收命令。另一个原因是需要数字设计的功能和灵活性，尤其是包含处理器的设计，而不是定制组件，例如专用集成电路。对于基于处理器的设计，只需更改几行代码即可解决性能问题并立即重新测试设计。对于在安全设施中制造的集成电路，同样的变化可能需要几个月的时间。如果安全设施有工作积压（这些需求资源的常见问题），则可能需要更长的时间。

综上所述，这些条件确保软件仍将是核武器设计的一部分。现在的任务是确保核武器与过去几十年一样安全、可靠和可信。现代数字武器设计提出了重大的新挑战，但其中许多挑战都可以通过上述测试设计方法来解决。形式化方法降低了复杂性并使软件可分析和可验证，它们还为黑客提供了一种安全措施。使测试武器和真实武器有效地相同将提高测试的准确性，减少必须进行的数百万美元测试的数量，并关闭至少一个由恶意软件引起的潜在网络安全漏洞，这些漏洞可以判断它何时处于测试环境中并处于休眠状态。

这些步骤将需要对当前的方法和人员和计划的投资进行重大改变，但它们对于使新的数字核武器设计安全、可靠和可信地达到历史悠久的旧标准非常重要和必要。核武器数字技术带来的挑战是我们知道如何应对的挑战。是时候投资于人员、工具和满足它所需的变革了。

作者简介

Laura Epifanovskaya是国防分析研究所的一名研究人员，为国防部采购计划开发新的软件测试方法。在加入IDA之前，她是能源部核武器综合机构的系统工程师和威慑分析师，负责监督国家安全系统的数字和供应链安全，并开发了研究战略核威慑的定量方法。Epifanovskaya拥有南加州大学物理化学专业博士学位。

声明：本文来自网空闲话，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。