Scientific knowledge map · Paper #54

APEX: A Verified Architecture for Proofs of Execution on Remote Devices Under Full Software Compromise

Ivan De Oliveira Nunes, Karim Eldefrawy, Norrathep Rattanavipanon, and Gene Tsudik

2020 · 29th USENIX Security Symposium

Theory
Applied
protocol
primitive

Research question

What does the paper try to establish?

Can a low-end embedded device under complete software compromise prove to a remote verifier that specified software ran atomically and produced an authentic fresh output?

Central answer

What is the proposed answer?

APEX defines a proof-of-execution security game and extends the verified VRASED attestation architecture with hardware-enforced execution, output, and metadata invariants. The design is model checked, implemented on OpenMSP430 and an FPGA, released as an artifact, and evaluated with low measured hardware overhead.

Full paper abstract

Abstract

Modern society is increasingly surrounded by, and is growing accustomed to, a wide range of Cyber-Physical Systems (CPS), Internet-of-Things (IoT), and smart devices. They often perform safety-critical functions, e.g., personal medical devices, automotive CPS as well as industrial and residential automation, e.g., sensor-alarm combinations. On the lower end of the scale, these devices are small, cheap and specialized sensors and/or actuators. They tend to host small anemic CPUs, have small amounts of memory and run simple software. If such devices are left unprotected, consequences of forged sensor readings or ignored actuation commands can be catastrophic, particularly, in safety-critical settings. This prompts the following three questions: (1) How to trust data produced, or verify that commands were performed, by a simple remote embedded device?, (2) How to bind these actions/results to the execution of expected software? and, (3) Can (1) and (2) be attained even if all software on a device can be modified and/or compromised? In this paper we answer these questions by designing, demonstrating security of, and formally verifying, APEX: an Architecture for Provable Execution. To the best of our knowledge, this is the first of its kind result for low-end embedded systems. Our work has a range of applications, especially, authenticated sensing and trustworthy actuation, which are increasingly relevant in the context of safety-critical systems. APEX is publicly available and our evaluation shows that it incurs low overhead, affordable even for very low-end embedded devices, e.g., those based on TI MSP430 or AVR ATmega processors.

Provenance: Transcribed from the checked-in full-text PDF; only typography, discretionary hyphenation, and line-break artifacts were normalized. Unusual source punctuation in the three numbered questions is preserved.

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 source combines a formal security game, machine-checked hardware invariants, a reduction argument, synthesizable implementation, measured overheads, and an end-to-end proof of concept, while clearly stating its assumptions and exclusions.
Proof-of-execution syntax and security game LTL specification, model checking, and PoX proof argument OpenMSP430 implementation and evaluation Limitations and future directions
Auditability High: A checked-in author copy with fixity metadata, official open-access record, public code, formal specifications, and represented artifact badge make the evidence highly inspectable.
Motivation, questions, and claimed contribution Public implementation repository USENIX publication and artifact record
Production provenance Medium: Authors, venue, source copy, public repository, platform, and verification stack are documented, but contributor roles and exact commit-to-paper build provenance are not fully captured in this map.
Public implementation repository USENIX publication and artifact record
External scrutiny High: Publication at USENIX Security plus the Artifact Evaluated - Passed badge provides both venue and artifact scrutiny; private review reports and independent proof rechecking remain unavailable.
USENIX publication and artifact record
Reception High: The dated exact-title OpenAlex record located 38 citations. Under the author-defined corpus rule, 11 or more located citations is High; the count remains index- and date-dependent.
Dated citation-count snapshot
Contribution significance High: The work defines and realizes a new low-end proof-of-execution service with formal and concrete evidence, and the citation snapshot indicates substantial uptake. Priority and correctness are still not guaranteed by this rating.
Motivation, questions, and claimed contribution Conclusion Dated citation-count snapshot

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.

paper