编者按
美国国防高级研究计划局（DARPA）正围绕“形式化方法”开展前瞻创新研究，并寻求将有关研究成果向美军广泛推广，从而防范软件漏洞引起的灾难性网络事件。
“形式化方法”已显示出巨大的潜力，可以证明软件系统的正确性并提供持续的证据。该方法不是仅通过在编写软件代码后对其进行测试来验证其安全性，而是通过严格的数学分析来设计软件，在构建之前和构建过程中验证其性能。该方法在工具、实践和培训方面的最新革命性进步促进了更大规模应用，预示着缺乏形式化方法培训的传统软件开发人员和工程师有更多机会获得价格合理的工具。DARPA认为，通过创建一个可持续的“形式化方法”工具生态系统，可以打造一个“软件不再存在任何漏洞的世界”，并消除美国防部认为系统无法避免由软件漏洞引起的灾难性网络事件的“习得性无助感”。DARPA围绕“形式化方法”开发的一些网络安全工具已进入美国防部备案项目，但采用程度有限。因此，DARPA正试图提高美国防采购界对解决方案存在且可供使用的认识，敦促美国防部管理人员利用闲置的DARPA网络安全工具，以防止关键项目遭受黑客攻击和事故。
DARPA近年来开展了大量研究工作，证明了“形式化方法”的软件设计方法可以在漏洞被编码错误或攻击利用前予以解决。其中，“高可靠性网络军事系统”（HACMS）项目寻求创建用于构建高保证信息物理系统的技术，可支持高可靠性军事系统，包括无人驾驶载具、武器系统、卫星以及指挥和控制设备，并已实际展示形式化方法可以消除飞机嵌入式系统中的重要安全漏洞；“安全文档”（SafeDocs）项目寻求开发新颖的经过验证的编程方法，用于为现有电子数据格式构建高保证解析器，并开发新颖的方法将相关格式理解、简化和减少为安全、明确、易于验证的子集，从根本上提高了软件拒绝无效和恶意数据的能力；“有保证的微补丁”（AMP）项目寻求开发工具和方法，借助有保证的、有针对性的“微补丁”来分析、修改和修复二进制形式的遗留软件，并确保系统的原始基线功能不会因修复而丢失或改变；“经过验证的大型遗留软件的安全性和性能增强”（V-SPELLS）项目寻求使开发人员能够使用新的验证代码逐步增强现有的遗留软件组件，并确保生成的软件能够安全地与现有系统组合；“验证器流水线推理实现稳健系统”（PROVERS）项目寻求开发形式化方法工具，指导软件工程师设计易于验证的软件系统并减少验证修复工作量，最终为国家安全系统提供一条应对网络安全威胁的途径，实现高保证系统工程，并生产具有可验证安全属性的网络强化、弹性的系统和支持基础设施。
奇安网情局编译有关情况，供读者参考。
几十年来，依赖软件的系统的工程实践一直在稳步发展，确认系统正确性和安全性的保证技术也在不断发展。数学上严谨的技术，即“形式化方法”（Formal methods），已显示出巨大的潜力，可以证明软件系统的正确性并提供持续的证据。
然而，这些技术中的大多数仍然高度专业化，需要高水平的专业知识。最近，形式化方法社区在工具、实践和培训方面的革命性进步促进了该方法的更大规模应用。这些进步预示着一个转折点，可能让缺乏形式化方法培训的传统软件开发人员和工程师有更多机会获得价格合理的工具。
01
DARPA大力推行“形式化方法”
以防网络灾难
随着恶意网络威胁不断增加，美国国防高级研究计划局（DARPA）正积极倾向于开发围绕“形式化方法”技术的框架，以更好地保护作战系统，愿景是打造一个软件不再存在任何漏洞的世界。
近年来，敌对性事件或意外事件等网络安全事件变得越来越普遍，例如2017年NotPetya网络攻击、2024年安全公司CrowdStrike的软件故障导致的全球宕机等。而美国国防部和美国政府在解决软件漏洞方面形成了“习得性无助感”。DARPA信息创新办公室主任凯瑟琳·费舍尔表示，这些事件凸显了关键基础设施中令人担忧的软件漏洞，同时凸显了美国国防官员在面对造成的损害时表现出的消极态度。由于认为系统无法避免由软件漏洞引起的灾难性网络事件，国防部往往专注于被动修复。
凯瑟琳·费舍尔表示，“我们可以想象一个没有这些软件漏洞的世界，我们可以消除国防部的习得性无助感，我们可以迅速保护关键系统……我们可以创建一个可持续的形式化方法工具生态系统，供人们随时使用。”
在过去的10到15年里，DARPA已经证明，“形式化方法”的软件设计方法可以在这些漏洞被编码错误或攻击利用之前解决它们。“形式化方法”不是仅仅通过在编写软件代码后对其进行测试来验证其安全性，而是通过严格的数学分析来设计软件，在构建之前和构建过程中验证其性能。
DARPA早期的一个项目展示了形式化方法的实用性，即“高可信网络军事系统”（HACMS）。此后，DARPA还开展了多项其他工作，以提高国防部平台形式化方法的可用性。其中，“安全文档”（SafeDocs）的项目解决了解析器（将数据转换为可用格式的软件工具）中的漏洞；另一项名为“有保证的微补丁”（AMP）项目提供了一种无需源代码即可修复软件漏洞的方法，并确保修复本身不会造成更多损害；“经过验证的大型遗留软件的安全性和性能增强”（V-SPELLS）项目寻求创建可以永久且经济地修复旧代码中所有漏洞的工具，利用经过验证的、有保证的代码对现有系统进行增量软件修复和增强；“验证器流水线推理实现稳健系统”（PROVERS）项目寻求开发形式化方法工具，指导软件工程师设计易于验证的软件系统并减少验证修复工作量。
DARPA开发的一些工具已进入美国防部备案项目，但采用程度有限。现在，随着人们对军事武器系统网络安全的担忧日益加深，DARPA正试图提高美国防采购界对这些解决方案存在且可供使用的认识。该机构官员已开始敦促美国防部管理人员利用闲置的DARPA网络安全工具，以防止关键项目遭受黑客攻击和事故。
美国防部采用这些工具的速度和范围取决于许多因素，包括军队内部的资金和优先顺序。为了帮助宣传和解决采用障碍，DARPA于2024年启动了Capstone项目。通过与美国防部研究与工程部副部长和作战测试与评估主任的合作，DARPA正在与美军各军种合作，以确定可以从形式化方法中受益的平台。
DARPA正在提供一些配套资金来提供这些工具，据DARPA信息创新办公室项目经理史蒂夫·库恩表示，预计将在5月前确定平台。一旦Capstone项目被选中，DARPA将帮助识别和修复其中的软件漏洞，并收集经验教训，汇编成所有项目都可以访问的最佳实践指南。史蒂夫·库恩表示，库恩表示，DARPA希望该指南能够帮助国防部项目办公室了解弹性软件工具的应用方式，并提供有助于实施的资源。
DARPA成功运用形式化方法技术的一个主要例子是“星座”（Constellation）计划。该计划于2022年作为DARPA和美国网络司令部间的一个试点项目启动，两家机构还达成了一项新的具有约束力的协议，以将该计划推向未来。“星座”计划的重点是“创建一条将网络技术从实验室转移到网络战场的快速通道”。
02
“高可靠性网络军事系统”
(HACMS) 项目
嵌入式系统形成了一种无处不在的网络化计算基础，构成了现代技术社会的基础。此类系统包括管理物理基础设施的大型监控和数据采集（SCADA）系统、起搏器和胰岛素泵等医疗设备、打印机和路由器等计算机外围设备、手机和收音机等通信设备以及飞机和卫星等交通工具。此类设备联网的原因多种多样，包括方便访问诊断信息、执行软件更新、提供创新功能、降低成本和提高易用性。研究人员和黑客已经表明，这些联网嵌入式系统容易受到远程攻击，此类攻击可以造成物理损坏，同时隐藏监控器无法察觉的影响。
DARPA的“高可靠性网络军事系统”（HACMS）项目的目标是创建用于构建高保证信息物理系统的技术，其中高可靠的定义是指功能正确并满足适当的安全和安保属性。
实现这一目标需要采取与软件社区迄今为止所采用的方法完全不同的方法。因此，HACMS采用一种全新的、基于“形式化方法”的方法，以便从可执行的形式化规范实现半自动化代码合成。除生成代码外，HACMS还寻求一种能够生成机器可检查验证的合成器，证明生成的代码满足功能规范以及安全和保障政策。一个关键的技术挑战是开发技术以确保此类验证是可组合的，从而允许使用高可信度组件构建高可信度系统。HACMS的关键技术包括交互式软件合成系统、定理证明器和模型检查器等验证工具以及规范语言。
HACMS项目从2012年运行到2016年，并进行了两次演示，第一次使用小型四轴飞行器无人机，然后在2017年使用波音公司的自动直升机无人小鸟。在第二次演示中，一支红队黑客试图入侵飞机，但没有成功。HACMS项目承包商表示，“在HACMS中，我们展示了可以使用形式化方法消除真实飞机嵌入式系统中的重要安全漏洞。”
对于国防部门，HACMS将支持高可靠性军事系统，包括无人驾驶载具、武器系统、卫星以及指挥和控制设备。
03
“安全文档” (SafeDocs) 项目
对于常用的电子数据格式，输入验证至少是一个规模问题，因为这些格式的规范包含数百到数千页。因此，输入验证意味着需要针对输入数据检查数千个或更多条件，然后才能安全地处理数据。手动编写代码来解析和验证输入，然后手动审核该代码是否完全正确地实现了所有必要的检查，这种做法不具可扩展性。
此外，即使对于专门设计为更易于执行此类任务的电子数据格式（例如JSON和XML），手动解析器编码和审计通常也会失败。在这些格式的主要解析器实现中发现了各种严重漏洞。
针对精心设计的输入攻击，广泛部署的缓解措施包括：尝试阻止不受信任的数据流向易受攻击的软件；使用随机输入测试软件，以查找和修补可能由恶意创建的输入触发的漏洞。不幸的是，上述两种方法都无法提供安全保障。
防止不受信任的数据流向易受攻击的软件的缓解措施可以通过网络或基于主机的措施（如防火墙、应用程序代理、防病毒扫描程序等）来实现，这些措施既不能消除目标的底层漏洞，也不能对文档或消息格式内部的完整知识进行编码。攻击者绕过此类缓解措施，利用缓解措施对数据格式理解的不完整性来利用仍然易受攻击的目标。
“安全文档”（SafeDocs）项目于2018年启动，最初的目标是提高电子通信的安全性，特别是在军事或政府行动等敏感或关键应用中。该项目寻求开发新颖的经过验证的编程方法，用于为现有电子数据格式构建高保证解析器，以及开发新颖的方法来理解、简化和减少这些格式为安全、明确、易于验证的子集（“安全子集”）。
“安全文档”项目将解决现有电子数据格式带来的模糊性和复杂性障碍，这些障碍阻碍了经过验证的编程的应用。该项目“多管齐下”的方法将结合：
提取现存格式的事实语法（包括任何故意接受并在野外大量使用的不符合规范的语法）；
识别该语法中一个语法更简单的子集，该子集可用于经过验证的编程，同时保留该格式的基本功能；
创建软件构建工具包，用于为这个语法上更简单的子集构建安全、经过验证的解析器，以及创建高保证度的转换器，用于将现存的格式实例转换为该子集。
“安全文档”项目开发的解析器构建工具包可供了解电子数据格式语法但缺乏验证编程理论背景的行业程序员使用。这些工具将使开发人员能够为新的电子数据格式以及现有的电子数据格式构建可验证的解析器。这些工具将指导新格式的语法设计，使易于表达的验证友好格式语法变得容易，反之亦然。
“安全文档”项目的研究和开发降低了文档格式的复杂性，即文档必须遵守的规则，以便软件可以打开它们。此外，研究团队从根本上提高了软件拒绝无效和恶意数据的能力，而不会影响新旧电子数据格式的核心功能。“安全文档”项目开发的工具还有助于保存电子文档历史记录并使功能丰富的电子文档保持可行。
04
“有保证的微补丁”（AMP）项目
关键基础设施由大量不同的计算设备运行，从交通系统到电网再到工业设备。与商用或个人计算设备非常相似，这些系统利用嵌入式软件来执行和管理其操作。为了修复某些安全漏洞，商用和个人设备必须频繁更新，每隔几年更换一次，有时在更新失败时更换更频繁。关键任务系统的使用寿命长达数十年，很少会有相同的短升级周期。这些系统的开发成本高昂且难以更换，而且随着它们为了维护诊断和数据收集而越来越多地相互连接，这种连接软件的激增使它们容易受到攻击。虽然部署的易受攻击软件的数量呈指数级增长，但大规模解决已知漏洞的有效手段却有限。
识别和修复遗留二进制文件中的软件漏洞需要技术精湛的软件工程师，他们能够根据可用的源代码示例和/或对原始开发环境的有限了解做出专家假设。工程师负责了解二进制文件的结构，手动开发和应用补丁，然后手动分析和测试二进制文件以确保其正常运行。此过程既费力又耗时，而且几乎不能保证系统在应用修复后仍能按预期运行。此外，随着关键任务系统中部署的软件数量不断增长，这种方法变得越来越站不住脚。
“有保证的微补丁”（AMP）项目寻求解决这些挑战，并加速修补任务关键型系统和基础设施中旧二进制文件的过程。该项目旨在开发工具和方法，借助有保证的、有针对性的“微补丁”来分析、修改和修复二进制形式的旧软件。微补丁是小补丁，它们尽可能少地更改二进制文件，以实现预期目标，同时最大限度地减少修复的潜在副作用。该项目旨在创建突破性技术来推理这些小型软件修复，并且提供证据以确保系统的原始基线功能不会因修复而丢失或改变。
为实现上述目标，“有保证的微补丁”项目寻求通过技术突破和新方法解决当前软件开发范式中的差距，包括但不限于：
识别可执行二进制映像中的模块单元，并识别模块的接口、交互和链接工件，以便随后确保修补的二进制模块重新链接和重新集成；
将可执行二进制代码反编译为适合自动为二进制中已知的安全漏洞打补丁的形式；
为现有的二进制图像生成最小变化的二进制微补丁，并对其效果进行严格推理，然后测试这些效果以验证这些变化不会干扰二进制的基线功能；
使用可用的信息源（例如源代码和二进制样本）来恢复源代码和构建过程缺失的相关部分。
05
“经过验证的大型遗留软件的安全性
和性能增强” (V-SPELLS) 项目
当前，美国国防和商业系统都充斥着难以现代化、增强和重新设计的遗留软件，这主要是由于缺乏对底层遗留代码的有效理解，这使得预测修改的影响成为一项挑战。从国防的角度来看，越来越需要用更安全、性能更高的代码来增强或替换关键平台和系统中现有软件的组件，以及希望在新硬件上使用遗留软件来提高系统性能。然而，在向大型遗留代码库引入增强或替换时，新代码无法与系统其余部分安全组合的风险很高。现有的验证更新软件是否正确构建的方法侧重于全新软件开发，本质上将其有效性限制在从头开发的软件上。此外，这些方法假设存在遗留系统通常不具备的现有形式化规范，并且它们需要大多数开发人员不易掌握的形式化方法的一定程度的专业知识。
为了应对上述挑战，DARPA的“经过验证的大型遗留软件的安全性和性能增强”（V-SPELLS）项目旨在使开发人员能够使用新的验证代码逐步增强现有的遗留软件组件，并确保生成的软件能够安全地与现有系统组合。该方法的关键是能够进行增量更新，这些更新既正确又兼容，而无需从头开始进行软件开发或完全替换软件代码库。为实现目标，V-SPELLS项目寻求结合程序理解和验证方面的新颖概念，以及领域特定语言（DSL）和大规模生产系统的可组合系统架构的最新发展。
V-SPELL项目寻求在以下技术挑战方面取得突破并采用新方法，包括但不限于：
自动程序理解，推断遗留源代码库中的架构结构、假设和依赖关系，使其能够分解为具有明确模块结构、接口、依赖关系和约束的组件。从遗留代码库中恢复领域抽象和模型，以简洁且富有表现力的表示形式，适合对可与现有系统安全组合的功能组件增强或替换进行编程。
将已知和提取的领域抽象和模型与遗留代码进行匹配，将遗留代码提升为简洁、可增强、可安全组合和可互操作的表示形式，并利用此类表示形式进行自动化规范推理。增强功能与系统其余部分的组合是可证明安全的。
利用新颖的经过验证的跨层优化和分布技术（“经过验证的堆栈扁平化和分布”）克服由于增加抽象层而导致的性能下降。开发用于可组合表示、打包和转换软件验证证明的非脆弱和细粒度规则，以支持经过验证的程序的分发和编排。
美国陆军、海军、空军和海军陆战队计划将分别向DARPA提供一个遗留平台，以证明V-SPELL项目工具的有效。
06
“验证器流水线推理实现稳健系统”
(PROVERS) 项目
通过一门被称为“验证工程”的新兴学科，DARPA致力于创建更高水平的保证，帮助关键的国防部软件系统免受某些类别的缺陷和漏洞的影响。
验证工程将帮助开发人员安全地构建软件并确保软件满足指定的保证要求。DARPA的“验证器流水线推理实现稳健系统”（PROVERS）项目将开发形式化方法工具，指导软件工程师设计易于验证的软件系统并减少验证修复工作量。
DARPA信息创新办公室PROVERS项目经理威廉·马丁表示，“美国防部软件在作战、保护国家资产和保障人类生命方面发挥的作用日益增强，对错误保证判断的容忍度也越来越低。PROVERS的最终目标是为国家安全系统提供一条应对网络安全威胁的途径，实现高保证系统工程，并生产具有可验证安全属性的网络强化、弹性的系统和支持基础设施。”
PROVERS建立在“软件验证工程、调整、修复和学习”（PEARLS）人工智能探索项目的基础上，该项目展示了人工智能和机器学习如何支持和自动化大规模软件形式验证中使用的证明的生成和维护。PROVERS是一个为期42个月的项目，涵盖三个阶段，包括验证工程、平台开发、模拟潜在对手攻击的红队，以及一个单独的联邦资助研究和开发中心，以提供定量评估和证据管理。
声明：本文来自奇安网情局，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
