编者按

美国国防高级研究计划局（DARPA）6月17日宣布，将推出“弹性软件系统加速器”项目，并将与美军各军种合作开展弹性软件系统顶点演示活动，旨在推动基于“形式化方法”的软件开发实践的广泛采用，提高军事系统的网络威胁抵御能力。

“形式化方法”是指用于开发高可信度、经过验证的软件的技术，其中采用数学证明来证明系统上的软件将按预期运行。“形式化方法”工具和技术具有普遍适用性，有助于提高软件系统的稳定性和抵御黑客攻击的能力，可显著提高美国防部大量已部署遗留代码的安全性，并确保未来系统的安全性。“形式化方法”应用并非在软件构建完成后测试其漏洞，而是在开发过程中使用数学证明来验证软件行为，从而可确保软件完全按照预期运行，从而本质上提高了软件的安全性。DARPA一直在开发利用“形式化方法”的工具和技术，并将大量工具和技术转移到美军各军种进行进一步开发和作战部署。

DARPA 将通过“弹性软件系统加速器”为“形式化方法”工具开发者提供种子资金，而开发者将与国防承包商公司合作，识别出能够从其工具的使用中受益的美国防部系统。相关资金将用于支持对美国防部系统漏洞进行初步红队评估、“形式化方法”工具的应用以及第二次红队评估，以衡量其影响和工作量。工具有效性结果将被纳入DARPA的《交付弹性系统的形式化方法指南》。DARPA表示，此类“评估-改造-再评估”流程对于防御和遏制由传统技术带来的对抗性网络威胁至关重要；“形式化方法”并不能解决所有问题，但可以让对手更难入侵国防工业基础的软件系统，从而达到“锁门关窗”的效果。

作为美国防部内部推进“形式化方法”的一部分，DARPA将通过其“弹性软件系统顶点项目”与美军各军种合作开展演示活动。相关顶点演示将包括对其当前网络漏洞状态的红队评估，随后进行“形式化方法”改进，然后进行后续红队评估，以测试系统可靠性并推动“正确构建”原则的广泛采用。该顶点项目由多个联合资助的作战平台项目组成，旨在评估关键发现，包括弹性、成本、时间的水平以及采用各种“形式化方法”能力所需的专业水平。各项目将持续约24个月，具体目标包括：实现本质上更安全的软件；加快软件操作授权流程；简化软件开发测试；制定最佳实践指南以支持广泛采用。

美国空军是首个确定其试点武器系统的机构，正在通过为MQ-9“死神”无人机加装软件来启动顶点演示。传统上，在开发弹性信息物理系统时，原始设备制造商和项目办公室会按照标准化的行业控制进行设计，使用静态代码分析工具来识别可能导致软件稳定性问题和/或潜在网络漏洞的手动编码错误。挑战在于，传统武器系统软件变化的跨度和复杂性往往导致大量的开发和网络测试，在典型的软件升级计划中，这些测试可能持续12至18个月。而“形式化方法”在应对这些冗长的测试和评估周期方面已展现出良好的前景。DARPA的软件保障/网络弹性工具套件已证明能够在开发环境上游开展更多验证活动，这与软件最终定版后的典型测试阶段截然不同。这些工具专为现有遗留源代码设计，可以直接从代码中生成经过验证的软件行为模型，动态评估软件行为的弹性、稳定性和安全性，甚至可以生成用于操作授权和适航性等认证目的的特定工件。此外，DARPA还将与美国海军部、陆军部以及美国国家航空航天局合作开展其他的顶点项目平台实验。

奇安网情局编译有关情况，供读者参考。

美国国防高级研究计划局（DARPA）6月17日宣布了一项“弹性软件系统加速器”（Resilient Software Systems Accelerator）项目，旨在推动广泛采用基于数学的软件开发实践，使军事系统在抵御网络威胁方面更加安全。

该加速器旨在为那些为国防企业开发“形式化方法工具”的公司提供种子资金。开发者将与国防工业基础公司合作，识别出能够从其工具的使用中受益的美国防部系统。DARPA的资金将用于支持对美国防部系统漏洞进行初步红队评估、“形式化方法”工具的应用以及第二次红队评估，以衡量其影响和工作量。工具有效性的结论将被纳入DARPA的《交付弹性系统的形式化方法指南》（简称“FMDRS指南”）。

