Search papers, labs, and topics across Lattice.
This paper introduces a novel approach to security verification of automotive network architectures by integrating formal verification with process mining. They use Attack Resilience Hyperproperties (ARHs) and a verification-orchestration algorithm to identify security vulnerabilities under a strong, active adversary model. By applying process mining to ARH counterexample traces, the method systematically identifies and aggregates attacker behaviors that lead to security property invalidations, enabling a deeper understanding of root causes and attack paths.
Uncover hidden attack patterns in automotive networks by combining formal verification with process mining, revealing root causes of security vulnerabilities that traditional methods miss.
The automotive domain is transitioning: vehicles act as rolling servers, persistently connected to numerous external entities. This connectivity, combined with rising on-board computing power for advanced driver assistance systems and similar use cases, creates escalating challenges for securing automotive network architectures. This work advances the security analysis of internet-connected automotive network architectures and their protocols. We introduce a strong, active adversary model tailored to the automotive domain. We substantially extend security protocol verification possible based on Attack Resilience Hyperproperties (ARHs) by introducing a verification-orchestration algorithm. Furthermore, we provide methods for comparative attribution of security property invalidations to specific, ne-grained component compromises. We present a novel integration of formal verification and process mining. By utilizing ARH counterexample traces for process mining, we systematically identify and aggregate attacker behavior that causes security property invalidations. This pipeline enables in-depth understanding of root causes and attack paths leading to protocol-security invalidations. We demonstrate real-world applicability through a prototype and case study on the secure transmission of battery management system data within an automotive network architecture.
