面向汽车网络架构的分层痕迹过程分析：实现可扩展的形式化安全验证
密码学与安全
2026-05-06 v2
摘要
汽车领域正发生转型：车辆作为滚动的服务器，持续连接到众多外部实体。这种连接性，加上日益增长的车载计算功力以支持先进驾驶辅助系统等类似用例，正在为Securing汽车网络架构带来日益严峻的挑战。本工作推进了针对Internet连接汽车网络架构及其协议的安全分析。我们引入了一个专为汽车领域量身定制的强大、主动的对手模型。我们通过引入一种验证调度算法，大幅扩展了基于攻击韧性超属性（Attack Resilience Hyperproperties, ARHs）的安全协议验证能力。此外，我们提供了将安全属性失效进行比较归因的方法，将其归因于具体的、更细粒度的组件妥协。我们提出了一种形式化验证与过程挖掘的新型集成方法。通过利用ARH反例痕迹进行过程挖掘，我们系统性地识别并聚合导致安全属性失效的攻击者行为。该管道使我们能够深入理解导致协议安全失效的根本原因和攻击路径。我们通过在汽车网络架构中实现电池管理系统数据安全传输的原型和案例研究，展示了其实际应用性。
引用
@article{arxiv.2604.21606,
title = {Process-Mining of Hypertraces: Enabling Scalable Formal Security Verification of (Automotive) Network Architectures},
author = {Julius Figge and David Knuplesch and Andreas Maletti and Dragan Zuvic},
journal= {arXiv preprint arXiv:2604.21606},
year = {2026}
}
备注
Full version prior to submission for publication