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

Abstract

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.

1 Introduction

The paradigm communicate with anyone anywhere at anytime nowadays spans to cyber-physical systems in general and impacts many fields, including different types of industry (e.g., transportation, manufacturing, IT, etc.), health, and mobility [1]. An increase in connectivity demands, including a built-in connectivity, is reflected in a great deal by vehicle manufacturing industry. The established path and goal for automotive industry include connected cars and autonomous driving [2].

Existing and potential services in the connected cars industry should increase the road safety, bring more comfort to all passengers, and add more efficiency in traffic flows. Different sensors and services inside connected cars communicate and synchronize in order to enhance drivers’ experience and make processes smoother. In addition to in-vehicle communication, connected cars communicate and interact with their environment, including other vehicles, roadside users, and external infrastructure and devices and even share processing efforts between other entities.

An increase in vehicles’ connectivity demands influences in a great deal a rise of security issues. The security-by-design frameworks, including threat modeling and formal methods, have potential to respond to these challenges.

This chapter covers two main objectives – (i) a comprehensive overview of the connected cars’ communication architecture and most important communication protocols under the V2X umbrella, with a special focus on the security perspective and (ii) 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. Additionally, it discusses challenges and future research directions, as research and development path within this industry. In Fig. 1, an illustration of a security-by-design procedure for in-vehicle communication is presented as research guideline. It includes threat modeling and formal verification based on inputs from previous steps and standards/specifications and their redesign according to findings.

Fig. 1

Illustration of security-by-design framework within connected cars industry

The chapter is structured as follows: In Sect. 2, a basic introduction into the communication architecture and the protocols in use for connected cars is given. Section 3 focuses on threat modeling and describes different modeling methodologies and their possible applications, benefits, and limitations to model connected cars. Section 4 focuses on formal methods and describes used tools and considered protocols. In Sect. 5, key points are summarized, and open challenges for future work are stated.

2 Connected Cars Communication Architecture and Protocols

This section focuses on the communication architecture and most important automotive communication protocols from the security perspective.

The term vehicle-to-everything, commonly known by abbreviation V2X, encompasses all types of communications in the automotive domain, involving different types of communication entities, like vehicles, infrastructure units, motorcycles, cycles, pedestrians, etc. The heterogeneous connected car network consists of two main subnetworks [3] – intra-vehicle network, which covers a communication between in-vehicle devices, and inter-vehicle network, including the communication between the vehicle and surrounding.

2.1 Connected Car Network

Intelligent transportation system usually refers to the connected car system. It encompasses diverse entities and technologies, like vehicles, infrastructure units, and roadside users, and then data processing, communication and sensor technologies, etc. The heterogeneous network of such a system that connects different types of entities using different types of communication technologies consists of two main subnetworks [4]:

• Intra-vehicle network – covers a communication between in-vehicle devices, including controlling units, sensors, and actuators.

• Inter-vehicle network – commonly refers to the communication between vehicles; in this paper this term will be extended to all communication types among the vehicle and surrounding devices: on-board unit in-vehicle and external entities, like roadside users (pedestrian, motorcyclists, etc.), infrastructure units, and central processing units (central/cloud server).

V2X on the other hand supports a unified connectivity platform for all connected end points and allows road entities to transmit information such as their current speed, position, and direction to the neighboring entities. It includes both intra- and inter-vehicle networks and can be categorized in different types of communication (Fig. 2):

• In-vehicle communication – represents the communication between entities in intra-vehicle subnetwork;

  Fig. 2

  

  Connected vehicle communication illustration

• Vehicle-to-vehicle (V2V) – covers the communication between vehicles, for example, the vehicle can broadcast the message of a pedestrian crossing the road to other vehicles, or the vehicle learns of another vehicle ahead braking suddenly and communicates this alert with other vehicles.

• Vehicle-to-infrastructure (V2I) – represents the communication between road entities and infrastructure units, for example, the vehicle can communicate with the traffic lights to know the speed at which he can drive to get green at the next traffic light, etc.

• Vehicle-to-grid (V2G) – supports the communication between vehicles and the electric grid, for example, plug-in electric vehicles communicate with the power grid to sell services on a return basis either by returning electricity to the grid or by throttling their charging rate;

• Vehicle-to-pedestrian (V2P) – provides the connection between the vehicle and vulnerable road users (VRU), including pedestrians, cyclists, and motorized two-wheeler operators; a typical V2P crash prevention system involves periodic exchange of safety messages among vehicles and VRUs [5].

This book chapter focuses on the security and safety perspectives of the most important automotive communication protocols, including in-vehicle communication and V2V and V2I protocols, because they address safety applications that are crucial for a rapid, robust, and timely performance, where any delay in message delivery could lead to a potentially fatal collision. Safety applications include various warnings (e.g., red light violations, curve speeds, reduced speed/work zones, emergency electronic brake lights, forward collisions, etc.) that are sent from their place of occurrence, picked by the closest vehicle, and then further propagated to the surrounding vehicles.

2.2 Intra-vehicle Communication

The interaction between various sensors and controlling units inside the vehicle requires an information exchange using specific communication protocols [2, 6].

Intra-vehicle communication usually involves LIN (Local Interconnect Network), CAN (Controller Area Network), FlexRay, MOST (Media Oriented System Transport), LVSD (Low-voltage differential signaling), or Automotive Ethernet. An overview of intra-vehicle protocols is presented in Table 1.

Table 1 Intra-vehicle protocols

2.2.1 CAN: Controller Area Network

CAN [7] is a robust automotive-specific bus standard. It defines the functionality of the first two layers of the Open Systems Interconnection (OSI) network model – Layer-1 and Layer-2. CAN’s design allows communication between different devices inside vehicles, including microcontrollers, or ECUs (electronic control units) [6]. CAN was first developed and released in 1986 by Robert Bosch GmbH. I1991 is the year of production of the first vehicle featuring this protocol [8].

CAN standard ISO 11898 was released in 1993 by the ISO – International Organization for Standardization. It was later restructured into two parts, with a third part released afterward. The most recent versions of those parts of ISO 11898 standard are as follows: (i) ISO 11898-1:2015¹ covering the data link layer and physical signaling; (ii) ISO 11898-2:2016² covering CAN, high-speed medium access units; (iii) ISO 11898-3:2006³ covering CAN, the low-speed, fault-tolerant, medium-dependent interface.

Typical applications include the communication between ECUs controlling engine, power transmission, gearbox, antilock braking/ABS, electric power steering, etc. Beside passenger vehicles, it is used in trucks and buses, agricultural equipment, electronic equipment for aviation and navigation, building automation, medical equipment, industrial automation, etc. CAN bus is used in the on-board diagnostics (OBD)-II [9] vehicle diagnostics standard, as one of five supported protocols. CAN nodes are connected through a twisted pair bus, and data rates supported are up to 1 Mbps.

CAN is a low-level protocol and contains no direct support for security features. The implementations do not contain an encryption standard, and it leaves networks using CAN protocol open to cyber attacks, like man-in-the-middle frame interception and inserting messages on the bus. Security mechanisms are customized and usually implemented on the application and manufacturer level.

2.2.2 MOST: Media Oriented Systems Transport

MOST [10] is an automotive-specific high-speed multimedia network technology. It defines the physical and the data link layer as well as other layers of the ISO/OSI model of data communication. It was first introduced in 2001 by the MOST Cooperation consortium and has been implemented in ten vehicle models in the same year. The technology is nowadays used in almost every car brand, including Audi, General Motors, BMW, Hyundai, Honda, Lancia, Jaguar, Porsche, Mercedes-Benz, Land Rover, Toyota, Saab, Volkswagen, SKODA, Volvo, and SEAT. It is used to transport data signals, video, and audio inside vehicles. MOST nodes are connected via plastic optical fiber (POF) (MOST25, MOST150) or electrical conductor (MOST50, MOST150) physical layers, and it supports data rates up to 150 Mbps (MOST150).

The MOST protocol is secured by an automatically generated CRC sum (4 bytes) and ACK/NAK mechanism with automatic retry. There is no automatic retransmission in case of an error, and it has to be handled by the higher layers [10].

2.2.3 LVDS: Low-Voltage Differential Signaling

LVDS [11] is a technical standard that specifies high-speed signaling, using a differential, serial communication protocol. It specifies only the physical layer, while different data communication standards and applications that are built on top of it specify a data link layer of the ISO/OSI model.

The LVDS standard was defined in 2001, as ANSI/TIA/EIA-644-A standard.⁴ It is used for high-speed video, graphics, video camera data transfers, and general-purpose computer buses. Although LVDS was not specifically developed for the automotive industry, its high-speed bandwidth of 655 Mbps over twisted-pair copper cable made it the top choice for automotive camera manufacturers. Besides automotive infotainment system, it is used in LCD-TVs, industrial cameras and machine vision, notebooks, tablets, etc.

LVDS protocol, as Layer-1 protocol, does not define any security mechanisms.

2.2.4 LIN: Local Interconnect Network

LIN [12] is an automotive-specific bus standard, defined as a cheaper alternative to CAN for less important components of the in-vehicle network [6], like the seats and steering wheel adjustment. It is a broadcast master-slave serial network protocol, which supports a data rate up to 19.2 kbps, via a single wire. Similar to CAN, it specifies the first two layers of OSI model.

The first fully implemented version of LIN protocol was specified in 2002, by the LIN Consortium, founded by five car manufacturers – BMW, Volkswagen Group, Audi, Volvo Cars, and Mercedes-Benz. It is standardized in the ISO 17987 series, where ISO/AWI 17987-8⁵ is the standard defined for LIN over DC power line (DC-LIN).

LIN supports only error detection and checksums and faces similar risk exposures as CAN.

2.2.5 FlexRay

FlexRay is an automotive-specific bus standard. Its advantages over CAN are higher reliability and speed, while disadvantage is additional cost overhead. Similar to the previously described bus standards, it specifies the first two layers of the OSI model – the physical layer and the data link layer.

The FlexRay Consortium developed it in 2009, mainly for high-performance onboard automotive computing applications, including drive electronics and safety (e.g., proximity control, active suspension, drive-by-wire, etc.). It comes with a bandwidth from up to 10 Mbps and uses unshielded cable pairs. The consortium, which later disbanded, included BMW, Volkswagen, Daimler, and General Motors (GM). FlexRay is specified in ISO 17458-1⁶, 17458-2⁷, 17458-3⁸, 17458-4⁹, and 17458-5¹⁰ standards.

FlexRay, like other previously described bus protocols, was engineered in the absence of any security concerns. Therefore, it is highly vulnerable to adversarial attacks [13].

2.2.6 IEEE 802.3: Automotive Ethernet

Ethernet standard, commonly utilized as communication bus, is introduced to automotive industry as automotive Ethernet. The driving force for Ethernet usage in the automotive industry was primarily the high bandwidth. Additionally, the usage of UTP (unshielded twisted single-pair) cabling, its size, flexibility, and cost, also contributed to Ethernet applicability in vehicles. UTP cabling reduces network complexity and cabling costs and also contributes to free space and less weight of cars [6].

There are several revisions to the IEEE 802.3 standard that were made to fully meet the automotive requirements:

• IEEE 802.3bw¹¹: 100BASE-T1 – 100 Mbps Ethernet over a single twisted pair for automotive applications, released 2015, superseded;

• IEEE 802.3bp¹²: 1000BASE-T1 – 1 Gbps Ethernet over a single twisted pair, automotive and industrial environments, released 2016, superseded;

• IEEE 802.3bv¹³: 1000BASE-RHx – 1000 Mbps Ethernet over plastic optical fiber (POF), intended for home, industrial, and automotive use, released 2017, superseded;

