| Title | PURE: Using Verified Remote Attestation to Obtain Proofs of Update, Reset and Erasure in low-End Embedded Systems |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | De Oliveira Nunes, Ivan, ElDefrawy, Karim, Rattanavipanon, Norrathep, Tsudik, Gene |
| Conference Name | 2019 IEEE/ACM International Conference on Computer-Aided Design (ICCAD) |
| Keywords | attestation, composability, compromised state, current memory state, Embedded systems, erasure, formally verified RA architecture, functional state, Human Behavior, important security services, invasive software, low-end embedded devices, low-end embedded systems, malware-free state, microcontrollers, obtain proofs, provably secure software update, Prv memory, pubcrawl, remote Prv, Resiliency, secure RA architecture, security service, software state, system-wide resets, trusted verifier, untrusted remote prover, useful security services, verified remote attestation, VRASED, VRF |
| Abstract | Remote Attestation ( RA) is a security service that enables a trusted verifier ( Vrf) to measure current memory state of an untrusted remote prover ( Prv). If correctly implemented, RA allows Vrf to remotely detect if Prv's memory reflects a compromised state. However, RA by itself offers no means of remedying the situation once P rv is determined to be compromised. In this work we show how a secure RA architecture can be extended to enable important and useful security services for low-end embedded devices. In particular, we extend the formally verified RA architecture, VRASED, to implement provably secure software update, erasure, and system-wide resets. When (serially) composed, these features guarantee to Vrf that a remote Prv has been updated to a functional and malware-free state, and was properly initialized after such process. These services are provably secure against an adversary (represented by malware) that compromises Prv and exerts full control of its software state. Our results demonstrate that such services incur minimal additional overhead (0.4% extra hardware footprint, and 100-s milliseconds to generate combined proofs of update, erasure, and reset), making them practical even for the lowest-end embedded devices, e.g., those based on MSP430 or AVR ATMega micro-controller units (MCUs). All changes introduced by our new services to VRASED trusted components are also formally verified. |
| DOI | 10.1109/ICCAD45719.2019.8942118 |
| Citation Key | de_oliveira_nunes_pure_2019 |
PURE: Using Verified Remote Attestation to Obtain Proofs of Update, Reset and Erasure in low-End Embedded Systems