Formally Verified Hardware/Software Co-Design for Remote Attestation

TL;DR

This paper introduces VRASED, the first formally verified hardware/software co-designed architecture for remote attestation, ensuring security for low-end embedded devices with minimal hardware costs.

Contribution

It presents the first formal verification of a remote attestation scheme combining hardware and software, applicable to simple IoT devices.

Findings

VRASED achieves security comparable to hardware-based approaches.

The implementation on TI MSP430 demonstrates low overhead.

Deployment on FPGA shows practical feasibility.

Abstract

In this work, we take the first step towards formal verification of Remote Attestation (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's publicly available implementation was deployed on the Basys3 FPGA.