Paper 2019/564

Verification of Authenticated Firmware Load

Sujit Kumar Muduli, Pramod Subramanyan, and Sayak Ray

Abstract

An important primitive in ensuring security of modern systems-on-chip designs are protocols for authenticated firmware load. These loaders read a firmware binary image from an untrusted input device, authenticate the image using cryptography and load the image into memory for execution if authentication succeeds. While these protocols are an essential part of the hardware root of trust in almost all modern computing devices, verification techniques for reasoning about end-to-end security of these protocols do not exist. This paper takes a step toward addressing this gap by introducing a system model, adversary model and end-to-end security property that enable reasoning about the security of authenticated load protocols. We then present a decomposition of the security hyperproperty into two simpler 2-safety properties that enables more scalable verification. Experiments on a protocol model demonstrate viability of the methodology.

Note: v2.2.1 of the paper with revisions based on referee comments.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Minor revision. Formal Methods in Computer-Aided Design (FMCAD) 2019
Keywords
formal methodsformal verificationmodel checkingsecurebootauthenticated loadsecurity property specification
Contact author(s)
spramod @ cse iitk ac in
History
2019-08-20: last of 5 revisions
2019-05-27: received
See all versions
Short URL
https://ia.cr/2019/564
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/564,
      author = {Sujit Kumar Muduli and Pramod Subramanyan and Sayak Ray},
      title = {Verification of Authenticated Firmware Load},
      howpublished = {Cryptology {ePrint} Archive, Paper 2019/564},
      year = {2019},
      url = {https://eprint.iacr.org/2019/564}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.