• IEEE 802.3cg¹⁴: 10BASE-T1 – 10 Mbps Ethernet over a single twisted pair, intended for automotive and industrial applications, released 2019, active;

• IEEE P802.3ch¹⁵: IEEE draft standard for multi-Gig automotive Ethernet (2.5, 5, 10 Gbps) over 15 m, release date tba, active.

Comparing to previously described bus standards, Automotive Ethernet, with high bandwidth gives leeway to better authentication or encryption mechanisms (e.g., Media Access Control (MAC)), and due to point-to-point characteristics of the Ethernet, a stricter separation into and within functional domains can be achieved, using Virtual Local Area Network (VLAN), Quality of Service (QoS), and firewall concepts [14].

2.3 Inter-vehicle Communication

The interaction between vehicles and surrounding devices, including other vehicles and road side users, usually includes discussions about two types of protocols – WiFi based, often referred to as IEEE 802.11p from the name of the first standard designed to this scope, and cellular technologies including LTE-V2X and recently 5G, as part of the fourth generation of Third Generation Partnership Project (3GPP) standards and under the broader umbrella of the C-V2X (Cellular-V2X) [1]. Inter-vehicle protocols overview is presented in Table 2.

Table 2 Inter-vehicle protocols

2.3.1 IEEE 802.11p

IEEE 802.11p¹⁶ is the name of the first WiFi-based standard designed for V2X communication, released in 2010. Later, IEEE 802.11p was included in the IEEE 802.11-2012, which is afterward superseded by the IEEE 802.11-2016¹⁷. IEEE 802.11p defines the layer-1 (PHY) and layer-2 (MAC) layer protocols. A number of other standards have been defined above IEEE 802.11p standard, creating two different pillars – one in the USA, known as DSRC (dedicated short-range communication) and WAVE (wireless access in vehicular environments), and one in Europe, known as ETSI-ITS-G5 [1].

In the USA, IEEE 1609 standards define protocols below the application layer as wireless access in vehicular environments (WAVE), with IEEE 1609.12-2019¹⁸ as the active version. In Europe, IEEE 802.11p was adopted by ETSI under the Cooperative Intelligent Transport Systems (C-ITS¹⁹) as ITS-G5²⁰, together with a large number of other documents dealing with all layers above it, dedicated to automotive ITS and Road Transport and Traffic Telematics (RTTT).

In May 2018, IEEE announced a new study group focused on the evolution of 802.11 technology for next-generation V2X communications. Their work resulted in publishing the amendment IEEE 802.11bd²¹ later the same year. The ability to communicate for relative vehicle speeds of 250 kmph is a key feature of 802.11p. It operates in the licensed ITS band of 5.9 GHz with 10 MHz channel. IEEE 802.11p typically supports the range of 150–300 m. Its data rate is typically 6–27 Mbps, and it uses mesh network topology.

2.3.2 Cellular V2X

In parallel with IEEE 802.11p development, cellular technologies have been evaluated as long-range alternative. In 2016, 3GPP created the so-called C-V2X within Long-Term Evolution (LTE) Release 14²². It included a short-range interface that can be used also outside the cellular coverage and that poses an alternative to IEEE 802.11p [1].

In general, LTE is a wireless broadband communication standard designed for data terminals and mobile devices. It is based on the 2G/2.5G GSM/EDGE and 3G UMTS/HSPA technologies. LTE is specified in the 3GPP Release 8 and 9 document series, where Release 9 defines minor enhancements. It is also known as 4G LTE, Advance 4G, and 3.95G, since it does not meet the technical criteria of a 4G wireless service (defined in the 3GPP Rel. 8 and 9). In the beginning of 2020, ETSI published LTE-V2X²³ standard – LTE-V2X Access layer specification for Intelligent Transport Systems operating in the 5 GHz frequency band.

LTE-V2X advantages include easy implementation – it can use existing cellular infrastructure. It supports relative speeds of up to 500 kmph [15]. It provides rates of 300 Mbps for downlink and 75 Mbps for uplink. A transmission range depends on application mode and can be up to 100 km in the radio network, while in Direct C-V2X applications, it is greater than 450 m. It provides a longer reaction time for driver, than in 802.11p communications [16].

In 2018, 3GPP published the Release 15²⁴ that describes 5G NR (5G New Radio), including vehicle-to-everything communications (V2X) Phase 2. 5G is the successor of GSM (2G), UMTS (3G), and LTE and LTE Advanced Pro (4G).

The International Telecommunication Union Radiocommunication Sector (ITU-R) has lists following main uses for 5G:

• eMBB – Enhanced Mobile Broadband: an enhancement of 4G LTE mobile broadband services that includes more capacity, higher throughput, and faster connections;

• URLLC – Ultra-Reliable Low-Latency Communications: includes support for applications that requires uninterrupted and robust data exchange, like mission critical applications (deployment expected after 2021);

• mMTC – Massive Machine Type Communications: connects a large number of low-power and low-cost devices in a wide area; it should have increased battery lifetime and high scalability (deployment expected after 2021).

The three key frequency ranges for 5G spectrum, necessary to deliver widespread coverage and support all use cases, are:

• <1 GHz, which supports IoT services and provides widespread coverage across urban, suburban, and rural areas

• 1–6 GHz, expected to operate within the 3.3–3.8 GHz and to provide a good mixture of coverage and capacity benefits

• >6 GHz, expected to operate in 26 GHz and/or 28 GHz band, needed to meet the ultrahigh broadband speeds envisioned for 5G.

The targeted air latency in 5G is 1–4 ms. 5G should operate with throughput up to 10 Gbps, a hundred times faster throughput than 4G (LTE) speed of 100 Mbps. 5G Phase 2 is announced in 3GPP Release 16²⁵, with final submission planned for June 2020. It includes V2X Phase 3, with platooning, extended sensors, automated driving, and remote driving as main key points. More 5G system enhancements are set to follow in Release 17²⁶. It is scheduled for delivery in 2021. Enhanced V2X services are announced in this release.

