Scientific knowledge map · Paper #46
PURE: Using Verified Remote Attestation to Obtain Proofs of Update, Reset and Erasure in Low-End Embedded Systems
2019 · IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
- Theory
- Applied
- protocol
Research question
What does the paper try to establish?
Can a verifier do more than detect compromise on a low-end embedded device—can it obtain trustworthy evidence that the device was updated, erased, reset, and returned to a functional malware-free state?
Central answer
What is the proposed answer?
PURE extends VRASED with three challenge-response services: Proof of Reset, Proof of Update, and Proof of Erasure. Security games and reductions tie valid proofs to the corresponding memory transition, modified trusted components are model-checked, and an OpenMSP430/Basys3 implementation adds about 0.4% registers and 50 bytes of trusted ROM.
Full paper abstract
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 Prv 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.
Provenance: Transcribed from the checked-in full-text PDF; calligraphic verifier/prover symbols were normalized to Vrf and Prv, and only typography, discretionary hyphenation, and line-break artifacts were otherwise normalized.
Evidence profile
Six dimensions, kept separate
The chart summarizes documented evidence and process. It is not a correctness probability, confidence score, or ranking, and no composite score is calculated.
LowMediumHighN/A = not assessed
A smaller value means less documented support for that dimension, not that the paper is false or unimportant.
- Epistemic evidence High
-
The full paper combines explicit games and reductions, model-checked trusted-component changes, a concrete FPGA implementation, resource/runtime evaluation, and public artifacts, while retaining clear trusted-boundary limits.
Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary FPGA resources, ROM/RAM, and runtime evaluation Public implementation and verification artifacts - Auditability High
-
A checked-in full paper with hash/page count, precise anchors, DOI, and public code/verification branch make assumptions and evidence inspectable; the exact artifact revision is not pinned.
Problem, architecture goal, contributions, and headline overhead Public implementation and verification artifacts Official peer-reviewed publication identity - Production provenance Medium
-
Authors, venue, DOI, predecessor architecture, toolchain, hardware platform, and repository are documented; roles, revision history, immutable artifact versions, and run provenance remain incomplete.
Official peer-reviewed publication identity Public implementation and verification artifacts FPGA resources, ROM/RAM, and runtime evaluation - External scrutiny High
-
ICCAD review plus inspectable model-checked components and public implementation provide multiple scrutiny surfaces; independent reproduction and public review reports were not found.
Official peer-reviewed publication identity Public implementation and verification artifacts - Reception High
-
OpenAlex reported 16 citations on 2026-07-11; under the finalized rubric, 11 or more located citations is High.
Dated citation-count snapshot - Contribution significance High
-
PURE turns verified compromise detection into a composable remote-remediation path with formal and concrete evidence for constrained devices; broad deployment and independent replication remain unaudited.
Problem, architecture goal, contributions, and headline overhead FPGA resources, ROM/RAM, and runtime evaluation
Assessment: Ai draft author review pending · 2026-07-11 · rubric 0.2. These dimensions describe documented support and process, not truth, correctness, or a universal ranking. No composite score is calculated.
Top-down and bottom-up view
Hierarchical knowledge map
Collapse a branch for a top-level reading, or follow its source links and child nodes to audit the evidence and boundaries underneath it.
PURE
A verified-attestation extension that gives a remote verifier cryptographic proofs of reset, update, and erasure on a low-end MCU.
Problem, architecture goal, contributions, and headline overhead-
question Research question
research questionAfter remote attestation detects compromise, can the verifier prove that remediation really changed all intended device state and restarted execution safely?
Problem, architecture goal, contributions, and headline overhead -
contribution Central answer
implemented and formally analyzedReuse VRASED's protected HMAC and hardware monitor to bind a fresh challenge to reset, update, or erasure transitions, then serially compose the three services.
VRASED architecture, LTL verification, and inherited RA game Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Proof-of-Erasure construction and helper-code caveat -
threat model Full software-compromise adversary
definedMalware controls the prover's writable memory and software execution, including code-reuse attempts and refusal to cooperate, but cannot violate protected hardware/ROM, extract the attestation key, or mount physical/fault attacks.
Full software-compromise adversary and physical/hardware assumptions -
assumption Trusted boundary
inherited and extendedGuarantees inherit VRASED's MCU-signal, reset, key, HMAC, compiler, and hardware-monitor assumptions; helper-code availability and verifier request authentication are separate operational concerns.
VRASED architecture, LTL verification, and inherited RA game Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Proof-of-Erasure construction and helper-code caveat -
protocol group Three remediation services specified verified and implemented
Each service has a security game and construction; only trusted-component changes are model-checked, while theorem proofs connect accepted HMAC evidence to the intended state transition.
Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Proof-of-Erasure construction and helper-code caveat-
protocol Proof of Reset (PoR)
implemented and model checkedTrusted code authenticates reset completion under a challenge, and hardware rules ensure that the proof is emitted only through the reset path before execution returns to unprivileged software.
Proof-of-Reset game, construction, theorem, and verified implementation -
protocol Proof of Update (PoU)
implemented and reduction provedUntrusted helper code writes target software S into region UR; VRASED then authenticates UR and request context so a valid proof is tied to the installed bytes, assuming request origin is authenticated when needed.
Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary -
protocol Proof of Erasure (PoE)
implemented and reduction reusedPoE specializes update to an all-zero target over the erased region; erasing all writable memory requires immutable or separately attested helper code to avoid hiding malware in an excluded region.
Proof-of-Erasure construction and helper-code caveat -
protocol Serial remediation sequence
composition argumentUpdate program memory, erase residual writable state, then reset so the verifier obtains evidence of new code, cleared old data, and reinitialized control flow.
Problem, architecture goal, contributions, and headline overhead Serial-composition conclusion and future directions
-
-
claim group Principal claims mixed formal and empirical
PURE claims game-based service security, formal conformance of modified trusted hardware, low incremental footprint, and practical runtime.
Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary FPGA resources, ROM/RAM, and runtime evaluation-
claim Accepted proofs imply intended transitions
proved conditionalUnder VRASED/HMAC assumptions, an adversary cannot produce accepted PoR or PoU/PoE evidence without taking the corresponding reset or memory-state action except with negligible probability.
Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Proof-of-Erasure construction and helper-code caveat -
claim Modified trusted logic satisfies LTL policies
model checked within rtl modelAdditional reset-operation state and DMA/execution rules are translated to NuSMV and checked as extensions to VRASED's hardware monitor; this is not verification of every MCU component.
VRASED architecture, LTL verification, and inherited RA game Proof-of-Reset game, construction, theorem, and verified implementation -
claim Small incremental cost
experimentally supportedRelative to VRASED, PURE adds 4 LUTs, 3 registers, about 50 bytes of trusted ROM, and 26 bytes of helper code; PoR takes 26 ms at 8 MHz and update/erasure scale linearly with memory size.
FPGA resources, ROM/RAM, and runtime evaluation
-
-
evidence group Evidence stack
formal artifact and fpga measurementSecurity games and theorem arguments, NuSMV checks of added trusted logic, an OpenMSP430/Basys3 FPGA implementation, resource synthesis, runtime measurements, and a public code branch jointly support the claims.
Proof-of-Reset game, construction, theorem, and verified implementation Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary FPGA resources, ROM/RAM, and runtime evaluation Public implementation and verification artifacts -
limitation group Security and deployment boundaries
materialA valid proof does not authenticate who requested a malicious update unless verifier authentication is enabled; writable helper code can be erased or infected; physical attacks, faults, and the complete MCU are outside the model.
Full software-compromise adversary and physical/hardware assumptions Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Proof-of-Erasure construction and helper-code caveat -
artifact group Implementation and verification artifacts
public unpinnedThe paper and PURE repository branch are public. This map records no immutable repository revision, build transcript, model-check log, FPGA bitstream hash, or independent reproduction.
Public implementation and verification artifacts FPGA resources, ROM/RAM, and runtime evaluation -
scrutiny External scrutiny
venue reviewed with machine checked componentsICCAD publication and public formal/implementation artifacts provide substantial exposure, but no public review reports or independent end-to-end verification were located.
Official peer-reviewed publication identity Public implementation and verification artifacts -
lineage VRASED extension
explicitPURE is downstream of VRASED (#50): it reuses VRASED's verified attestation TCB and HMAC path, adding remediation states and services rather than replacing the base architecture.
VRASED architecture, LTL verification, and inherited RA game Problem, architecture goal, contributions, and headline overhead
Audit trail
Source index
Locators state the depth of the current audit. PDF page numbers, where present, are one-based file pages; metadata-, summary-, and abstract-bounded records explicitly identify their limitations.
- Problem, architecture goal, contributions, and headline overhead Abstract and Section 1, PDF pages 1-2
- VRASED architecture, LTL verification, and inherited RA game Section 3, PDF pages 2-4
- Full software-compromise adversary and physical/hardware assumptions Section 4, PDF page 4
- Proof-of-Reset game, construction, theorem, and verified implementation Section 5, PDF pages 4-6
- Proof-of-Update game, construction, theorem, request authentication, and helper-code boundary Section 6, PDF pages 6-7
- Proof-of-Erasure construction and helper-code caveat Section 7, PDF page 7
- FPGA resources, ROM/RAM, and runtime evaluation Section 8, Table 2 and Figure 5, PDF pages 7-8
- Serial-composition conclusion and future directions Section 9, PDF page 8
- Public implementation and verification artifacts PURE repository branch, accessed 2026-07-11
- Official peer-reviewed publication identity ICCAD 2019, DOI 10.1109/ICCAD45719.2019.8942118
- Dated citation-count snapshot OpenAlex reported 16 citing works on 2026-07-11