https://www.mdu.se/

Automotive systems are not only becoming more open through developments like advanced driving assistance functions, autonomous driving, vehicle-to-everything communication and software-defined vehicle functionality, but also more complex. At the same time, technology from standard IT systems become frequently adopted in this setting. These developments have two negative effects on correctness and security: the rising complexity adds potential flaws and vulnerabilities while the increased openness expands attack surfaces and entry points for adversaries. To provide more secure systems, the amount of verifying system security through testing has to be significantly increased, which is also a requirement by international regulation and standards. Due to long supply chains and non-disclosure policies, verification methods often have to operate in a black box setting. This thesis strives therefore towards finding more efficient methods of automating test case generation in both white and black box scenarios. The focus lies on communication protocols used in vehicular systems. The main approaches used are model-based methods. We provide a practical method to automatically obtain behavioral models in the form of state machines of communication protocol implementations in real-world settings using automata learning. We also provide a means to automatically check these implementation models for their compliance with a specification (e.g., from a standard). We furthermore present a technique to automatically derive test-cases to point out found deviations on the actual system.We also present a method to create abstract cybersecurity test case specifications from semi-formal threat models using attack trees. 

This thesis strives towards finding more efficient methods of automating security test case generation, which are currently in a state of infancy for automotive systems, in both white and, especially, black box settings. The thesis focuses on communication protocols used in vehicular systems and we base our research on formal methods. The rationale is their rigor, as they are based on sound logical principles, and their potential for efficiency gains, since formally defined systems can be more easily analyzed algorithmically and, therefore, tested automatically. Our contributions include:

• Methods for deriving automata: 

• We provide a method to automatically obtain behavioral models in the form of state machines of communication protocol implementations in real-world settings using automata learning.   
• We demonstrate a method to derive compound protocol state machines, i.e., state machines representing systems that communicate via more than one protocol at the same time

• Methods for checking automata:   

• We provide a means to automatically check these state machines for their compliance with a specification (e.g., from a standard, like ISO/IEC 14443-3). 
• We provide a scheme, Context-based Proposition Maps (CPMs), to aug    ment the state machines with propositions (i.e., attributes that can be checked).   
• We define generic Linear Temporal Logic (LTL)-based properties to recognize cybersecurity-related specification violations.   
• We provide a method to model-check inferred state machines utilizing the Rebeca modeling language providing a formally defined template.

• Methods to facilitate test case generation: 

• We present a technique to automatically derive test cases to demonstrate deviations identified in a state machine on the actual system.   
• We also present a method to create abstract cybersecurity test-case specifications from semi-formal threat models using attack trees.   
• We provide a method for utilizing Large Language Models (LLMs) to derive test cases from threat models and inferred state machines.   
• We present a method utilizing LLMs to derive security properties from threat models to model-check implemented state machines, determining the consistency of designs’ threat models and implementations’ state machines.