We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.CR

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Cryptography and Security

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

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.
Comments: Manuscript submitted to IEEE Trans. Dependable Secure Comput
Subjects: Cryptography and Security (cs.CR); Hardware Architecture (cs.AR)
Cite as: arXiv:2209.07936 [cs.CR]
  (or arXiv:2209.07936v1 [cs.CR] for this version)

Submission history

From: Mingshuai Chen [view email]
[v1] Fri, 16 Sep 2022 13:54:43 GMT (8674kb,D)

Link back to: arXiv, form interface, contact.