3 Threat Modeling

The increasing connectivity demands of various handheld devices, Internet of Things (IoT) and infrastructure assets together with the built-in automotive components, result in new threats from cyber space that are striking directly without any warning time. Therefore, theoretical modeling about the security status of a complex system is becoming increasingly important. A theoretical modeling approach is threat modeling, which has the goal to identify potential threats and vulnerabilities based on the architecture of the given IT system. Conceptually different methodologies are used ranging from secure and agile application development to operative and business-driven concepts. Threat modeling is especially useful when applied during the design phase, as it delivers a semiformal security assessment which identifies security issues and the most likely attack vectors.

This section describes different threat modeling methodologies and their possible applications and limitations to model the domain of connected cars.

Threat modeling is a process for identifying security issues for various IT systems. By using different methodologies, threat modeling can be used for plenty of scenarios and is not limited in any way of creating new methodologies or even adapting existing ones for new purposes. Hence, with regard to connected cars, the research community has already adapted well-established methods and achieved great results.

3.1 Threat Modeling Overview

Different threat modeling techniques have been developed addressing not only different aspects, like data and data flow, application and assets, and risk based or impact oriented but also different application areas like the software engineering or system architectures overall. However, more general threat modeling is split into two approaches [17]:

• Application Threat Modeling

• Operational Threat Modeling

The former is focusing on identifying threats of applications or IT architectures, which are represented using process-flow diagrams (PFD). These threats can then be addressed by software developers, software testers, as well as system architects and cyber security experts to work on mitigation. The latter are created from an attacker’s point of view using data-flow diagrams (DFD). Operational threat models provide a visualization of the infrastructure’s big picture in order to give a better view on the full attack surface. The result is usual used within (Sec)DevOps life cycles. Regardless of the approach and the application field, threat modeling is usually performed in four steps [18]:

• 1. Model system

• 2. Find threats

• 3. Address threats

• 4. Validate

While the first point is usually done using different software tools, the second point usually differs from the used threat modeling approach, which will be discussed in more detail in the following subsections. The third point then focuses on addressing the found threats by coming up not only with mitigation strategies but also, depending on the used approach, with a risk assessment. In the last step, a validation of the work done in point one to three should be performed.

The following subsections discuss several techniques of threat modeling, outlining the different aspects they address, in order to understand the different approaches.

3.1.1 ATT&CK

Adversarial Tactics, Techniques, and Common Knowledge (ATT&CK) was created by MITRE and is used as a knowledge base and model for cyber adversary behavior. ATT&CK reflects the life-cycle phases of an adversary attack and the corresponding platforms. It can be used during various scenarios like red teaming or to improve defenses against network intrusion attacks. It started for Windows systems only, but now includes also Linux, macOS, cloud platforms, and mobile devices [19]. As stated in [20], the behavior model consists of three core models:

• Tactics, denoting short-term, tactical adversary goals during an attack (the columns);

• Techniques, describing the means by which adversaries achieve tactical goals (the individual cells);

• Documented adversary usage of techniques and other metadata (linked to techniques).

To illustrate an example, Table 3 [21] shows the ATT&CK Cloud Matrix. Since this technique has already been adapted for various platforms and systems, it could also be possible to adapt it for connected cars.

Table 3 ATT&CK cloud matrix

3.1.2 Attack Trees

Attack trees are a rather old but a still valid and valuable approach to discover threats in various environments. The concept was invented by Bruce Schneier [22] for modeling threats against computer systems. Attack Trees are not limited to computer systems, but in the information technology, they are a formal and methodical way to describe security threats based on possible attacks. Shostak describes in [18] three ways of using them: (1) use an attack tree created by someone else for your purposes; (2) create a tree specifically for your project; and (3) create a tree for general use, with the indent others will use it. Now, if you want to use a tree created by someone else, a modeled system is necessary first. Once this is done, the attack tree can be applied for each node of the model to see if the threat might be applicable or not. To illustrate the approach, an example attack tree for spoofing data flow is given in Fig. 3.

Fig. 3

Attack tree: spoofing of data flow

The illustration shows that the root node is most properly the goal of the attack but might also represent a component of the system. If it represents a component, the subnotes should indicate what could get wrong. If the root node is the goal of the attack, the next steps show how to achieve it. When adding multiple subnotes, it is important to decide if the relationship between the nodes represents AND or OR. However, most of the time, the attack trees are using OR relationships. Once the goal of the tree as well as every single step how to achieve it is drawn, you should consider to prune the tree. This way, each node will once again be evaluated if it is duplicative or maybe even already mitigated by your system. Lastly, an attack tree should not exceed a single page in order to keep it clearly represented. If that is not the case, a tree might need to be split up into several trees.

To sum up, in order to create an attack tree, six steps need to be followed:

• 1. Decide on representation (AND or OR)

• 2. Create the root node (goal or components)

• 3. Create subnotes

• 4. Consider completeness

• 5. Prune the tree

• 6. Check the representation

As there are plenty of general attack trees which already can be applied to various projects, this approach can also be applied on automotive systems. Also, as this section discussed, there is always the possibility to create new, specifically for automotive vehicles, attack trees.

3.1.3 STRIDE

STRIDE was originally introduced by Microsofts’ cyber security professionals Loren Kohnfelder and Praerit Garg as part of Microsoft’s Security Development Lifecycle (SDL) concept. STRIDE uses data flow diagrams to describe the communication between processes and data stores in order to generate threats that are divided into the following six categories [23]:

• Spoofing identity: A user or service illegally accesses and uses other authentication information to gain illegitimate access to a system or data.

• Tampering with data: Data tampering occurs when data is maliciously modified. This includes data at rest, data in use, as well as data in transit.

• Repudiation: This means that an entity may plausibly deny an action that it has taken. Countering these threats usually requires a combination of authentication, authorization, and logging, ideally in a cryptographically secured way.

