国防高级研究计划局（DARPA），五角大楼的研究与开发机构，正在询问行业和研究人员如何自动生成同一军事系统的多个不同版本，每个版本都经过数学证明能够完成相同的任务，但在构建上有足够的不同，以至于攻击或故障导致一个版本失效时不会影响其他版本。该信息请求于11月3日由DARPA的信息处理技术办公室发布，涵盖了一个名为“系统异构性的形式学习与抽象”（FLASH）的项目，响应截止时间为11月30日下午5点（东部时间）。
该通知（DARPA-SN-27-17）属于市场研究，而非招标，DARPA尚未宣布任何后续奖励的项目、预算或时间表。该机构表示，将会丢弃任何针对该请求提交的摘要或提案，并且不会支付响应费用。
FLASH的核心思想是可以将多样性作为一种防御手段。DARPA希望将系统的高层需求与任何单一设计的细节分开，然后利用这种分离生成多个设计实例，这些实例保持相同的指定属性，同时在故障模式和攻击面上有所不同。如果对手发现一个实例中的漏洞、配置弱点或共同故障，该机构认为，这种知识的持久性将较低，且更难转移到其他实例。
该机构描述了三个技术重点。第一个是形式化系统的需求、操作意图和不变性，即必须永远保持不变的属性，同时暴露出可以自由变化的设计选择。第二个是生成具有保证功能等价性和形式可证明正确性的不同设计实例。第三个是在每个设计旁边生成保证和解释材料，以便可以通过数学方式展示正确性、多样性和韧性，而不仅仅依赖于测试进行评判。
为此，DARPA希望将基于生成模型的软件代理与符号推理相结合，符号推理是用于形式验证的基于规则的逻辑，以捕捉设计意图并合成其所称的语义异构的网络物理工程系统。网络物理系统是指软件直接控制物理硬件的系统，例如飞行控制、武器、车辆或工业设备。该请求列出了希望响应者解决的具体技术，包括由oracle引导的归纳合成，其中程序是从示例构建的，并反复与验证器进行检查，以及将生成的多模态基础模型与交互定理证明器配对，这些工具使工程师和软件能够构建机器检查的数学证明。
DARPA列出了自主战术平台、安全通信管道、工业控制系统、自主机器人车队、高性能计算集群、边缘计算网络和网络安全工具作为该方法可能适用的示例。它要求响应者定义目标应用及其威胁环境，解释当前加固方法的不足之处，并确定在每个生成版本中必须保持固定的功能、安全、保密、时序、互操作性和性能属性。
第二组问题涵盖了如何构建和测量这样的系统。DARPA要求提供异构性的度量标准、验证功能等价性的方法以及测试针对自适应对手的韧性的实验，包括其所称的使用智能代理的自主利用开发。它还询问了系统设计的单代理和多代理架构，以及特定应用的可重用形式规范、模型和证明库。
在1977年，Liming Chen和Algirdas Avizienis提出了N版本编程，其中独立团队根据相同的规范编写不同的程序，投票者比较它们的输出，假设独立开发的软件会独立失败……
仅显示内容预览。完整文章请访问原始来源。 查看完整文章
国防高级研究计划局（DARPA）正在启动FLASH计划，以开发能够抵御网络攻击的多样化军事系统。该倡议于2026年11月3日宣布，旨在创建多种版本的军事系统，这些系统在设计上有所不同，但保持相同的操作能力，以防止漏洞被利用。对信息请求的响应截止日期为2026年11月30日，DARPA旨在增强网络物理系统的韧性。
- 国防高级研究计划局（DARPA）正在启动FLASH计划，以创建多样化的军事系统。
- 该计划旨在生成多种版本的军事系统，以增强抵御攻击的韧性。
- 对DARPA的信息请求的响应截止日期为2026年11月30日。
- FLASH计划专注于规范系统要求并生成具有功能等效性的设计实例。
- DARPA的方法建立在之前的正式方法工作基础上，以改善网络安全。