Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures

TL;DR

This paper introduces a novel integration of formal verification and process mining to analyze security vulnerabilities in automotive network architectures, enabling scalable and detailed security analysis.

Contribution

It extends security protocol verification with a verification-orchestration algorithm and applies process mining to attack traces for root cause analysis in automotive security.

Findings

Demonstrated real-world applicability with a prototype and case study.

Enabled systematic identification of attacker behavior causing security invalidations.

Extended security verification methods for automotive network protocols.

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.