Remote Attestation (RA) is a security service that allows a trusted verifier (Vrf) to measure the software state of an untrusted remote device -- Prv. If correctly implemented, RA allows Vrf to remotely detect if Prv is in an illegal or compromised state. Although several RA architectures have been proposed, little attention has been devoted to their verifiability and security guarantees that can be derived through formal verification of RA architectures.
In this talk we introduce 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. Since VRASED 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. It is also the first formal verification of a HW/SW implementation of any security service. VRASED's publicly available implementation was deployed on the Basys3 FPGA and requires 16x fewer Look-Up Tables and 36x fewer registers than the cheapest pure HW-based design.