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

The paradigm communicate with anyone anywhere at anytime nowadays spans to cyberphysical 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 vehicletoeverything (V2X). Different sensors and processing units inside connected cars communicate and synchronize using different types of intravehicle protocols. In addition to invehicle communication, connected cars communicate and interact with their environment, using socalled intervehicle protocols. Because of significant advancements in V2X technology, security issues related to them are on the rise. The securitybydesign 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 securitybydesign 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.