Verification of Authenticated Firmware Loaders
| Autor: | Sujit Kumar Muduli, Pramod Subramanyan, Sayak Ray |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Authentication
business.industry Firmware Computer science Input device Cryptography 02 engineering and technology computer.software_genre 020202 computer hardware & architecture System model Embedded system Scalability 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing business Protocol (object-oriented programming) computer Adversary model |
| Zdroj: | FMCAD |
| DOI: | 10.23919/fmcad.2019.8894262 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|