Cryptology ePrint Archive: Report 2019/564

Verification of Authenticated Firmware Load

Sujit Kumar Muduli and 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.

In this paper, we take 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 property into two simpler hyperproperties. This decomposition enables more scalable verification. Experiments on a protocol model demonstrate viability of the methodology.

Category / Keywords: foundations / formal methods, formal verification, model checking, secureboot, authenticated load, security property specification

Date: received 25 May 2019, last revised 10 Jun 2019

Contact author: spramod at cse iitk ac in

Available format(s): PDF | BibTeX Citation

Note: v2.0 of the paper with improved results and several typos fixed.

Version: 20190611:055422 (All versions of this report)

Short URL: ia.cr/2019/564