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

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.