PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
arXiv (Cornell University)(2022)
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.
MoreTranslated text
Key words
verified authentication protocol,multiprocessor
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined