Formal Modeling: A Step Forward to Cyber Secure Connected Car Systems

Publication from Digital
Forschungsgruppe Cyber Security and Defence

Branka Stojanovic, Katharina Hofer-Schmitz, Heribert Vallant, Christian Derler, Kai Nahrgang

In: Hamid U.Z.A., Al-Turjman F. (eds) Towards Connected and Autonomous Vehicle Highways. EAI/Springer Innovations in Communication and Computing. Springer, Cham., 6/2021


The paradigm communicate with anyone anywhere at anytime nowadays spans to cyber-physical systems in general including automotive industry. The established path and goal for the automotive industry include connected cars and various services, like autonomous driving. Communication technologies used with connected cars fall into one umbrella, called vehicle-to-everything (V2X). Different sensors and processing units inside connected cars communicate and synchronize using different types of intra-vehicle protocols. In addition to in-vehicle communication, connected cars communicate and interact with their environment, using so-called inter-vehicle protocols. Because of significant advancements in V2X technology, security issues related to them are on the rise. The security-by-design frameworks, including threat modeling and formal methods, have the potential and means to answer these challenges. This chapter contains a comprehensive, security focused, overview of the connected cars’ communication architecture and the most important protocols. Then it discusses security-by-design frameworks application within this domain – threat modeling state of the art methodologies and the ability to adapt those for the automotive industry, and formal verification tools and their applications in V2X protocols space. Furthermore, challenges and future research directions are discussed.

Keywords: Connected cars, security, automotive protocols, security-by-design, threat modeling, formal verification, model checkers