编者按
美国国防部高级研究计划局（DARPA）信息处理技术办公室于11月3日发布“系统异构性形式化学习与抽象”（FLASH）项目信息征询通知，向业界和研究人员征询如何自动生成同一军事系统的多个结构各异但均经数学证明能够完成相同任务的不同版本，从而使其中一个版本遭攻击或出现故障时不影响其他版本。
DARPA正在探索将基于生成模型的代理与符号推理技术相结合的新颖方法论，以形式化方式表征设计意图，快速高效地综合构建语义异构的网络物理工程系统，并生成设计与保障辅助资料。FLASH项目探索将高层系统需求与具体实例层面的设计细节进行系统性解耦，从而达到通过异构性来实现系统的稳健性；所生成的系统实例在故障模式和攻击面方面可呈现出显著差异但仍能保持预定的系统属性，从而削弱针对特定系统实例的敌对发现的持久性和可迁移性，如已发现的漏洞、配置信息或常见故障模式；通过同步生成用于系统保障和理解的设计辅助资料，可提供证明系统的正确性、异构性和韧性均可通过形式化方法进行评估的证据，而非仅仅依赖经验性的评估手段。项目三大关键技术方向包括：一是对系统需求、运行意图及语义不变量进行形式化定义并明确有效设计自由度；二是开发在确保功能等效性和形式化正确性前提下生成不同设计实例的模型与技术；三是开发跨设计实例共同生成保障与解释工件，并构建可复用领域特定工程知识形式化表述的技术。
DARPA邀请各方就两组问题提供响应信息。一是识别并界定FLASH技术有望带来变革性作战优势的特定国家安全应用场景及运行环境，如自主战术平台、安全通信链路、工业控制系统、自主机器人集群、高性能计算集群、边缘计算网络、网络安全应用等。具体回复应涵盖以下内容：运行域与目标应用的精确界定；充分的国家安全理由及威胁环境；当前保护或加固此类系统的技术水平及其根本局限与潜在故障点；“动态异构性”和FLASH技术方向如何缓解现有防御手段未能充分解决的漏洞、共模故障或攻击路径；各备选方案中必须保持不变的功能、安全、防护、时序、互操作性和性能属性及可用设计自由度。二是描述实现FLASH愿景的技术框架、架构和评估标准。具体回复应涵盖以下内容：异构性指标、验证功能等价性及其他不变系统属性的方法、评估适应性韧性的实验（包括使用智能代理的自主利用开发）；结构约束的归纳和演绎方法，如预言引导的归纳合成、生成式多模态基础模型与交互式定理证明器相结合；适合系统设计和理解的单代理与多代理架构；针对特定应用领域的形式化规范、模型和证明的可重用库。
DARPA的构想可追溯至1977年N版本编程设想，以及1986年检验该假设后发现相关故障概率远高于独立性预测、从而引发对设计多样性质疑的实验。FLASH与N版本编程的不同在于：不依赖独立人工团队和统计独立性，而是寻求通用形式化规范、自动生成变体及机器验证证明以确保每个变体满足相同属性。该信息征询也建立在DARPA自身形式化方法研究基础上：2017年结束的“高可靠性网络军事系统”（HACMS）项目中，红队最初远程控制四旋翼飞行器和波音“小鸟”无人直升机，但在工程师用形式化方法重建关键软件后，同一团队在长达六周完全系统访问权限测试中未能攻破系统；DARPA后来将该工具应用于卫星和自动驾驶卡车，并于2025年起与美国空军合作通过“弹性软件系统顶点项目”将形式化方法工具引入MQ-9“死神”无人机。
奇安网情局编译有关情况，供读者参考。
美国国防部高级研究计划局正在向业界和研究人员征询如何自动生成同一军事系统的多个不同版本。每个版本都经过数学证明能够完成相同的任务，但其结构各不相同，因此即使其中一个版本遭到攻击或出现故障，也不会影响其他版本。DARPA信息处理技术办公室2026年11月3日发布一项信息征询，内容涵盖名为“系统异构性形式化学习与抽象”（Formal Learning and Abstractions for System Heterogeneity，FLASH）的项目，回复截止日期为美国东部时间2026年11月30日17时。
此份编号为DARPA-SN-27-17的通知属于市场调研，而非招标公告。DARPA尚未公布任何后续项目、预算或时间表。该机构表示，将弃置针对此次征集所提交的任何摘要或提案，且不会为相关回复支付费用。
项目背景
DARPA正在探索一种新颖的方法论：将基于生成模型的代理与符号推理技术相结合，从而以形式化方式表征设计意图，同时快速、高效地综合构建语义异构的网络物理工程系统，并生成相应的设计与保障辅助资料，以辅助对系统的理解。通过将高层系统需求与具体实例层面的设计细节进行系统性解耦，FLASH框架旨在通过异构性来实现系统的稳健性。在此范式下，所生成的系统实例在故障模式和攻击面方面可呈现出显著差异，同时仍能保持预定的系统属性。利用这种差异性，可以削弱针对特定系统实例的敌对发现（如已发现的漏洞、配置信息或常见故障模式）的持久性和可迁移性。通过同步生成用于系统保障和理解的设计辅助资料，该框架能够提供证据，证明系统的正确性、异构性和韧性均可通过形式化方法进行评估，而非仅仅依赖经验性的评估手段。
FLASH项目的关键技术方向包括：
对系统需求、运行意图及语义不变量进行形式化定义，同时明确有效的设计自由度，从而支持多种异构方案的选择；
开发相关模型与技术，在确保功能等效性和形式化正确性的前提下，生成不同的系统设计实例；
开发能够跨不同设计实例共同生成保障与解释工件，并构建出可复用的领域特定工程知识形式化表述的技术。
所需信息
DARPA诚邀各方识别并界定特定的国家安全应用场景及运行环境（例如：自主战术平台、安全通信链路、工业控制系统、自主机器人集群、高性能计算集群、边缘计算网络、网络安全应用等），在这些领域中，FLASH技术有望带来变革性的作战优势。回复内容应涵盖以下方面：
对运行域（operational domain）和目标应用的精确定义；
充分的国家安全理由及所处的威胁环境；
当前在保护或加固此类系统方面的技术水平，并指出其根本局限性及潜在的故障点；
“动态异构性”和FLASH技术方向如何缓解现有防御手段未能充分解决的漏洞、共模故障或攻击路径（包括关键假设、局限性及拟议的评估方法）；
在生成的各种备选方案中必须保持不变的功能、安全、防护、时序、互操作性和性能属性，以及可用的设计自由度。
DARPA邀请响应者描述能够实现FLASH愿景的技术框架、架构和评估标准。回应内容应涉及：
异构性指标、验证功能等价性和其他不变系统属性的方法以及评估适应性韧性的实验（包括使用智能代理的自主利用开发）；
结构约束的归纳和演绎方法，例如预言引导的归纳合成以及将生成式多模态基础模型与交互式定理证明器相结合进行设计；
适合系统设计和理解的单代理和多代理架构；
针对特定应用领域的形式化规范、模型和证明的可重用库。
突破思路
1977年，陈立明（Liming Chen）和阿尔吉尔达斯·阿维齐尼斯提出了N版本编程，即由不同的团队根据同一规范编写不同的程序，然后由投票者比较它们的输出结果。他们的假设是，独立开发的软件会各自独立地出现故障。1986年，约翰·奈特和南希·莱维森用两所大学独立编写的同一程序的27个版本，运行了一百万个测试用例，检验了这一假设。结果发现，这些版本同时出现故障的概率远高于独立性所预测的概率。约翰·奈特和南希·莱维森的研究得出结论：对多版本软件的分析必须考虑相关错误，这一结果从此引发了人们对设计多样性的质疑。
FLASH与N版本编程的不同之处在于其寻求保障的方面。DARPA不依赖于独立的人工团队和统计独立性，而是寻求一个通用的形式化规范、自动生成的变体以及机器验证的证明，以确保每个变体都满足相同的属性。该信息征询并未说明DARPA将如何衡量生成的变体是否足够多样化，从而避免1986年实验中发现的相关性故障，因此要求响应者提出异构性指标。
该信息征询也建立在DARPA自身形式化方法研究的基础上。在2017年结束的“高可靠性网络军事系统”（HACMS）项目中，红队最初远程控制了一架四旋翼飞行器和波音公司的“小鸟”无人直升机。但在工程师使用形式化方法重建关键软件后，同一团队在长达六周的完全系统访问权限测试中（包括一次载有两名飞行员的飞行测试）未能攻破系统。DARPA后来将该项目的工具应用于卫星和自动驾驶车队卡车，并于2025年开始与美国空军合作，通过其“弹性软件系统顶点项目”将形式化方法工具引入MQ-9“死神”无人机。
FLASH是自DARPA于2026年5月恢复信息处理技术办公室（IPTO）名称以来，该办公室推出的首批重点项目之一。该办公室前身为信息创新办公室（Information Innovation Office），后重新启用原IPTO的名称。IPTO曾在20世纪60年代由约瑟夫·利克莱德领导，为ARPANET和早期交互式计算提供资金，并于2010年并入信息创新办公室。IPTO主任帕特里克·林肯表示，更名后的办公室将专注于复杂系统的韧性和理解，以及网络安全和隐私保护。
声明：本文来自奇安网情局，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
