An Approach to Formal Verification of Autonomous Vehicle Systems using Threat Analysis

The rapid advancement and deployment of connected and autonomous vehicles (CAVs) present transformative opportunities to enhance safety, efficiency, and convenience within the transportation industry. However, these innovations introduce significant cybersecurity risks due to the complex electronics and continuous connectivity that CAVs depend on. Traditional testing methods, while critical, often fall short in detecting vulnerabilities across the vast range of scenarios these vehicles may encounter. Formal verification, a mathematical approach to system validation, offers a more rigorous and comprehensive solution by ensuring that systems operate as expected to search through all possible execution paths. However, defining appropriate system properties for verification remains a challenge, as a system designer may write properties that fail to address real-world threats effectively. This research addresses this gap by integrating threat analysis into the process of defining security properties, ensuring that the verification process is aligned with actual cybersecurity risks. We leverage Natural Language Processing (NLP) to extract key security details from threat analysis result texts, automating the generation of system properties. This approach simplifies the verification process, with its usability demonstrated through a high-level 5G-V2X design use case scenario.