Integrating Threat Analysis and Formal Verification for Secure OTA Updates

The automotive industry increasingly relies on Over-the-Air (OTA) updates to deliver essential security patches to vehicles. However, this dependence may introduce significant cy-bersecurity vulnerabilities, particularly concerning the integrity and privacy of updates. This paper presents an integrated framework that combines threat modeling and formal verification by employing an identical system model across all stages. The process begins with applying the ThreatGet tool to identify potential threats in the OTA update process, which directly guide the formulation of formal security requirements expressed as Computation Tree Logic (CTL) properties. The same high-level model encompassing a Cloud Server (CS), Telematics Control Unit (TCU), Central Gateway Unit (CGU), Advanced Driver Assistance System (ADAS) module, and an attacker module is consistently used for both threat modeling and encoding in the NuSMV model checker. This unified approach ensures that identified threats translate seamlessly into verifiable properties. Experimental threat analysis and verification results demonstrate the effectiveness of our integrated approach in uncovering OTA update vulnerabilities properties.