• Information disclosure: Refers to any information exposed to unauthorized users.

• Denial of service (DoS): DoS attacks deny services availability to valid users.

• Elevation of privilege: These threats occur when unprivileged users gain privileged access and, thus, are able to compromise an entire system.

The Microsoft Threat Modeling Tool²⁷ offers different templates for various scenarios and also gives the possibility to create new templates. STRIDE therefore has already been adapted also for the automotive domain [24,25,26,27] and hence will be discussed in Sect. 3.2.1.

3.1.4 TARA

Threat Agent Risk Assessment (TARA), developed by Intel, is a methodology that not only identifies threats but also shows which of them are most likely to occur [28]. This is achieved by focusing on threat agents, their motivations and methods. Threat agents represent attackers with certain capabilities of skills and resources. These properties of a threat agent are then mapped to methods that can occur, which might lead to possible threats. TARA is also taking a step further, by considering acceptable levels of corporate risks. This means that although an attack is likely to occur, the impact might be too little, and TARA might not identify this threat has a high-priority item.

TARA consists of three components:

• Threat agent library (TAL)²: The library identifies 22 threat agent archetypes including from internal employees to different kinds of external criminals.

• Common exposure library (CEL): The CEL includes common security vulnerabilities and exposures and maps them to known mitigations.

• Methods and objective library (MOL): The MOL lists a set of methods on how threat agents usually plan to achieve their objectives.

When mapping these three components together, it becomes clear how the methodology works. As an example, Table 4 shows a sample from the MOL library. In Sect. 3.2.2, it is discussed how the approach and its components are adapted for the automotive industry.

Table 4 Sample from MOL library

3.2 Examples of Threat Modeling in the Automotive Industry

Since the previous section gave an overview about the different threat modeling methodologies, this section focuses on how to adapt threat modeling approaches for the automotive industry. Therefore, two examples on how popular approaches were already adapted in related works are given.

3.2.1 STRIDE for the Automotive Industry

The adaption of STRIDE is done using the template feature of the Microsoft Threat Modeling Tool. Here, a new template with regard to the automotive industry has been created by the NCC Group [26, 27]. The authors claim to provide following features:

• Processes and Data Stores related to connected cars;

• External Interactors tailored to an automotive system;

• Data Flows including over the air (OTA) and CAN bus;

• Trust Boundaries including vehicle-to-vehicle (V2V) networks;

• Known threats to components of connected cars, following the STRIDE categories.

Based on this template, a sample architecture of a connected car has been created and can be seen in Fig. 4. Here, a driver using a Human Machine Interface (HMI)/In-Vehicle Infotainment (IVI) and various sensors and cameras of the connected car is illustrated. These sensors and cameras are gathering information from the environment entity and are then passed to the Sensor Fusion Electronic Control Unit (ECU). The ECU sends the data to the gateway, which stores the data to the respective database. Also, a firmware update server and the respective data storage are drawn.

Fig. 4

Connected car: sample threat model

Figure 4 shows a simple example of a connected car threat model using an automotive industry template. A sample of the generated threats can be seen in Fig. 5, which shows newly added threats like tricking the sensor fusion ECU in into triggering an emergency stop, which, for example, would affect the safety of the vehicle, the passengers, and most probably also outside traffic participants. Although most of the threats are created specifically for the automotive template, all of them are still categorized in the STRIDE categories.

Fig. 5

Connected car: sample of generated threats

3.2.2 TARA for the Automotive Industry

In order to adapt TARA for the automotive industry, Karahasanovic et al. in [29] extended the TAL and MOL with industry-specific threat agents, methods, and objectives. The adapted version of the TAL includes a total of 19 threat agents for the automotive industry, which all have 9 different attributes. When used by security experts during the first two steps of TARA, the library helps to determine which threat agents present the greatest risk to the system. Table 5 illustrates the adapted TAL, showing the 19 threat agents and their attributes.

Table 5 Adapted TAL

Next, the Common Exposure Library is extended with all interfaces of a modern vehicle. Beside the interfaces, it also shows the impact level, the type of access, as well as the impact potential. Figure 6 illustrates the adapted library, which however is not complete as the properties might differ from various car manufactures.

Fig. 6

Adapted CEL

Lastly, for the methods and objectives library (MOL), the “Acts” and “Limits” sections were removed, and the “Method” section was newly introduced, containing the values “Theft of PII and business data,” “Denial of Service,” “Intentional Manipulation,” “Unauthorized Physical Access,” and “Unpredictable Action.” These methods conclude most of the cyber attacks which threaten the connected vehicles. Furthermore, the attribute “Impact” has new impact levels: “reputation damage,” “privacy violation,” “loss of financial assets/car,” and “traffic accidents and injured passengers.” The updated MOL can be seen in Table 6.

Table 6 Adapted MOL

4 Formal Modeling and Verification

Another possibility to identify possible attacks and to minimize the attack vectors at an early stage is the use of formal verification methods. By using a diverse set of mathematical and logical methods, security guarantees with respect to a given model developed from, e.g., a protocol specification, an implementation or (parts of) a system can be obtained.

In general, there are two types of formal verification tools, model checkers and theorem provers. Model checkers are usually more restricted to a certain problem domain and the verification of properties in that field. Based on a given model and its specification, the dependent state space is automatically and exhaustively checked. Theorem provers are useable for a wider field of potential problem settings. However, they often need human expertise as the formulation of algebraic constrains or theorems to guide a proof of correctness [30, 31].

For intra- and inter-vehicle protocols, a wide variety of tools for formal verification are applied. Approaches include:

• techniques to prove functional correctness

• detection of possible attacks

• considerations of the performance or worst-case scenarios

The focus of most of the publications is different depending on the protocols:

• intra-vehicle protocols: publications mainly focus on proving functional correctness and investigation of performance

