PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot

TL;DR

PA-Boot tackles a new hardware supply-chain threat that can bypass multiprocessor secure boot by compromising processors or inter-processor channels. It presents PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems, with a full Isabelle/HOL formalization and a mechanized security proof, complemented by a C-based CPA-Boot prototype. Experimental validation on ARM Fixed Virtual Platform shows effective detection of AP replacements and man-in-the-middle attacks with a modest boot overhead of $4.98\%$. The work bridges high-assurance formal verification with practical deployment through a validation framework that extracts executable code from the model and tests it against the implementation. This approach enhances boot-time security for critical multiprocessor devices without requiring new hardware components.

Abstract

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.

Figures (7)

• Figure 1: Key components in multiprocessor secure boot.
• Figure 2: Threat model of PA-Boot. marks potential vulnerabilities to adversarial behaviors \ref{['attack-AP']} and \ref{['attack-chip']} in multiprocessor secure boot. Components of PA-Boot are colored in yellow.
• Figure 3: The workflow of our approach. ✓ indicates verified properties encoding security and functional correctness.
• Figure 4: Key message flows in PA-Boot. marks potential vulnerabilities to adversarial behaviors \ref{['attack-AP']} and \ref{['attack-chip']}.
• Figure 5: Snippets of the state machine $\mathcal{S}_l$ of PA-Boot. A state $s$ is identified by its status and colored in light green (normal termination), red (abnormal termination), or in blue, dark green, yellow, or orange if the transition to $s$ is triggered by BSP, AP, both BSP and AP, or the attacker, respectively; The (condensed) transition $;; \ldots \!\rightarrow\! \top$, for $p,q \in \{3, 4, 8\}$ (cf. \ref{['tab:behaviors']}), is triggered if all the checks in the event sequence $,,\ldots$ are successful, otherwise $;; \ldots \!\rightarrow\! \bot$ is triggered.

Theorems & Definitions (6)

• Remark 1
• Definition 1: High-Level Specification of PA-Boot
• Lemma 1: Functional Correctness w.r.t. $\mathcal{S}_l$
• Lemma 1: Security w.r.t. $\mathcal{S}_l$ under Normal Executions
• Lemma 2: Security w.r.t. $\mathcal{S}_l$ against Tampered Configurations
• Lemma 3: Security w.r.t. $\mathcal{S}_l$ against Man-in-the-Middle Attacks