作为美国防部内部推进“形式化方法”的一部分，DARPA当日还宣布，将与美军各军种合作进行“形式化方法”应用的顶点演示活动。

“形式化方法”：未来的安全基础

强大而致命的军队需要尖端且高弹性的软件来驱动作战人员所依赖的各种武器和支援系统。然而，美国国防部依赖老化的 IT 基础设施，并沿用过去30年制定的安全策略，导致其系统（从传统架构到先进武器）存在固有漏洞。

与此同时，对手正在积极利用这些漏洞，获取关键系统和基础设施的访问权限。他们还窃取并重新设计敏感的军事系统源代码，以获取美国防部相关系统的知识，从而可能发动与国家安全相关的网络攻击。

为此，美国国防高级研究计划局（DARPA）一直在开发基于“形式化方法”（一种数学上严谨的软件开发方法，有助于在软件部署前消除可利用的漏洞）的开源工具，可以保护几乎所有美国防部系统并证明其不存在可利用的漏洞。“形式化方法”工具和技术具有普遍适用性，可以显著提高国防部大量已部署遗留代码的安全性，并确保未来系统的安全。

“形式化方法”是指用于开发高可信度、经过验证的软件的技术，其中采用数学证明来证明系统上的软件将按预期运行。“形式化方法”的应用有助于提高软件系统的稳定性和抵御黑客攻击的能力。

“形式化方法”并非在软件构建完成后测试其漏洞，而是在开发过程中使用数学证明来验证软件行为。这种方法确保软件完全按照预期运行，从而本质上更加安全。DARPA的许多“形式化方法”工具已经转移到美军各军种进行进一步开发和作战部署。

DARPA呼吁业界协助改善

和加强美国防部网络安全

6月17日，在弗吉尼亚州阿灵顿举行的弹性软件系统研讨会上，美国防部、国防高级研究计划局（DARPA）和业界的领导人谈到了老化的IT基础设施、安全标准和软件工具以及被称为“形式化方法”的技术，这些方法已被证明可以显著提高国防领域使用的军事系统的弹性、安全性和功能性。

DARPA信息创新办公室主任凯瑟琳·费舍尔将“形式化方法”描述为使用户能够证明软件的属性以获得保证的“基于数学的方法”，并补充称DARPA十多年来一直致力于开发与“形式化方法”相关的工具。

凯瑟琳·费舍尔表示，DARPA 迫切希望业界合作伙伴参与其中，因此该机构启动了“弹性软件系统加速器”项目。该项目将为与国防公司合作应用“形式化方法”工具的“形式化方法”工具开发人员提供种子资金，并衡量他们实施这些工具的努力程度。

凯瑟琳·费舍尔称，“我们来这里是为了号召你们采取行动，抓住这个机会，并……鼓励你们倾听并思考，你们的哪些系统可以从‘形式化方法’中受益。DARPA今天宣布，我们将……提供资金，对一个系统进行红队评估。你们先进行一次网络改造，然后再进行另一次红队评估，以评估差异，然后以最佳实践标准格式记录你们在改造过程中所做的工作。”

凯瑟琳·费舍尔表示，此类流程对于防御和遏制由传统技术带来的对抗性网络威胁至关重要。她解释称，国防工业基础（DIB）拥有采用“形式化方法”所需的工具，但鉴于DARPA自2011年以来一直在其“高可靠性网络军事系统”（HACMS）项目中采用“形式化方法”，其在这方面的进展远远落后。

凯瑟琳·费舍尔表示，“我们正在尝试形成一种螺旋式发展，让每个人都达成共识，并有同等程度的意识，即这些技术是存在的，并且已经准备好在黄金时段推出，并且有一个用户群、一个客户群，已经准备好使用这些技术。”

凯瑟琳·费舍尔表示，“形式化方法”可以保证对手入侵DIB软件系统将“变得更加困难”。她称，“我把‘形式化方法’比作安全，用于物理安全，用于房屋、企业、军事设施。目前，我们与网络安全的类比是，我们的门是开着的，我们的窗是开着的。我们实际上知道如何关门、关窗、锁门、锁窗，但我们选择不使用这些技术，我们选择让门开着，窗关着，不用锁。”