• inter-vehicle protocols: especially for 5G, the focus is on security properties as secrecy and authentication.

Enhanced protocols are mainly considered for CAN, which do not provide authentication by default, and for 5G, where most of the work focus on 5G-AKA.

4.1 Formal Verification Tools Overview

Commonly used tools in literature are the security protocol model checkers AVISPA, ProVerif, Scyther, and Tamarin. In the class of probabilistic/statistical model checkers, the tools UPPAAL and PRISM are widely used (see also [32]). For those tools, a short description shall be given.

The push-button tool AVISPA ²⁸ stands for Automated Validation of Internet Security Protocols and Applications. The tool suite contains different verification techniques as On-the-Fly model checker (OFMC), Constraint-Logic-based Attacker Searcher (CL-AtSE), SAT-based model checking (SAT = satisfiability problems in propositional logic), and tree automate-based automatic approximation [33] for the security’s protocols analysis, applicable on the same protocol specification. Some of the techniques can deal with unbounded verification. Furthermore attack finding and visualization is supported.

The command-line tool ProVerif ²⁹ was developed for the automatic analysis of the security of cryptographic protocols. It can handle an unbounded number of runs of a protocol. The analysis of (weak) secrecy properties can be performed via reachability properties, authentication properties by using correspondence assertions. Additionally, ProVerif can prove observational equivalence, which can, e.g., be used for proving strong secrecy or real or random secrecy. In case a proof fails, the tool assists in the reconstruction of an attack.

The tool Scyther ³⁰ has a similar goal as ProVerif. Proofs can be obtained based on a symbolic representation of sets of protocol runs with the backward search algorithm. Moreover, it can be used for attack finding and visualization, can handle an unbounded number of sessions, and additionally has a GUI.

Another similar tool is Tamarin,³¹ which is both, a model checker and a theorem prover. Tamarin uses a generalization of Scyther’s backward search, which makes it capable of handling protocols with non-monotonic mutable global states and complex control flows such as loops. Tamarin enables attack finding and visualization. It can deal with models such as the eCK model for key exchange protocols and equational theories as Diffie-Hellman. Moreover, it can handle bilinear pairings as well as user-specified subterm-convergent theories.

The toolbox UPPAAL ³² focuses on system’s modeled as a collection of non-deterministic processes with finite control structures and real-value clocks, where the communication is performed via shared variables or through channels. Therefore, suitable application areas of the tool are, e.g., real-time controllers and communication protocols including critical timing aspects. The toolbox has three main parts, a description language, a simulator used for validation, and a model-checker based on timed automata theory.

The probabilistic model checker PRISM ³³ developed at the University of Birmingham is intended for formal modeling and the analysis of systems that exhibit random or stochastic behavior. The tool can handle several probabilistic models as probabilistic automata and probabilistic timed automata, discrete-time and continuous-time Markov chains, as well as Markov decision processes. The underlying probabilistic verification techniques include quantitative abstraction refinement and symmetric reduction. Furthermore, the generation of optimal adversaries/strategies is supported.

4.2 Examples of Formal Modeling and Applications in Connected Cars

In this section, an overview of different intra- and inter-vehicle protocols where formal methods are applied is given. It extends our previous work in [2], provides more details, and addresses a wider range of protocols.

4.2.1 Intra-vehicle Protocols Formal Verification

For intra-vehicle protocols, formal methods are applied to the CAN, Automotive Ethernet, and FlexRay.

Most of the work there are applications of formal method to specifications/standards in order to check selected properties. For CAN there are also enriched schemes/protocols checked. Additional security for the low-level protocol CAN is considered in [39], where an authentication protocol for CAN is presented. Furthermore, a clock synchronization service for CAN is proposed. An overview about different approaches is given in Table 7. Details on the existing approaches are given below.

Table 7 Intra-vehicle protocols

Guergens et al. propose in [34] an abstract vehicle communication system model providing telemetric functions and onboard communication. It considers four car components, namely, the fieldbus, the telemetric ECU (electronic control unit), a backend server, and also terminals representing clients. As main attack points, the interface GSM/GPRS for a remote attacker and the fieldbus interface for a local attacker is considered. For formal modeling under the Dolev-Yao attacker model [40], the authors use Asynchronous Product Automata (APA), an operational description concept for cooperating systems. As tool, the Simple Homomorphism Verification tool (SHVT), providing components for the complete cycle from formal specification to exhaustive analysis and verification and supports APA, is used. The authors consider a real-world example, which is – with support from SHVT – analyzed for three different scenarios which differ by the foreknowledge of the attacker. There, especially replay messages, unlocking someone else’s car, and downgrading of security mechanisms are taken into account. Additionally, a formal model of a fieldbus is given.

Pan et al. consider in [35] a formal verification with UPPAAL of the CAN bus protocol with a focus on the arbitration process, the transmission process, and the fault confinement mechanism. The authors formalize 11 properties, which can be divided into three categories, namely, safety, liveness, and invariant. The formal verification with UPPAAL shows that the main security issues of the CAN bus system are deadlock, starvation, data inconsistency, and the fault confinement mechanism. The authors state that the detected problems can at least be partly solved in the application layer.

Bruni et al. give in [39] a formal analysis of MaCAN. MaCAN is an authentication protocol developed in order to enable authentication in the CAN bus. By using ProVerif, the authors detected two flaws. The first one leads to unavailability during key establishment. The second one allows a re-using of authenticated signals for different purposes. The authors state that some aspects of MaCAN had to be adjusted (e.g., the usage of timestamps for ensuring message’s freshness). However, it is stated by the authors that they could not express the freshness of timestamps in ProVerif, since ProVerif abstracts away the state information. Furthermore, the presence of an attack in their own implementation of the protocol is experimentally verified.

