美国国防高级研究计划局(DARPA)的网络保证系统工程（CASE，Cyber Assured Systems Engineering）项目，从系统工程的角度解决网络安全问题，旨在开发一系列设计、分析和验证工具，研究网络安全技术如何以广泛、可拓展的方式进行应用，确保网络弹性在嵌入式计算系统的每个阶段都发挥关键作用。网络弹性也将成为每个防御平台的核心属性，并与其他非功能性属性结合。
一、简介
CASE项目启动于2018年，预计持续四年，共分为三个阶段。第二阶段侧重于技术增强和对新型工具的测试。其中，2020年4月，美通用电气公司的技术开发部门（GE Research）公布了其正在研发的一种网络安全工具VERDICT（Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats，网络安全威胁预测的验证证据和弹性设计），融合多种现有安全工程和网络安全指标，可对网络安全威胁进行全面评估、提出漏洞处置建议、预测未来网络攻击发生的可能性，为美国关键军事及工业系统网络提供安全防护保障；可用于检查并改进DARPA项目的关键军事和工业系统的网络状况和防御能力，为系统提供对网络威胁的全面评估，建议如何解决暴露的漏洞，并预测即将发生的攻击的可能性。VERDICT的特别之处在于其将Mitre的常见攻击模式枚举和分类以及NIST 800-53中的安全和隐私控制列表机器化。
二、项目详细内容
1、部分参与方
DARPA的网络保证系统工程 (CASE)项目的目标是开发必要的设计、分析和验证工具，以允许系统工程师在设计复杂的嵌入式计算系统时设计网络弹性和管理权衡。网络弹性意味着系统能够容忍网络攻击，就像安全关键系统能够容忍随机故障一样，它们可以恢复并继续执行其任务功能。
Collins Aerospace、Adventium、新南威尔士大学（悉尼）、堪萨斯大学等联手为CASE计划的设计弹性和工具集成目标提供全面的解决方案，开发了一个称为 Brief CASE的基于模型的系统工程环境，允许工程师通过组合分析来处理一系列属性并管理系统复杂性，在设计过程的各个级别集成形式方法。工具基于架构分析和设计语言(AADL)，并扩展了开源AADL工具环境 (OSATE)。
BriefCASE 工具和方法的主要创新是：提供自动化架构设计模式来满足网络弹性要求，包括从正式规范中综合高保证组件；MBSE环境可以针对不同的操作系统，包括 seL4微内核，从而使开发人员可以轻松访问其正式的安全保证。这确保了生成的实现忠实于建模系统；方法基于系统设计和保证工件的共同演化，因此设计更改会自动更新相关的认证证据。保证案例嵌入在架构模型中，以捕获和记录设计决策以及相关的基本原理；形式化方法集成在整个工作流程中，包括需求捕获、组件合成、验证、代码生成和seL4微内核。
在 CASE项目上开发的工具是开源的，可以在GitHub上找到。包括：AADL建模和分析工具；适用于Windows的安装脚本；Linux安装脚本；用于配置虚拟机的Vagrant脚本，包含建模/分析工具和面向seL4的构建环境；BriefCASE工具的用户指南。
2、CASE项目的时间线
第1阶段包括初步研究和工具开发。
第2阶段包括在一个或多个实验平台上对新兴工具进行技术改进和测试。
在第3阶段，CASE 工具将用于重新设计一个选定的代表性演示，以展示网络弹性的真实系统。
3、AADL 网络弹性建模和分析工具：GE VERDICT / DARPA CASE
2021年2月，一次业内论坛上披露，由GE Research领导的一个团队，包括GE Aviation Systems和爱荷华大学，在DARPA网络保证系统工程 (CASE)项目上创建了一个基于AADL的工具。该工具被命名为VERDICT。VERDICT使系统工程师能够基于AADL架构模型和任务场景进行建模、联合分析安全和安保，生成故障和攻击/防御树，然后综合满足所有设计约束的架构。
有资料称，VERDICT是一个在架构级别执行系统分析的框架。它由两个主要功能组成：基于模型的架构分析和综合 (MBAAS) 和网络弹性验证 (CRV)。VERDICT用户首先使用AADL捕获架构模型，该模型代表系统的高级功能组件以及它们之间的数据流；然后使用VERDICT属性、关系和分析要求对模型进行注释。VERDICT MBAA后端工具将分析架构识别网络漏洞并推荐防御措施。用户还可以使用 VERDICT MBAS功能来综合一组最小的防御措施，以降低其实施成本。VERDICT还支持使用AGREE使用行为建模信息对架构模型进行细化。VERDICT CRV后端工具针对正式网络属性对更新模型进行正式分析，以识别网络威胁影响的漏洞。这种有价值的功能提供了模型分析的额外深度，包括架构组件模型的行为细节，这将有助于在开发过程的早期发现设计错误。
主要特点包括：
基于模型的架构分析与综合(MBAAS)
识别 CAPEC 威胁和推荐NIST 800-53控制；顶级事件攻击成功概率的判定；系统故障概率的计算；生成割集、故障树和攻防树；综合一套最小的防御措施，以减轻与实施成本有关的所有网络要求；使用现有实施的防御以两种模式合成一组最小的防御以缓解所有网络要求：缓解和未缓解（缓解模式：MBAS 建议消除无关的防御并降低防御设计保证水平（DAL）；无缓解模式：MBAS建议对防御DAL进行新的实施和升级）。
网络弹性验证 (CRV)
网络弹性属性的证明：功绩分配
网络弹性属性的反证
过失赋值。
三、外媒相关报道
外媒曾报道称，VERDICT工具旨在让系统工程师即使没有深厚的专业知识也能评估网络安全。2020年4月，通用电气公司的技术开发部门GE Research公布了它正在开发一种网络安全工具VERDICT，以检查并随后改进关键军事和工业系统的网络地位和DARPA项目的防御。
VERDICT工具旨在跨一系列计算机系统工作，例如用于智能设备、船舶、飞机、发电厂和风电场的计算机系统。目标是为系统提供对网络威胁的全面评估，建议如何解决发现的漏洞，并预测即将发生的攻击的可能性。
GE Research项目团队成员称：“我们希望VERDICT是任何系统工程师都可以选择和使用的工具，无论有没有深厚的网络安全专业知识。”“最好的情况是，如果我们可以减少产品安全专家完成工作所花费的时间和精力，使他们能够分析和评估系统的安全性，并获得准确和可重复的结果。”
该项目正在通过DARPA的CASE项目运行，该项目从系统工程的角度解决网络安全问题。GE Research希望开发一种工具来帮助系统工程师评估网络弹性——抵御攻击的能力——就像他们评估安全或性能特性一样。
该项目于2018年启动，但官员们指出，其中一些概念是对以前项目的扩展，以新的形式出现。“例如，生成后端攻击防御树的基于模型的框架是对先前与NASA Langley研究中心所做工作的扩展，该工作为基于模型的框架生成故障树以分析安全性。”
据该团队称，VERDICT之所以与众不同，部分原因在于它旨在机械化Mitre的常见攻击模式枚举和分类以及NIST 800-53 中的安全和隐私控制列表。该团队表示，这两个项目都需要花费大量时间和精力来提炼到所需的内容。“因为我们从一开始就在我们的开发团队中包括了一名安全从业人员，所以我们始终以适用于现实世界问题和使用的原则为指导，同时，该工具以严谨的分析方法为后盾，由开发团队中的形式方法和语义专家构建。”
VERDICT旨在改进的许多电力系统与云分开运行，以降低网络攻击的风险——但它们仍然面临威胁。与此同时，国防部和其他相关政府实体正在采用越来越多的商用现成物品，这加剧了严格检查和跟踪网络漏洞的必要性。此外，研究人员补充说，最近，攻击这些关键系统的尝试“在本质上变得更加复杂”。
（来源：综合外网外媒等。本文参考内容均来源于网络，仅供读者了解和掌握相关情况参考，不用于任何商业用途。侵删）
热门跟贴