利用软件验证发现无人机的安全漏洞

嵌入了脆弱单体软件的无人机（UAV）的激增，最近因其并发性方面和脆弱的通信链路而引发了对其安全性的严重关切。然而，基于传统测试来验证无人机软件的安全性仍然是一个开放的挑战，这主要源于可扩展性和部署问题。在此，我们研究软件验证技术以检测典型无人机中的安全漏洞。特别是，我们调研了现有的软件分析器和验证器，它们实现了模糊测试（fuzzing）和有界模型检测（BMC）技术，用以检测内存安全和并发错误。我们还研究了与无人机通信链路相关的脆弱性方面。所有无人机组件（例如，位置、速度和姿态控制）都严重依赖于通信链路。我们的初步结果表明，模糊测试和BMC技术能够检测到各种软件漏洞，这对于确保无人机的安全性具有特别的意义。我们能够通过渗透测试对无人机的连接和软件系统成功实施网络攻击。由此，我们展示了真实的网络威胁，并预示着在可预见的未来，利用现实世界无人机软件中更多安全漏洞的可能性。