Rodriguez-Navas et al. apply in [41] model checking on a proposed clock synchronization service for the Controller Area Network (CAN) for highly synchronized clocks even in the occurrence of faults in the system. For modeling and verification, the tool UPPAAL is used. The model is based on timed automata, and a novel technique for drifting clocks is proposed. The author’s solution achieves the desired precision event in case of the presence of various node and channel faults. Furthermore, their results indicate that inconsistent channel faults pose a big threat to clock precision. However, it is possible to reduce their negative impact by using a suitable resynchronization period.

Thiele et al. focus in [36] on an analysis of timing impact, which is introduced by various CAN/Ethernet multiplexing strategies at gateways. The authors state that the timing determinism of critical control and streaming data is crucial in the automotive network design. In particular, three different aspects of multiplexing are considered: buffering, triggering, and mapping. By using Compositional Performance Analysis CPA [42], the authors model and analyze three different multiplexing scenarios. In the evaluation, the authors focus on the effect of multiplexing on the design metrics worst-case and end-to-end latency and load. Furthermore, their analysis allows to capture and quantify differences between different multiplexing strategies.

Zhang considers in [37] the FlexRay bus guardian component. The bus guardian component helps to protect the communication channel against faulty behavior of communication controllers in FlexRay. The author uses Isabelle/HOL, a theorem prover for higher-order logic for specifying and verifying. The focus in the paper is on two properties of the bus guardian, namely, the correct relay and the integrity. In order to verify the properties, the correctness of the FlexRay clock synchronization is assumed.

Gordon and Choosang give in [38] a formal analysis of the AUTOSAR FlexRay Transport Protocol by using Colored Petri Nets, a mathematical modeling language. The authors prove that the FlexRay Transport Protocol is deadlock-free for certain configurations in case of delivering a single-protocol data unit from the sender to the receiver. Furthermore, it captures the desired service language. Moreover, it is stated by the authors that their results indicate the absence of functional errors in the protocol specification and that the protocol is likely error-free.

4.2.2 Inter-vehicle Protocols Formal Verification

Formal verification is considered for the MAC of IEEE 802.11p and a wide variety of approaches for 5G (see Table 8). For 5G especially, 5G-AKA and 5G-EAP-TLS are considered. Furthermore, there are several approaches to formally verify enhanced versions of 5G in general – not focusing on the automotive domain explicitly – as [43,44,45,46,47]. Details of the approaches are given below. A review of formal verification method approaches considering 5G is also given in [32].

Table 8 Inter-vehicle protocols

Zou et al. in [48] consider the Media Access Control (MAC) of IEEE 802.11p. The MAC abilities are essential in order to reach requirements as high-speed data transmission and self-organization of networks. In the MAC protocol of 802.11p, the collision avoidance mechanism is used. That means in a first step, a node needs to listen to a channel. Then, two cases can be distinguished: The channel is free (for a specific time period), and then data packets can be sent directly. Otherwise, the node has enter the backoff procedure and wait. For modeling probabilistic timed automaton (PTA) is used, since it fully takes the characteristics of the MAC into account due to the non-deterministic existence and the support of continuous time and probabilistic choice. As tool PRISM is used. For modeling, the MAC protocol is abstracted into four modules, a destination node, two sending nodes, and a transmission channel, which are sufficient to cover any transfer case in 802.11p. As performance measures, two different types, the probabilistic and the expected reachability, are considered. With the probabilistic reachability, the successful completion of the data transmission process in 802.11p can be verified. Moreover, the probability of reaching the max backoff counter of any station is much less for 802.11p than for the 802.11 standard. Therefore, the data can be transmitted forward under a high speed. Furthermore, by using expected reachability, it is shown that a collision event in 802.11p is less likely than in 802.11. The authors also point out an approximately four times higher average transmission speed for 802.11p compared to the one of 802.11 standard.

Basin et al. provide in [49] an extensive formal analysis of the Authenticated Key Exchange protocol used in 5G (5G AKA). This protocol and especially its security guarantees are important for ensuring the security of the users’ calls, text messages, and mobile data. The contribution of the authors is very broad. First, the authors formalize the standard, targeting a wide range of properties – confidentiality, authentication, and privacy – and fine-grained versions of them. Second, the authors create a formal model, which is then evaluated by using the Tamarin tool. The formal, systematic security evaluation shows that some critical requirements are underspecified (especially for authentication) or even missing. It is pointed out that without further assumptions, some properties are violated, as the agreement properties on the session keys. Furthermore, the authors criticize the standard’s choice of implicit authentication as well as the absence of key confirmation. The authors explicitly state that this introduces weaknesses if the protocol is not used in the way it is intended for. Moreover, the authors detect a likely realistic privacy attack, due to the fact that 5G AKA does not provide unlinkability against an active attacker. Additionally, the authors suggest a fix for the security issue.

Cremers and Dehnel-Wild also study in [50] 5G AKA, performing a fine-grained formal analysis with the Tamarin tool. The authors state several challenges which complicated their work: first, the complexity of the specification documentation; second, the complexity of the protocol involving all four parties which are defined in the protocol specification and third, the informal nature of the security requirements, forcing the modeler to make complex assumptions on the basis of possible use cases. All four parties are modeled by the authors. Furthermore, possible assumptions on the channels connecting these four parties have been modeled precisely. The proposed formal model from 5G AKA standard enables a detailed view of the interactions between several security-critical components. The results show that 5G AKAs security is based on unstated assumptions on the inner workings of underlying channels. This results in an attack which exploits a potential race condition. However, even for the honest case, solving the race condition does not necessarily prevent the attack. It is stated that in practice, the standard can be implemented “correctly” in an insecure manner. Moreover, the authors propose a possible fix based on their findings.

