PA-Boot：一种用于多处理器安全启动的形式化验证认证协议
密码学与安全
2025-04-22 v3 硬件体系结构
摘要
硬件供应链攻击对多处理器系统的启动过程构成了重大的安全威胁。本文指出了一种新的、普遍存在的硬件供应链攻击面，由于缺少处理器认证机制，该攻击面可绕过多处理器安全启动。为防御此类攻击，我们提出 PA-Boot，这是首个针对多处理器系统安全启动的形式化验证处理器认证协议。PA-Boot 被证明功能正确，并保证能检测多种对抗行为，例如处理器替换、中间人攻击以及证书篡改。PA-Boot 的细粒度形式化及其完全机械化的安全证明在 Isabelle/HOL 定理证明器中完成，包含 306 个引理/定理以及约 7,100 行代码。基于概念验证实现的实验表明，PA-Boot 能以相当小的开销有效识别启动过程攻击，从而提升多处理器系统的安全性。
引用
@article{arxiv.2209.07936,
title = {PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot},
author = {Zhuoruo Zhang and Rui Chang and Mingshuai Chen and Wenbo Shen and Chenyang Yu and He Huang and Qinming Dai and Yongwang Zhao},
journal= {arXiv preprint arXiv:2209.07936},
year = {2025}
}