黑客已经抢得了一个先机:他们已能访问无人机的部分计算机系统,他们所需要做的是入侵无人机的机载飞行控制计算机,然后无人机就是他们的了。

在美国国防部高级研究计划署(DARPA)发起的这个项目的早期,“红队”黑客们就像入侵你的家庭无线网络那样轻而易举的控制无人机。但随后的几个月,DARPA 的工程师实现了一种新的安全机制——一种无法用现有技术破解的软件系统。它的代码就像数学证明那样可靠。即使给予红队六周的时间访问无人机及其网络系统,他们仍然无法破解其防御。DARPA 准备将这项技术应用于更多的领域。挫败黑客们的编程技术叫形式化验证,今天的大部分程序代码都是非形式化的,对其的评估主要是基于它是否能工作。形式化验证代码读起来就像是数学证明。整个程序的测试具有与数学家作证明同等的确定性。

2015 年夏天,一组黑客尝试控制一架军用无人直升机。

8 收藏


直接登录
最新评论
  • 龙雀 野生程序员 2016/09/23

    代码在你手里就不用找漏洞破解了,直接逆向分析就行了。无人机显然属于后者。

  • dam githuber,自由职业人 2016/09/23

    认识一些人是做这方面的研究工作的,不过我也不太了解,应该是COQ方面的

推荐关注