美国DARPA无人机系统安全设计

2015年，在计划实施前，一批黑客奉命对美国军方Little Bird无人直升机发动电子攻击，并掌握无人机控制权的事件中。黑客最初的攻击十分顺利，攻入了UAV，截获控制权，并借此攻破UAV操作员的电脑。然而，当DARPA重新开发了该无人机的核心控制程序后，即使是给黑客提供了源码和系统文档，黑客在长达6个星期的时间内使用了世界上所有的攻击手段，也未能攻破新部署的系统。

到底是什么技术给予了Little Bird超强的防御能力，从而使它阻挡了所有的攻击？答案就是：形式化验证方法。DARPA而在采用“形式化验证”后，全面采用逻辑/推理，系统设计/开发/验证，获得了坚不可攻的防御能力。

目前，美国DARPA已将此方法开始应用于无人驾驶飞机（Unmanned Aerial Vehicle）技术中。这类方法可能成为安全领域的“反导武器”。