面向安全车辆软件更新的形式化验证

随着软件定义车辆 (SDV) 的兴起，软件几乎控制车辆的大部分功能，并实现了增强的连接性，安全软件更新的需求变得越来越关键。软件漏洞可能严重影响安全、经济和社会。为了应对这一挑战，Strandberg 等人 [escar Europe, 2021] 引入了统一软件更新框架 (UniSUF)，旨在提供与现有车辆基础设施无缝集成的安全更新框架。尽管 UniSUF 之前就网络安全问题进行了评估，但这些评估未采用形式化验证方法。为弥合这一差距，我们对 UniSUF 进行形式化安全分析。我们建模 UniSUF 的体系结构和假设，以反映真实世界的汽车系统，并开发了基于 ProVerif 的框架，对 UniSUF 符合基本安全要求的合规性进行形式化验证——包括机密性、完整性、真实性、新鲜性、顺序性和存活性，通过符号执行 demonstrating their satisfiability。我们的结果表明，UniSUF 符合指定的安全保证，确保其安全框架的正确性和可靠性。