Project topics and materials
Get Complete Project Material File(s) Now! »
Security modeling and verification in the mapping phase
As to be discussed in Chapter 3, most security modeling describes the detailed implementation of security protocols, and takes place in the last phases of design. However, the choice of architecture should depend on its ability to support security features. When designing an architecture and mapping the functions to architecture, the selection of an optimal mapping relies on correct approximations of execution times of functions [141]. Therefore, the time to execute these security protocols should be considered when selecting an architecture/mapping.
However, placement of security functions depends on which data should be secured, which in turn depends on both the capabilities of the attacker to access the architecture, and which data can be accessed from those architectural locations. While previous works can take into account the performance overhead due to execution of security protocols, they lack the ability to check if an attacker can access or modify critical data [14, 288]. To be certain that security protocols are correctly placed and all security properties are satisfied, a formal security verification process should be used. To assist the designer, it could also be helpful to add security mechanisms automatically based on the verification results, and thus generate a new model fixing all the security flaws.
This thesis describes an approach on modeling attacker capabilities affecting the security of an architecture, and how to abstractly model the functional and architectural security mechanisms for secure communication, including encryption, Hardware Security Modules, and Firewalls [201]. Furthermore, we discuss how to translate mapping models to a formal specification to be analyzed by the security verifier ProVerif. Based on the verification results, the security flaws in the model could be fixed through the addition of various security mechanisms. To actualize these ideas, the security modeling and verification steps are implemented in our toolkit.
Proof of Correctness of Model Transformation for Formal Security Verification
While some formal verification tools conveniently operate directly on program code or graphical models, most use a mathematical specification language that is complex, difficult to read, and unusable for actual design [41]. As we rely on graphical models for their ease of use, to formally analyze our models requires a model transformation process. The correctness of verification results, however, relies as much on correctness of the model transformation as it does the correctness of the model and formal verification tools [220, 328].
We prove the correctness of the model transformation to a formal specification that can be analyzed with a security prover, leveraging in part the proof and transformation process described in [208].
Survey of Hacks on Connected Vehicles
The authors of [159] presented privacy and security risks of a Tire Pressure Monitoring System. By monitoring RF signals from the sensors, the authors found the unique sensor ID for identification of the vehicle, and spoofed packets to send fake tire pressure warnings. This attack could force a driver to pull over thinking he had a flat tire, and also the ability to track cars by their wireless signals is a privacy concern.
Telematics units can be attached to cars, and often used for insurance purposes, have been an avenue of attacks on the operation of vehicles themselves. The authors of [188] performed an attack through the OBD-II port using the CAN-to-USB interface. The authors built a CAN packet sniffer/injector and determined how to control units, many commands discovered through fuzzing. Furthermore, the attack restarts the ECU and erases any evidence of the attack code. However, the attack required physical access to the OBD device.
Another minor attack [345] used a malicious application on a paired smartphone and a car with an OBD-II scan tool. When an OBD-II and smartphone with diagnostic application are connected through bluetooth, an attacker can send malicious CAN frames to the vehicle. While it required the user to accidentally install the malicious application and for the car to have a telematics unit installed, it demonstrates another avenue of attack.
The authors of [109] analysed the Metromile TCUs, an aftermarket device interfacing with the OBDII port. The ssh keys were common to all TCUs and could be acquired by dumping the NAND flash. Updates to the TCU were sent through SMS messages, which the authors used to create a new console starting a remote shell to obtain access to the device through ssh. The authors note that the update did not have the vehicle verify the server’s identity, which is a major vulnerability.
Table of contents :
1 Introduction
1.1 Safety and Security Concerns in IoTs/Embedded Systems
1.2 Design of Embedded Systems
1.3 Problem Statement
1.4 Contribution of this Thesis
1.4.1 Security modeling and verification in the mapping phase
1.4.2 Proof of Correctness of Model Transformation for Formal Security Verification
1.4.3 Attacker Modeling
1.4.4 Latency analysis
1.4.5 Proposition of a modified SysML-Sec Methodology
1.4.6 Taxonomy for Safe and Secure Autonomous Vehicle Design
1.5 Organization of this Thesis
2 Context: Autonomous Vehicles
2.1 Safety and Security Flaws
2.1.1 Safety Flaws in Commercial Vehicles
2.1.2 Survey of Hacks on Connected Vehicles
2.1.3 Safety Limitations of Autonomous Vehicles
2.1.4 Survey of Potential Attacks on Future Autonomous Vehicles
2.1.5 Conclusion
2.2 Approaches to Vehicle Safety and Security
2.2.1 Proposals for Safe and Secure Automotive and Embedded System Design
2.3 Taxonomy
2.3.1 Potential Causes of Failure
2.3.2 Undesired States of System Behavior
2.3.3 Unsafe Comportment
2.3.4 Countermeasures
2.3.5 Conclusion
2.4 Countermeasures
2.4.1 Safety Countermeasures
2.4.2 Security Countermeasures
2.4.3 Secondary Effects of Countermeasures on Safety, Security, and Performance
2.4.4 Conclusion
2.5 Design Process Requirements
2.5.1 Methodology Capabilities
2.5.2 Properties to Verify
2.5.3 Security Properties
2.5.4 Conclusion
3 Related Work
3.1 Software Development approaches
3.1.1 Agile
3.1.2 Waterfall/V Life Cycle
3.2 Model Driven Methodologies and Toolkits
3.2.1 Frameworks for Analysis
3.2.2 Frameworks for the Design of Embedded Systems
3.2.3 Frameworks for Software Design
3.2.4 Conclusion
4 Modeling Methodology
4.1 Introduction
4.2 Overview
4.3 Analysis
4.3.1 Requirements
4.3.2 Attack Trees
4.3.3 Fault Trees
4.3.4 Relationship between Analysis Phase Diagrams
4.4 Design Phases
4.5 HW/SW Partitioning
4.5.1 Application/Functional Modeling
4.6 Software Design
5 Security-Aware HW/SW Partitioning
5.1 Motivation
5.2 Attacker Model
5.3 Security Modeling
5.3.1 Architecture Vulnerabilities
5.3.2 Attacker Scenarios
5.3.3 Attacker Scenario Analysis
5.3.4 Security Countermeasures
5.4 Conclusion
6 Security Verification
6.1 Introduction
6.2 ProVerif
6.2.1 Functions
6.2.2 Declarations
6.2.3 Queries
6.2.4 Main Process
6.2.5 Sub-processes
6.2.6 Formalizations
6.2.7 DIPLODOCUS to ProVerif Translation Process
6.3 Formalization for Translation
6.3.1 DIPLODOCUS Formalization
6.3.2 AVATAR Formalization
6.4 DIPLODOCUS to AVATAR Translation Formalization
6.4.1 Full DIPLODOCUS to AVATAR translation
6.4.2 DIPLODOCUS to AVATAR translation for Security
6.4.3 Translation of Operators
6.5 Translation to ProVerif
6.5.1 Translation of Queries
6.5.2 Translation of Tasks
6.5.3 Translation of Actions
6.6 Proof of Correctness
6.6.1 Base case
6.6.2 Inductive Step
6.6.3 Conclusion
6.7 ProVerif Results
6.8 Automatic Generation
6.8.1 Security Requirements
6.8.2 Addition of Security Operators
6.8.3 HSM Generation
6.8.4 Automatic Key Mapping
6.8.5 Automatic Generation for Case Study
6.9 Conclusion
7 Performance Evaluation
7.1 Introduction
7.2 Latency Analysis
7.2.1 Latency Requirements
7.2.2 Latency Annotations
7.2.3 Latency Analysis
7.2.4 Backtracing Latencies
7.3 Relating Latencies across Levels of Abstraction
7.4 Performance Impact due to adding Security
7.5 Conclusion
8 Conclusion and Perspectives
8.1 Integration of full Safety and Security Features into Autonomous Vehicle Model
8.2 Contributions
8.3 Perspectives
8.3.1 Security for Embedded Systems in Practice
8.3.2 Accurate Representation of Countermeasures
8.3.3 Full Automatic Generation of Countermeasures
8.3.4 Security Modeling and Verification
8.3.5 Time in ProVerif
8.3.6 Safety Countermeasure Modeling
8.3.7 Safety and Security Analysis Diagrams
8.3.8 Relationship between Safety, Security, and Performance
8.3.9 System Resilience
8.3.10 Vulnerability Modeling
8.3.11 Improved Connections between Phases
8.3.12 Integration of Security Verification Results
8.3.13 Proof of Correctness for Authenticity
8.3.14 Attack Probabilities
9 Resume
9.1 Introduction
9.2 Contexte
9.2.1 Sûreté et Sécurité des Voitures Autonomes/Connectés
9.2.2 Contre-mesures proposées
9.2.3 Effets secondaires des contre-mesures pour la sûreté, la sécurité et la performance .
9.2.4 Travail Connexe
9.3 Méthodologie
9.4 Sécurité d’un Partitionnement Logiciel/Matériel
9.4.1 Modèle d’Attaquant
9.4.2 Modèle de Vulnérabilités
9.4.3 Scénarios d’attaque
9.4.4 Modèle de Contre-mesures
9.4.5 Vérification Formelle
9.4.6 Génération Automatique de Contre-mesures
9.5 Évaluation des Performances
9.5.1 Mesure des Temps de Latence
9.5.2 Analyse de Système Sûr et Sécurisé
9.6 Conclusion
9.6.1 Contributions
9.6.2 Perspectives
Bibliography
