声明：以下内容编译自互联网，不代表本公众号的观点，如有侵权，请联系删除。
项目背景
据国防高级研究计划局称，这些尖端武器似乎受到“普遍脆弱性”的影响，这使它们面临被劫持的具体风险。“普遍脆弱性”的概念被广泛讨论并成为深入研究的主题，该弱点还影响SCADA系统、车辆、医疗设备、计算机外围设备和通信设备。
此类漏洞的补丁管理，尤其是在军事领域，非常复杂，修复 UAC 控制系统中存在的错误在大多数情况下需要对整个飞机进行重新认证。一个补丁需要一系列的测试，以避免在系统中引入更多的漏洞修复。
塔夫茨大学科学家兼 DARPA 项目经理 Kathleen Fisher 博士确信问题与控制算法的设计有关，该算法的编写方式似乎从根本上是不安全的。费舍尔正在开展一个名为高保障网络军事系统或HACMS的项目，该项目历时四年，预计耗资 6000 万美元，目的是定义一种创新且安全的编码实践。
罗克韦尔柯林斯正在领导一项由国防高级项目研究局 (DARPA) 资助的研究计划，该计划正在取得重大进展，产生旨在防止飞机网络安全攻击的技术和概念。使用无人驾驶飞行器 (UAV) 作为研究平台，高保障网络军事系统 (HACMS) 计划证明正式方法方法可以帮助开发旨在防止黑客访问关键飞行控制和其他机载航空电子系统的软件。
HACMS 由 DARPA 于 2012 年推出，其目标是创建旨在使用基于形式方法的软件和硬件开发方法构建高可靠性网络物理系统的技术。罗克韦尔柯林斯是飞行器团队的主要承包商，与波音公司、澳大利亚数据创新集团 Data 61、明尼苏达大学 (UMN) 和位于俄勒冈州波特兰的研究公司 Galois 合作。据 DARPA 称，该计划的目标是，是生成开源的、高可靠性的操作系统和控制系统组件，以构建高可靠性的军用网络飞机平台，同时还将其技术转移到国防和商业领域。
虽然 HACMS 飞行器团队正在使用小型四轴飞行器遥控飞机 (RPA) 进行研究，但总体目标是能够将这些技术和概念转变为全尺寸载客飞机，罗克韦尔柯林斯大学高级研究员 Darren Cofer技术中心和 DARPA HACMS 项目飞行器团队的成员，告诉航空电子杂志。为了复制大型客机和具有超视距 (BLOS) 能力的无人机的结构，HACMS 团队对其四轴飞行器进行了修改，以配备机载网络、飞行控制计算机和能够向飞行控制计算机发送命令的任务计算机管理外部数据链路，同时对数据链路进行加密和解密，并托管其他有效载荷功能，例如监控摄像头。
HACMS：高保障网络军事系统
无人机和其他军用飞机具有用于指挥和控制、共享传感器数据以及与其他部队协调的车外网络连接。这种连接提供了巨大的新功能，但也使这些军事资产面临与困扰我们的 PC 和 Web 服务器相同的安全风险。
安全性是系统的紧急属性。这意味着系统中没有提供安全性的特殊盒子。我们必须查看整个系统以及它的组件如何相互交互和与外部世界交互。漏洞可能来自“前门”（网络协议）、组件错误（软件错误）或其他正确组件之间的意外交互。
当前的网络安全方法依赖于在发现漏洞后修补系统。我们需要一种全新的、基于数学的方法来构建安全软件。DARPA 发起了HACMS 计划（高保障网络军事系统），以开发应对网络嵌入式系统的网络威胁所需的技术。
Rockwell Collins 正在领导 DARPA HACMS 计划中的安全数学保证控制模型组合 (SMACCM) 项目。SMACCM 项目正在开发用于构建无人机软件的新工具，该软件可证明可以抵御多种类型的网络攻击。我们的目标不仅是提供安全性，而且是提供可验证的安全性；也就是说，我们可以对其安全性有信心和证据的系统设计。我们正在开发系统架构模型、任务和控制功能的软件组件以及操作系统软件，所有这些都经过数学分析以确保关键的安全属性。
我们的方法的独特方面包括：
证明与软件工程的整合
正式验证的操作系统软件
基于形式化设计语言和综合的高保证控制组件
我们正在研究型四轴飞行器上对这些新技术进行原型设计，然后将它们转移到波音公司的无人小鸟 (ULB) 直升机上，以证明其实用性和有效性。我们用于建筑建模、分析和综合的集成工具（如图所示）使这种方法实用且有效。这些用于安全软件开发和分析的工具可用于过渡到其他车辆程序（同意和坚决）。
在项目的每个阶段结束时，HACMS 红队都有六周的时间，可以完全访问两辆车的源代码，以评估他们的网络安全声明。他们无法危及任何一辆车的安全。
作为该项目的一部分开发的所有模型、软件和工具都是开源的，可在SMACCM github 存储库中找到。有关研究型四轴飞行器构造的详细信息，请访问smaccmpilot.org。项目最终报告中提供了更多信息。
第 3 阶段最终演示，包括对研究型四轴飞行器的网络攻击和有关波音 ULB 最终演示的视频。
整个项目将持续 4.5 年，分为三个 18 个月的阶段，由 5 个技术领域 (TA) 组成
TA1 – 军用车辆专家
TA2 – OS 组件的形式化方法和综合
TA3 – 控制系统的形式化方法和综合
TA4 – 研究整合
子领域 1：形式方法工作台
子领域 2：高可靠性组件的集成
TA5 – 红队
政府对军事领域的工具和基于形式方法的技术的定义感兴趣，以开发用于创建安全防御车辆的安全控制算法。最终的控制算法将在罗克韦尔柯林斯无人机、波音直升机和 Black-I-Robotics 地面机器人等各种防御车辆上进行测试，但该项目更为雄心勃勃，它的最终目标是定义“一个可以在附近写字的软件”。- 完美的代码本身”。
阅读 HACMS 程序的介绍时，我被技术领域 5：红队（“进攻之声”）所吸引，其中包括目标车辆的静态和动态评估安全性。该阶段还包括基于在系统中注入任意代码和向车辆传感器提供虚假值的攻击的特定任务。这些是迄今为止观察到的最危险的攻击类型，该程序还希望保护任务目标免受黑客攻击，黑客攻击可能会在冲突期间泄露敏感信息，例如任务目标（例如侦察或轰炸）、部队的位置在袭击的领土和最终目标上。
HACMS 的交付物将是一套集成到高保证框架中的公开可用工具，将分发用于军事和商业软件领域，目的是促进这些工具生成、高保证和开放-源操作系统和控制系统组件。
如果该项目成功，它可能代表历史的一个转折点，我们将能够设计出不受黑客攻击的无人机，我们非常接近于创造出完美的机器
相关成果
Galois 构建了两种新的领域特定语言 (DSL)，并使用它们开发了一个“防黑客”、功能齐全的无人驾驶航空系统。我们提高生产力和保证的秘诀是构建嵌入式 DSL，其中 DSL 是 Haskell 中的库。我们从相对较小的规范中生成保证内存安全的嵌入式 C 代码。
作为 DARPA 高保障网络军事系统 (HACMS) 的一部分，Galois 正在使用用于嵌入式系统编程的新软件方法构建关键的飞行控制软件。我们于 2014 年 5 月 21 日在五角大楼举行的DARPA I2O 演示日展示了迄今为止根据该计划开发的技术。在最近发表在 Signal Online 上的这篇文章中阅读有关该计划以及我们团队正在做什么的更多信息。
我们在 HACMS 计划下开发的技术的旗舰应用称为 SMACCMPilot：一种用于小型四旋翼 无人机 (UAV)的新型飞行控制器 。SMACCMPilot 是用象牙语言编写的， 象牙语言是一种用于安全系统编程的新的特定领域语言。我们在 Ivory 语言之上构建了一个库生态系统，包括并发框架和微控制器硬件驱动程序。Ivory 有一个简单的外部 C 代码接口，允许 SMACCMPilot 重用来自ArduCopter 开源项目的软件组件 。
我们还在 Ivory 中实现了通信协议栈和控制原语。SMACCMPilot 目前是 alpha 质量的软件，因为我们积极开发飞行控制软件本身并发展我们用来构建它的新技术。在接下来的几年里，我们将继续致力于 SMACCMPilot 项目。
SMACCMPilot 背后的所有软件都是开源的， 可在 github 上获得，并记录在 项目网站上。我们欢迎与编程语言、形式方法和飞行控制研究人员的合作！
消息来源：
1.http://loonwerks.com/projects/hacms.html
2.http://securityaffairs.co/wordpress/11456/security/darpa-hacms-program-for-a-software-without-pervasive-vulnerability.html
3.https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597724/
4.https://galois.com/project/hacms-high-assurance-cyber-military-systems/
5.http://www.cyber.umd.edu/sites/default/files/documents/symposium/fisher-HACMS-MD.pdf
6.https://www.aviationtoday.com/2016/05/17/darpa-program-makes-progress-with-aircraft-cyber-security-research/
声明：本文来自网络安全风云榜，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
