VRASED: A Verified Hardware/Software Co-Design for Remote Attestation

Authors: 

Ivan De Oliveira Nunes, University of California, Irvine; Karim Eldefrawy, SRI International; Norrathep Rattanavipanon, University of California, Irvine; Michael Steiner, Intel; Gene Tsudik, University of California, Irvine

Abstract: 

Remote Attestation (RA) is a distinct security service that allows a trusted verifier ( Vrf) to measure the software state of an untrusted remote prover ( Prv). If correctly implemented, RA allows Vrf to remotely detect if Prv is in an illegal or compromised state. Although several RA approaches have been explored (including hardware-based, software-based, and hybrid) and many concrete methods have been proposed, comparatively little attention has been devoted to formal verification. In particular, thus far, no RA designs and no implementations have been formally verified with respect to claimed security properties.

In this work, we take the first step towards formal verification of RA by designing and verifying an architecture called VRASED: Verifiable Remote Attestation for Simple Embedded Devices. VRASED instantiates a hybrid (HW/SW) RA co-design aimed at low-end embedded systems, e.g., simple IoT devices. VRASED provides a level of security comparable to HW-based approaches, while relying on SW to minimize additional HW costs. Since security properties must be jointly guaranteed by HW and SW, verification is a challenging task, which has never been attempted before in the context of RA. We believe that VRASED is the first formally verified RA scheme. To the best of our knowledge, it is also the first formal verification of a HW/SW implementation of any security service. To demonstrate VRASED’s practicality and low overhead, we instantiate and evaluate it on a commodity platform (TI MSP430). VRASED was deployed using the Basys3 Artix-7 FPGA and its implementation is publicly available.

USENIX Security '19 Open Access Videos Sponsored by
King Abdullah University of Science and Technology (KAUST)

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {236230,
author = {Ivan De Oliveira Nunes and Karim Eldefrawy and Norrathep Rattanavipanon and Michael Steiner and Gene Tsudik},
title = {{VRASED}: A Verified Hardware/Software Co-Design for Remote Attestation},
booktitle = {28th {USENIX} Security Symposium ({USENIX} Security 19)},
year = {2019},
isbn = {978-1-939133-06-9},
address = {Santa Clara, CA},
pages = {1429--1446},
url = {https://www.usenix.org/conference/usenixsecurity19/presentation/de-oliveira-nunes},
publisher = {{USENIX} Association},
month = aug,
}

Presentation Video