论文标题
PA-Boot：多处理器安全启动的正式验证的身份验证协议
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
论文作者
论文摘要
硬件供应链攻击正在引起对多处理器系统引导过程的重大安全威胁。本文确定了一种新的，普遍的硬件供应链攻击表面，由于缺乏处理器认证机制，可以绕过多处理器安全引导。为了防止此类攻击，我们提出了PA-Boot，这是第一个在多处理器系统中安全启动的正式验证的处理器认证协议。 PA-boot在功能上被证明是正确的，并保证可以检测多种对抗行为，例如处理器更换，中间攻击和用证书篡改。 PA-boot的细粒度形式化及其完全机械化的安全性证明是在Isabelle/Hol定理供摊厂中进行的，具有306个引理/定理和〜7,100 LOC。对概念验证实现的实验表明，PA-Boot可以有效地识别带有相当小的开销的启动过程攻击，从而提高了多处理器系统的安全性。
Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. This paper identifies a new, prevalent hardware supply-chain attack surface that can bypass multiprocessor secure boot due to the absence of processor-authentication mechanisms. To defend against such attacks, we present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems. PA-Boot is proved functionally correct and is guaranteed to detect multiple adversarial behaviors, e.g., processor replacements, man-in-the-middle attacks, and tampering with certificates. The fine-grained formalization of PA-Boot and its fully mechanized security proofs are carried out in the Isabelle/HOL theorem prover with 306 lemmas/theorems and ~7,100 LoC. Experiments on a proof-of-concept implementation indicate that PA-Boot can effectively identify boot-process attacks with a considerably minor overhead and thereby improve the security of multiprocessor systems.
