编者按
在近日美国DEF CON网络安全大会上，美国防高级研究计划局（DARPA）邀请黑客入侵其研发的无人机网络安全软件，结果显示该软件是无法破解的，即使对专业人士也是如此。
该软件名为“高保障网络军事系统”（HACMS），其演示工作于2017年结束，但这是DARPA首次邀请黑客尝试破解它。HACMS使用了“形式化方法”技术，在数学上确保不存在让黑客侵入并接管计算机系统的软件缺陷。该软件架构严格地分离了任务控制系统的不同功能，即使黑客能够入侵无人机的摄像机软件，但仍然无法劫持其指挥控制系统。
DARPA表示，随着软件变得越来越复杂，传统的网络安全保证基线技术变得越来越耗时，效率也越来越低，对网络安全的日益关注将增加对“形式化方法”大规模应用的需求。波音公司已在其“无人小鸟”（Unmanned Little Bird）自主直升机项目中使用了HACMS。
奇安网情局编译有关情况，供读者参考。
美国国防高级研究计划局（DARPA）对其为遥控四轴飞行器开发的防黑客软件非常有信心，以至于在最近的DEF CON网络安全大会上邀请黑客试图侵入并接管它。
DARPA信息创新办公室项目经理雷·理查兹表示，无人获得成功。理查兹表示，DARPA的“高保障网络军事系统”（HACMS）演示工作于2017年结束，但这是DARPA首次邀请所有来者尝试破解它。
8月6日，拉斯维加斯，DEF CON航空航天村一个视频演示展示了用于飞行控制的传统软件架构的脆弱性和HACMS等高保障软件技术的价值。在视频中，一支红队黑客利用摄像机中未修补的软件漏洞侵入了四轴飞行器的任务控制系统。一旦进入摄像机，黑客就能够重写保护四轴飞行器与其地面基地的指挥控制通信加密密钥，戏剧性地劫持飞行器并将其飞回自己的基地。
DARPA承包商柯林斯航空航天公司说明传统软件架构的弱点
但是使用一种称为“形式化方法”的技术，HACMS软件在数学上确保不存在让黑客侵入并接管计算机系统的软件缺陷。波音公司在其“无人小鸟”（Unmanned Little Bird）自主直升机项目中使用了HACMS。
事实证明，用于四轴飞行器的“形式化方法”构建软件是无法破解的，即使对DEF CON上的专业人士也是如此，因为该架构严格地分离了任务控制系统的不同功能。尽管仍然有可能侵入摄像机软件，但“转向”黑客经常依赖的指挥控制是不可能发生的。
不过，为了以防万一——并且根据飞行安全规定——DARPA让黑客在DEF CON航空航天村入侵的四轴飞行器是无法飞行的。
来自DARPA承包商柯林斯航空航天公司的达伦·科弗在演示中解释称，黑客可以用摄像机做任何他们想做的事情。他表示，“他们可以做任何事情——例如让摄像机软件崩溃或让四轴飞行器的虚拟机崩溃——并且四轴飞行器能够继续飞行，而不会影响合法地面站的指挥控制。”他补充称，事实上，地面控制器可以远程重启虚拟机本身，以重新控制摄像机。
DARPA技术人员正在准备一架HACMS保护的四轴飞行器
“形式化方法”作为一种软件保证技术于1973年首次提出，但长期以来一直被广泛认为过于昂贵和费力。但雷·理查兹表示现在情况不是这样了。计算机协会（ACM）的期刊《ACM通信》7月报道称，谷歌和火狐都在其Web浏览器中安装了“形式化方法”验证的组件，Amazon Web Services（AWS）也在其关键云服务中的关键组件中采用了该技术。
雷·理查兹表示，随着软件变得越来越复杂，测试——传统上选择的网络安全保证基线技术——变得越来越耗时，效率越来越低。他称，“对网络安全的日益关注将增加对‘形式化方法’的大规模应用的需求。”
附：形式化方法，formal method，又称“形式方法”“正规方法”。在计算机科学和软件工程领域，“形式化方法”是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计，是期望能够像其他工程学科一样，使用适当的数学分析以提高设计的可靠性和强健性。
声明：本文来自奇安网情局，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