Zhang et al. focus in [51] on the 5G-EAP-TLS protocol, which is defined in 5G networks for subscriber authentication in limited use cases as private networks or IoT environments. One main security goal is to ensure mutual authentication between subscribers and their home network. The authors state to provide the first 5G-EAP-TLS formal protocol model and perform a security analysis with the use of the Scyther model checker. In their model two roles are considered, user equipment (UE) and network (NW). The last is a composition of the home network and the server network. The authors check four security related properties: the secrecy of the Subscription Permanent Identifier (SUPI) and the one of the session key; for UE, the secrecy hold for SUPI and the session key; and for NW, only the secrecy of the SUPI can be verified. The other two security-related properties, the non-injective synchronization of events and the non-injective agreement on data, are falsified with Scyther, for both UE and NW.

Zhang et al. focus in [52] on the 5G-EAP-TLS protocol. There, the protocol is modeled in applied pi calculus, while ProVerif is used for the security analysis. The authors extend their previous work in [51] by using a more expressive formal language which is capable of modeling the protocol’s behavior more precisely. Moreover, a more fine-grained formal model is provided, i.e., the severing network and the home network are considered to be a single entity. The authors check three secrecy and two authentication statements. For the authentication, it is falsified with ProVerif that the subscriber and the home network agree after successful termination on the identification of each other. Furthermore, ProVerif falsifies that after successful termination, both parties agree on the pre-master key. The secrecy statements can be successfully verified with ProVerif. Those statements include: The adversary must not be able to obtain the SUPI of an honest subscriber, nor the pre-master key, nor the session key. The authors propose a provable fix, showing that their revised version fulfills the stated security properties.

Koutsos considers in [43] the privacy of 5G-AKA. Although asymmetric randomized encryption is used in order to reach a better privacy than for 3G or 4G, only the IMSI-catcher attacker can prevented. Other known privacy attacks as the Failure Message Attack and Encrypted IMSI Replay Attack still hold. In a second step, the 5G-AKA protocol is modified for the prevention of those attacks. The security proof is performed by Bana-Comon indistinguishability logic and shows the absence of those privacy attacks.

Braeken et al. propose in [44] based on the detected security issues in 5G-AKA in [49] a new version. There a non-monotonic logic – also known as RUBIN – is used to successfully verify the proposed scheme. The reason for choosing RUBIN was that this method is quite close to the actual protocol’s implementation.

Sharma et al. proposes in [45] an enhanced handover AKA protocol for being used in 5G communication networks in order to overcome security vulnerabilities as false base-station attack, key compromise, DoS attacks, and high authentication complexity. The authors use AVISPA to show that their proposed protocol is not vulnerable to the stated attacks.

Han et al. in [46] suggest the employment of Mobile Edge Computing (MEC) servers into the traditional authentication architecture for re-authentication. Furthermore, instead of using one-way hash functions and permanent names for authentication, the use of existing Extensible Authentication Protocol-Authentication and Key Agreement (EAP-AKA) protocol pseudonyms is proposed. In their security analysis, the authors use AVISPA and especially consider mutual authentication, confidentiality, and anonymity. All those security attributes can be verified.

Cao et al. propose in [47] a group-based handover authentication and re-authentication protocol for massive machine type communication (mMTC) in 5G wireless networks. By using BAN logic and the model checkers AVISPA and SPAN, the authors verify that their proposed protocol is secure against various malicious attacks.

5 Conclusions and Key Points

Connected cars services, which increase road safety, and contribute to traffic flows’ efficiency and passengers’ comfort, require complex communication infrastructure behind. V2X, the most important technology in connected cars communication, includes two main subnetworks – intra-vehicle network, including a collection of in-vehicle controlling and processing units and sensors, and inter-vehicle network, including the communication between the vehicle and surrounding.

Intra-vehicle communication usually involves bus protocols and media-oriented protocols. The most common bus protocols are LIN, CAN, and FlexRay. Widely used media protocols are MOST and LVSD. Nowadays, Automotive Ethernet, due to increased bandwidth and cheap components, is taking over both purposes.

Inter-vehicle communication includes two types of protocols, categorized by the used technology. The first type is a WiFi-based protocol, often referred to as IEEE802.11p from the name of the first standard designed to this scope. The IEEE802.11p protocol is now superseded and became part of WiFi protocol IEEE802.11. Two other initiatives based on IEEE802.11p are ETSI ITS-G5 in Europe and IEEE 1609 in the USA. In parallel to WiFi-based protocol, cellular technologies also offer solutions for V2X communication. Cellular solutions are known as C-V2X (Cellular-V2X) and include LTE-V2X and recently 5G, with additional V2X functionalities announced for future releases, including platooning, extended sensors, automated driving, and remote driving.

Because of significant growth and 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.

The threat modeling section discussed state-of-the-art methodologies and the ability to adapt those for the automotive industry. It was shown that various methodologies already exist for plenty of scenarios by either using more general approaches or even adapting those general approaches for more specific settings. For the latter, two explicit, for the automotive domain adapted, methodologies were discussed. Upcoming challenges will therefore not only include enhancing those methodology in the research but more likely to consider this research into the development process of the automotive domain.

Another security-by-design framework – formal verification and its applications in automotive industry were also discussed in this chapter. It was shown that formal verification approaches are clearly different depending on the type of the protocol. While for intra-vehicle protocols the focus of the approaches are mainly functional correctness and the investigation of performance, for inter-vehicle protocols – especially for 5G – the focus is clearly security properties as secrecy and authentication. However, none of the approaches focus on implementations of the corresponding protocols. So far applying formal verification tools to verify those implementations, with different purposes as checking for implementation errors, but also to check if the implementation follows the standard/specification and does not pose additional security issues, is still an open issue. As stated in [53] and the references therein, for several implementations for widely used implementations of different application layer protocols, several security issues have been detected, opened by the implementation since they do not follow the corresponding standard.

Further research might consider – as stated in [2] – forced protocol downgrading, which might arise due to the unavailability of the technology. Further research also might deal with [32] a combination of tools for better overall results in case of restrictions of the model checker, model checking for different versions of a protocol, and an in-depth analysis in order to provide a very broad verification for the connected vehicle by a suitable combination of different in-depth verifications of pieces in the protocol and some an overall analysis.