凯瑟琳·费舍尔，“形式化方法”并不能解决所有问题，但它是一个良好的开端。她称，“一个防守严密、资源充足的对手，或许仍然能够入侵我们的企业、住宅和军事设施，但难度会大得多，而且能给我们更多时间来保卫自己等等。所以这仍然是一个非常好的决定。”

弹性软件系统顶点项目

作为美国防部内部推进“形式化方法”的一部分，DARPA将与各军种合作进行“形式化方法”应用的顶点演示。每次顶点演示都包括红队对其当前网络漏洞状态的评估，随后进行“形式化方法”改进。改进完成后，将进行后续红队评估，以测试系统可靠性。

DARPA正通过其“弹性软件系统顶点项目”与各军种合作，以应对这一迫切需求。该顶点项目由多个联合资助的作战平台项目组成，旨在评估关键发现，包括弹性、成本、时间的水平以及采用各种“形式化方法”能力所需的专业水平。

每个项目将持续约24个月。目标包括：

  • 实现本质上更安全的软件；

  • 加快操作授权（ATO）流程；

  • 简化软件开发测试；

  • 制定“最佳实践指南”以支持广泛采用。

DARPA顶点项目管理官斯蒂芬·库恩表示，“当国防部系统攸关生命时，目前对国防部系统软件开发的‘修补和祈祷’方法根本是不可接受的。DARPA 通过该顶点顶目的过渡方法将为各军种和行业合作伙伴带来高弹性的软件工具，并使我们能够汲取经验教训，推动‘正确构建’（correct by construction）原则的广泛采用。这项工作将成为一个模板，可供其他机构使用，帮助他们快速启动将DARPA的高弹性软件工具融入其平台和开发流程的工作。”

美国空军是第一个确定其试点武器系统的机构——MQ-9“死神”计划，由通用原子航空系统有限公司（GA-ASI）开发。美国空军正在通过为MQ-9“死神”无人机加装软件，启动顶点演示。

传统上，在开发弹性信息物理系统时，原始设备制造商（例如 GA-ASI）和项目办公室会按照标准化的行业控制进行设计。他们使用静态代码分析工具来识别可能导致软件稳定性问题和/或潜在网络漏洞的手动编码错误。

挑战在于，传统武器系统软件变化的跨度和复杂性往往导致大量的开发和网络测试，在典型的软件升级计划中，这些测试可能持续12至18个月。

“形式化方法”在应对这些冗长的测试和评估周期方面已展现出良好的前景。DARPA的软件保障/网络弹性工具套件已证明能够在开发环境上游开展更多验证活动，这与软件最终定版后的典型测试阶段截然不同。这些工具专为现有遗留源代码设计，可以直接从代码中生成经过验证的软件行为模型，动态评估这些行为的弹性、稳定性和安全性，甚至可以生成用于操作授权（ATO）和适航性等认证目的的特定工件。

简而言之，项目办公室和原始设备制造商现在拥有可用于现有代码的软件加速工具，可以补充软件采购途径等政策改进。

美国空军选择MQ-9作为顶点

美国空军将与 DARPA 密切合作，将严谨的“形式化方式”纳入其 MQ-9“死神”无人机项目。与DARPA合作开展顶点项目的美国空军团队之所以选择 MQ-9，是因为该武器系统本身的技术门槛较低，而且组织企业内部的文化门槛也较低。

美国空军生命周期管理中心中空无人机系统部门首席工程师奥伦·爱德华兹表示，“MQ-9顶点项目将通过逐步提高我们加速将强大而有弹性的武器系统软件投入战场的能力来改善对DARPA计划的支持。”

他称，“数字化转型的文化壁垒之一是误以为需要投入大量时间和金钱才能证明项目转型成功，这种误解通常与‘死亡之谷’联系在一起。事实上，投资是必需的，但政府和商业工具的整个产业都在不断证明这种误解是错误的，而这正是我们正在做的。使用DARPA的保障加速工具将某些验证活动移至软件开发周期的上游，不仅可以提高MQ-9的敏捷性，还将为美国空军和国防部的后续项目提供重要的杠杆机会。”

DARPA还将与美国海军部、陆军部以及美国国家航空航天局（NASA）合作开展额外的顶点项目平台实验。

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