Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures
Julius Figge, David Knuplesch, Andreas Maletti, Dragan Zuvic
TLDR
This paper introduces process mining of hypertraces for scalable formal security verification of automotive network architectures, enhancing root cause analysis.
Key contributions
- Introduces a strong, active adversary model specifically for automotive network security analysis.
- Extends security protocol verification using Attack Resilience Hyperproperties (ARHs) with a new orchestration algorithm.
- Provides methods for attributing security property invalidations to specific component compromises.
- Integrates formal verification and process mining to identify and aggregate attacker behavior from ARH counterexamples.
Why it matters
As automotive networks become more complex and connected, securing them is critical. This work provides a novel, scalable approach to formally verify security, offering deep insights into attack paths and root causes of vulnerabilities.
Original Abstract
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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.