Formalising UPTANE in CSP for Security Testing
Formalising UPTANE in CSP for Security Testing
复制标题
在 CSP 中正式化 UPTANE 以进行安全测试
DOI：
10.1109/qrs-c55045.2021.00124
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
David Price
中科院分区：
文献类型：
--
作者：
Rhys Kirk;N. H. Nga;J. Bryans;S. Shaikh;D. Evans;David Price
由于电子架构的复杂性和连接技术的逐步集成，现代车辆容易受到网络安全攻击。解决网络安全问题的一个很有前途的解决方案是无线（OTA）更新。最近，Uptane已经推出，目前被认为是汽车OTA系统解决方案的事实上的安全标准。为了确保Uptane系统能够提供更新以保护车辆，系统本身必须足够安全，以免本身成为攻击载体。为此，我们提出了一种基于模型的汽车OTA更新安全测试方法。这是通过对OTA更新系统和通信顺序进程（CSP）中的Dolev-Yao攻击者进行建模来实现的。可以验证组合模型以生成安全测试用例，并对Uptane系统上的攻击者提供全面的评估。
Modern vehicles are susceptible to cybersecurity attacks due to the complexity of their electronics architecture and a progressive integration of connectivity technologies. A promising solution to resolve cybersecurity issues is Over-The-Air (OTA) updates. Recently, Uptane has been introduced and is currently considered as the de facto security standard for automotive OTA system solutions. To ensure that a system, Uptane, can deliver updates to secure a vehicle, the system itself must be sufficiently secure as to not become an attack vector itself. To this end, we present a model-based security testing approach to OTA updates for automotive vehicles. This is done by modelling the OTA update system and the Dolev-Yao attackers in Communicating Sequential Processes (CSP). The combined models can be verified to generate security test cases and provide a comprehensive evaluation of attackers on the Uptane system.