Project topics and materials
Get Complete Project Material File(s) Now! »
Current Vehicles Architecture
This section presents a fine grained view of current automotive architectures. The architectural description is taken as a reference to show associated security concerns. Uncovered security aspects are described in next subsection 2.3. Some parts of the technology are currently under development and still need to be secured and tested. Current in-vehicle networks exhibit general characteristics of standard computer networks. An in-car network counts dozens of interconnected nodes named ECUs supporting thousands of inter-dependent SW applications which are composed by gigabytes of code [166]. In addition to existent on-board applications, several off-board facilities are being developed in order to communicate vehicle with outside world. The ECU nodes are linked via a variety of buses like CAN, MOST, FlexRay, LIN or Byteflight. ECUs are HW/SW components integrated by modules that are structured by layers. ECUs play dedicated roles within the network: they may be sensors, gateways, routers, actuators, etc. Along with a generic role, ECUs also support a variety of high level applications. ITS deployment shall introduce new safety-critical applications, e.g., emergency braking systems, operating in parallel with non-safety critical ones, e.g., infotainment media. The introduction of X-by-wire technology [118] shall allow ECUs to fully or partially automate a variety of mechanical systems like those controlling brakes or accelerator, e.g., Brake-by-wire. Recently, the steering-by-wire technology was introduced in commercial vehicles by the first time ever [143].
Several principles are being applied to secure embedded systems. As suggested in [85], the use of virtualization techniques may help to deal with interactions from attackers. By categorizing and separating ECU applications according to their exposure to threats, their exchanges can be better controlled and the system protected. It is considered [85] that Virtual Machines can be used to enforce security requirements in combination with tamper resistant modules like the TPM [194] or the HSM [198]. Just referred modules are the basis upon which ECU security is built since both can play the role of security anchors: they provide mechanisms to enforce platform integrity, authenticity, confidentiality, and freshness. Even so, TPM and HSM own different features. In particular, the TPM is standardized what favorably impacts applications development and portability. The HSM is not standardized but provides HW acceleration, modular architecture, more cryptographic primitives, and a Coordinated Universal Time (UTC) clock, all not supported by the TPM. Figure 2.1 shows the crosslayer modular composition of an ECU supporting security, safety, and user oriented applications. This architecture specification is borrowed from [13].
Known Attacks and Potential Impact
This subsection presents a refined view of vulnerabilities in off-board and on-board vehicle embedded systems. As shown in [121], [179], if an attacker gains enough ECU control, several safety critical applications as those controlling, alerts, engine or even brakes can be compromised. By performing techniques like sniffing, target probing, and packet fuzzing over CAN buses, the attacker can lead to undermine the operation of applications, sensors, and actuators. Indeed, a hostile party can for instance: display arbitrary messages, speed-up and disturb engine, impede driver from starting or stopping engine, perform braking, lock or disable brakes, and freezing instruments panel [121]. Attacker capabilities can be increased by applying reverse engineering upon sniffed data. By doing that, the attacker may even fully drive the Body Electronic Module. Hence, attention is raised on the fact that vehicle architectures should be endowed with adequate security protections with regard to a set of potential attacks [121].
Table 2.2 presents a list of some known attacks associated to target vehicle assets. Some major consequences of the attack are also mentioned, e.g., with respect to security, safety, and driver’s economy. The list is descriptive and made according to the issues mentioned in previous subsection 2.3.1. It means that other relevant attack scenarios due to for instance dishonest owners or garage service providers are also feasible. For example, configuration/development tools like [67] and [213] can be used to modify ECU’s configuration so as to unbridle car’s engine. This kind of attacks are out of scope and consequently they are not addressed in this thesis manuscript.
Verification Methodologies Survey
This section shows several methodologies targeting verification in concurrent embedded systems. Methodologies are shown according to the taxonomy previously adopted. Descriptions mainly include modeling semantics, support for requirements modeling, and formal verification procedures. When adequate, other phases covered by the approach are described, e.g., code generation. A brief evaluation is provided what highlights main advantages and also limitations. The terms “methodology” and “approach” are used in the same semantical sense. It is nonetheless recognized that some of the items presented in the survey do not truly correspond with a methodology but only with a standalone environment, framework, tool, language, or method. They are even so analyzed due to their support and relevance for the engineering development process.
Table of contents :
1 Introduction
1.1 Context
1.2 Problematic
1.3 Contributions
1.3.1 Objective
1.3.2 Thesis Approach Synopsis
1.4 Outline
2 Security and Vehicular Applications
2.1 Vehicular Applications Evolution and Security
2.1.1 80’s Decade Developments
2.1.2 90’s Decade Developments
2.1.3 2000’s Decade Developments
2.1.4 From 2010 Up to Now Developments
2.2 Current Vehicles Architecture
2.3 Uncovered Security Aspects
2.3.1 Critical Security Aspects
2.3.2 Known Attacks and Potential Impact
2.3.3 Hypothetical Automotive Attack
2.4 Conclusions
3 Methodologies for Embedded Systems Verification
3.1 Verification Methodologies Survey
3.1.1 Generic Formal Theories
3.1.2 Generic Formal Based Tools
3.1.3 Formal Security Oriented Methodologies
3.1.4 Cryptographic Protocol Oriented Approaches
3.1.5 Model Driven Engineering Environments
3.1.6 High Level Non-MDE Environments
3.1.7 Certification Oriented Approaches
3.2 Qualitative Evaluation of Verification Approaches
3.2.1 Features by Category
3.2.2 Pros and Cons of Verification Methodologies
3.2.3 Properties Support and Framework Usability
3.3 Summary and Conclusions
4 Proposed Methodology for Verifying Critical Embedded Systems
4.1 Contributions and Methodology Overview
4.2 Methodology Description
4.2.1 Threats Analysis
4.2.2 System Analysis
4.2.3 System Design
4.2.4 Requirements Structuring
4.2.5 Properties Modeling
4.2.6 Formalization and Verification
4.2.7 Coverage Assessment
4.2.8 Code Generation and Adaptation
4.2.9 Platform Tests
4.3 Conclusions
5 Assisted Design with Avatar
5.1 The Avatar Design Framework: An Overview
5.1.1 Avatar Design Metamodel
5.1.1.1 Block Metamodel Components
5.1.1.2 SMD Metamodel Components
5.1.2 Avatar Design Framework Implementation
5.2 Extending Avatar Design Profile
5.2.1 Avatar Design Limitations
5.2.2 Avatar Extensions: The Avatar Security Environment
5.3 Attaching a Formal Semantics to AvatarSE
5.3.1 Avatar & AvatarSE Formal Descriptions
5.3.1.1 Avatar Formal Description
5.3.1.2 AvatarSE Formal Description
5.3.2 AvatarSE-to-ProVerif Transformation
5.3.3 Example of Transformation
5.4 Approach Limitations and Conclusions
5.4.1 Approach Limitations
5.4.2 Conclusions
6 Case Study: Securing and Testing EVITA Architecture
6.1 Securing EVITA Symmetric Keying Protocol
6.1.1 Initial System Analysis
6.1.2 Threats and Requirements Analyses
6.1.3 Design and Verification
6.1.4 Attack Coverage Assessment
6.1.5 Conclusions: Case Study I
6.2 EVITA HSM Driver Tests
6.2.1 HSM Driver Context
6.2.2 Driver Test Method
6.2.3 Driver Testing Environment
6.2.4 Results and Discussion
6.2.5 Conclusions: Case Study II
7 Conclusions and Perspectives
7.1 Initial Findings
7.2 Contributions and Conclusions
7.3 Discussion: Shortcomings and Perspectives
A Underlying Formal Backend
A.1 ProVerif
Bibliography
