Formal Methods-Based Security Testing Utilizing Threat Modeling, Automata Learning, and Model Checking

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.