Pith. sign in

REVIEW 3 major objections 4 minor 66 references

A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read VAPE is a formally verified architecture that lets a remote verifier obtain an unforgeable proof that a low-end device executed a specified program atomically and that its reported output came from that execution, even if all device…

desk verdict VAPE is the first credible low-cost PoX architecture, but the proof as written doesn't bind OR contents to execution, and LTL 9 has a self-contradictory typo. read the letter →

arxiv 1908.02444 v2 pith:YSN4BRM6 submitted 2019-08-07 cs.CR

Ivan De Oliveira Nunes , Karim Eldefrawy , Norrathep Rattanavipanon , Gene Tsudik This is my paper · ORCID
classification cs.CR
keywords proofsofexecutionremoteattestationlow-endembeddeddevicesformalverificationlineartemporallogicmodelcheckingauthenticatedsensinghardwaresecurityarchitecture
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

VAPE is an architecture that gives a remote verifier an unforgeable proof that a low-end microcontroller executed a requested program in full, from its first to its last instruction, and that any returned output came from that execution, even if all software on the device is malicious. The paper's central claim is that this Proof-of-Execution guarantee reduces to the already-verified security of a remote attestation architecture: VAPE hardware maintains a one-bit EXEC flag, sets it only when the monitored CPU signals show atomic execution and intact code, metadata, and output regions, and folds that flag into the memory covered by the attestation MAC. If the claim is right, a verifier can trust both the fact of execution and the authenticity of results on devices as weak as an MSP430 or ATMega, without needing trusted software, a TPM, or control-flow attestation. The paper supports the claim with a machine model, linear-temporal-logic invariants checked by model checking, a computer-checked implication proof, and an FPGA implementation reporting roughly 2% register and 12% LUT overhead.

What carries the argument

The load-bearing object is the EXEC flag and the hardware module that computes it from seven monitored signals: PC, memory read/write enables and addresses, DMA enable and address, and the interrupt signal. The flag is read-only to software and is included as part of the attested metadata region. Ten LTL invariants, numbered 3 through 12 in Definition 6, capture the required behavior: immutable code during and after execution, atomic entry at the first instruction and exit only at the last instruction, no interrupts during execution, protection of the output and metadata regions, sane region bounds, reset clearing EXEC, and the rule that the only way EXEC returns to 1 is a fresh start at the first instruction. An automated model checker verifies each Verilog sub-module against these invariants; a theorem-prover proof shows their conjunction implies the formal correctness definition; and a cryptographic reduction shows that underlying RA security plus EXEC correctness implies PoX security. The mechanism's work is to make the attestation MAC a witness to execution state rather than merely to memory contents.

What would settle it

On the FPGA implementation, load a program into the execution region and, while the CPU is inside that region, have DMA write to an instruction word in the region; if the resulting attestation still verifies with EXEC=1, the DMA invariant is not enforced. A second check is to trigger an interrupt in the middle of execution, return to a different instruction inside the execution region, and see whether any accepted proof can be produced; a valid proof would contradict the atomicity invariant.

Watch

Extended reading notes

Core claim

The discovery is that secure Proofs of Execution can be built for low-end MCUs by enforcing a small set of temporal invariants in hardware and binding them to an existing verified remote-attestation MAC. VAPE's hardware watches the program counter, memory read/write enables and addresses, DMA enable and address, and interrupt signal, and maintains a software-unwritable EXEC flag. EXEC starts at 0, becomes 1 only when the PC enters the execution region at its first instruction under no violation, and drops to 0 on any write to the code region or metadata, any interrupt or reset during execution, any out-of-range PC transition, or any DMA access or activity during execution. The attested memory includes the execution region, the output region, and the metadata region holding the challenge and region bounds, so the HMAC-based proof is valid only if EXEC is 1 at attestation time. The paper proves that the LTL invariants plus the machine model imply this EXEC correctness, and that this correctness, composed with the security of the underlying verified remote-attestation module, implies the formal PoX security definition.

Load-bearing premise

The CPU architecture strictly adheres to and correctly implements its specification, so the monitored PC, memory-access, DMA, and interrupt signals always truthfully reflect the operations the silicon actually performs and no relevant operation goes unmodeled.

Editorial extensions

If this is right

  • A verifier can trust both that the requested code ran and that the returned output is authentic, with no Trusted Platform Module, trusted hypervisor, or control-flow enumeration required.
  • Verification of a proof costs no more than verifying a standard remote-attestation response for the same code, because the proof is the attested MAC over the code, output, and metadata.
  • Proofs are bound to the challenge window, so old recordings of valid executions cannot be replayed as fresh responses.
  • Authenticated sensing and actuation follow directly: sensor readings or actuation writes placed in the output region are covered by the same unforgeable MAC, so malware cannot report fabricated values or ignore commands without detection.
  • The architecture adds no instructions and no ISA changes, so existing MSP430 and ATMega-class software can be made PoX-capable with modest linker and entry-exit transformation, at roughly 2% additional registers and 12% additional LUTs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Interrupt-driven and real-time code could be supported by extending the invariants to require that all interrupt handlers be immutable and included in the attested region; the paper sketches this as a relaxation but does not verify it.
  • The same EXEC-flag-plus-attestation pattern could be combined with control-flow measurements to certify not only that a program ran but which path it took; that would add hardware cost the paper avoids.
  • The guarantees are only as strong as the signal-interface fidelity: a concrete chip that latches, filters, or suppresses the monitored signals could break the proof despite a pristine LTL model, so testing the synthesized design under fault injection would be a natural next step.
  • Because the security reduction bottoms out in the underlying remote-attestation module's MAC security, replacing the cryptographic core with a different MAC would require re-verifying the RA composition, not just VAPE's hardware invariants.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces VAPE, a hardware/software architecture that augments the formally verified VRASED remote-attestation design to provide remote proofs of execution (PoX) on low-end MCUs under full software compromise. The authors formalize a PoX security game, specify a set of LTL invariants for the VAPE hardware, model-check the Verilog implementation with NuSMV, compose the LTL invariants into an end-to-end correctness condition via a SPOT proof, and reduce VAPE security to VRASED security in Appendix B. They also report an FPGA implementation on MSP430 with modest hardware overhead and a proof-of-concept fire-sensor application. The paper claims to be the first verified PoX architecture for low-end embedded devices.

Significance. If the security claim holds, this is a valuable contribution: it extends formally verified remote attestation to proof-of-execution with authenticated outputs, an important primitive for trustworthy sensing and actuation in low-end CPS/IoT devices. The strengths of the paper include the public RTL implementation, the use of model checking and a theorem prover for the hardware invariants, the explicit composition with a previously verified RA architecture, and the concrete evaluation on real hardware. The overhead figures (2% registers, 12% LUTs) are compelling. However, the formal guarantee as stated has a gap concerning the provenance of OR contents, and at least one printed LTL formula is inconsistent with its stated purpose. These issues affect the central security theorem and must be resolved before the claims can be accepted.

major comments (3)
  1. [§5.2/§6.3/Appendix B] The formal correctness condition and the enforced LTL properties do not require OR to be written during ER execution. Definition 5 condition 4 and LTL 7 constrain OR modifications only after the state S0 in which PC=ERmin; neither prohibits pre-loading OR contents before execution starts. An adversary with full software control can therefore pre-load OAdv into OR while EXEC=0, then execute any S that never stores to OR (for example, a trivial ER consisting of a jump from ERmin to ERmax). All LTL properties 3–12 are satisfied, EXEC becomes 1, the attestation covers OAdv, and XVerify accepts the pair (H,OAdv). But OAdv was not produced by XAtomicExec, whose output for this S is empty, so Definition 2 case (b) is violated. The reduction in Appendix B only rules out modification of OR after execution completes (Cond3) and does not address pre-execution placement. The paper must either add a mechanism and invariant that makes OR contents execution-derived (e.g., hardware zeroization of OR at ERmin, or a requirement that every OR byte is written during execution), or weaken the security definition; with the current properties the PoX guarantee does not follow.
  2. [Definition 6, LTL 9] LTL 9 is printed as G{ERmin≤CRmax ∨ ERmax>CRmax → ¬EXEC}. Because the antecedent is a disjunction, any pair of non-overlapping ER and CR regions satisfies at least one disjunct (if ER lies below CR, then ERmin≤CRmax; if ER lies above CR, then ERmax>CRmax), so the formula forces EXEC=0 in every valid configuration. This cannot be the intended 'ER and CR do not overlap' property and, as printed, would make every proof of execution invalid. The authors should correct the formula (likely to a conjunction or a negated overlap condition) and re-run the NuSMV verification and the SPOT proof of Theorem 1.
  3. [Definition 4 and Appendix B] Definition 4 states that MR, CR, AR, KR, XS, and METADATA are non-overlapping memory regions, but the construction and the reduction in Appendix B instantiate AR as a region containing ER, OR, and METADATA (METADATA⊂AR). If AR is the VRASED attested region, it must overlap METADATA; if AR is instead a separate fixed region, the reduction's use of AR as the attested union is inconsistent with the machine model. This needs to be resolved in the formal notation before the composition theorem can be assessed.
minor comments (4)
  1. [Abstract/§1] There are several typos, e.g., 'ARV ATMega' should be 'AVR ATmega' and 'commads' should be 'commands'; these should be corrected in a revision.
  2. [§6.3] The notation X(PC)∈ER is used without definition; the surrounding text should define X(PC) as the value of the program counter in the next cycle for clarity.
  3. [§6.3/Figure 3] Figure 3 refers to t(CRmax) and Hready, but these quantities are not defined in the caption or the surrounding text; a short explanation would improve readability.
  4. [§7.2] The caption of Figure 4c states that VAPE's dedicated RAM corresponds to VRASED's exclusive stack, but this is not explained in the text; clarify what is being compared.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the security proof is a compositional reduction to VRASED's independently machine-checked RA property, not an input-equivalent derivation.

full rationale

The derivation chain is: (1) formal LTL properties 3-12 imply Definition 5 (Theorem 1); and (2) Definition 5 plus VRASED's RA security implies the PoX security game (Theorem 2). Step (1) is a machine-checked implication over a stated machine model; Definition 5 is not stipulated to be the same formula as LTLs 3-12, and no empirical parameter is fitted. Step (2) is a cryptographic reduction: any PoX adversary is converted into an adversary against VRASED's RA game, and VRASED is a published, formally verified architecture whose assumptions (monitored bus signals, ROM SW-Att, HMAC) do not include PoX; under the stated rules this citation is independent support and does not raise the circularity score. The pre-load-OR concern is a soundness gap in Definition 5, not a circularity: the proof treats OR contents as execution-produced because OR is never modified outside ER execution, but Definition 5 never requires OR to be written during ER execution. This is an unmodeled attack, not an equivalence between output and input by construction.

Assumptions & free parameters 0 free parameters · 6 assumptions · 3 invented entities

No numerical free parameters. The central result rests on the monitored-signal machine model, VRASED security, HMAC security, and tool correctness, all listed as axioms.

assumptions (6)
  • domain assumption CPU architecture strictly adheres to and correctly implements its specification, including PC, memory access, DMA, reset, and interrupt signals (axioms A1-A5)
    Section 4.2 states this explicitly; VAPE's hardware monitors these signals, so if the CPU violates its specification, EXEC may be set incorrectly.
  • domain assumption VRASED is a secure remote attestation architecture per Definition 7
    Theorem 2 assumes VRASED security; VRASED is prior work by overlapping authors with independent formal verification.
  • standard math HMAC is an existentially unforgeable MAC under KDF-derived keys
    Used in the cryptographic reduction in Appendix B; standard assumption for secure MAC constructions.
  • domain assumption The machine model in Definition 4 captures all MCU behaviors relevant to memory modification (Wen/Daddr, DMAen/DMAaddr, interrupts)
    The LTL verification is only as strong as this model; attacks using mechanisms not covered are out of scope.
  • domain assumption Memory regions MR, CR, AR, KR, XS, and METADATA are non-overlapping
    Definition 4.3 requires disjoint regions so that the attestation binds all sensitive regions into AR.
  • standard math Formal verification tools (NuSMV, Verilog2SMV, SPOT) are correct
    The paper relies on these tools without proving their correctness, which is standard practice.
invented entities (3)
  • VAPE hardware module (HW-Mod extension)
    purpose: Monitors PC, memory access, DMA, and interrupt signals and enforces LTL properties by setting EXEC=0 on violations; ensures atomic execution and memory immutability for proof of execution.
    New hardware component; evidence is the paper's own verification and FPGA synthesis, with no external falsifiable prediction.
  • EXEC flag
    purpose: 1-bit hardware flag included in the attestation HMAC; set to 1 only after a clean atomic execution of the executable region and reset to 0 on any violation.
    New internal state bit with no external measurable prediction beyond the architecture's own behavior.
  • METADATA memory region
    purpose: Memory-mapped peripheral storing ERmin, ERmax, ORmin, ORmax, Chal, and EXEC; EXEC is read-only to software and the region is monitored by VAPE to bind execution parameters to the proof.
    New architectural region that is an implementation detail of VAPE.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise." pith.science (2026). https://pith.science/paper/YSN4BRM6

@misc{pith2026190802444,
  author       = {Pith},
  title        = {Pith review of: A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YSN4BRM6}},
  note         = {Machine review of arXiv:1908.02444}
}
read the original abstract

Modern society is increasingly surrounded by, and 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 and industrial automation (smart factories). Some devices are small, cheap and specialized sensors and/or actuators. They tend to run simple software and operate under control of a more sophisticated central control unit. The latter is responsible for the decision-making and orchestrating the entire system. If 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 by a simple remote embedded device? and (2) How to ascertain that this data was produced via execution of expected software? Furthermore, (3) Is it possible to attain (1) and (2) under the assumption that all software on the remote device could be modified or compromised? In this paper we answer these questions by designing, proving security of, and formally verifying, VAPE: Verified Architecture for Proofs of 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, to authenticated sensing and trustworthy actuation, which are increasingly relevant in the context of safety-critical systems. VAPE architecture is publicly available and our evaluation demonstrates that it incurs low overhead, affordable even for lowest-end embedded devices, e.g., those based on MSP430 or ARV ATMega processors.

Figures

Figures reproduced from arXiv: 1908.02444 by the authors.

Figure 1
Figure 1. Overview of VAPE’s workflow VAPE implements a secure PoX = (XRequest, XAtomicExec, XProve, XVerify) scheme conforming to Definition 3. The steps in VAPE workflow are illustrated in [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. depicts VAPE’s architecture. In addition to VRASED hardware that provides secure RA by monitoring a set of CPU signals (see Section 3.2), VAPE monitors values stored in the dedicated physical memory region called METADATA. METADATA contains addresses/pointers to memory bound￾aries of ER (i.e., ERmin and ERmax) and memory boundaries of expected output: ORmin and ORmax. These addresses are sent by V rf as part of XReq… view at source ↗
Figure 3
Figure 3. Illustration of time intervals that each memory re [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: Hardware setup for a fire sensor VAPE is used to prove execution of the fire sensor software. This software is shown in Figure 8a in Appendix D. It consists of two main functions: ReadSensor and SoundAlarm. Proofs of execution are requested by the safety authority via …
Figure 6
Figure 6. Figure 6: Verified FSM for LTLs 4-6, a.k.a., EP2- Ephemeral [PITH_FULL_IMAGE:figures/full_fig_p016_6.png]
Figure 7
Figure 7. Figure 7: Verified FSM for LTL 10, a.k.a., MP3- Challenge [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: Code snippets for (a) fire sensor described in Section 7.3 (b) linker script [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

66 extracted references · 66 canonical work pages

  1. [1]

    C-flat: Control-flow attestation for embedded systems software

    Tigist Abera et al. C-flat: Control-flow attestation for embedded systems software. In CCS ’16, 2016

    work page 2016

  2. [2]

    V APE source code

    Anonymous Authors. V APE source code. https: //www.dropbox.com/sh/9id1ntfrnjy40tc/ AADONZgUdibXlONxSMdlm6npa, 2018

    work page 2018

  3. [3]

    The security impact of a new cryptographic library

    Daniel J Bernstein, Tanja Lange, and Peter Schwabe. The security impact of a new cryptographic library. In In- ternational Conference on Cryptology and Information Security in Latin America, 2012

    work page 2012

  4. [4]

    Implementing TLS with verified cryptographic security

    Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. Implementing TLS with verified cryptographic security. In SP, 2013

    work page 2013

  5. [5]

    Vale: Verifying high- performance cryptographic assembly code

    Barry Bond, Chris Hawblitzel, Manos Kapritsos, K Rus- tan M Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. Vale: Verifying high- performance cryptographic assembly code. In USENIX, 2017

    work page 2017

  6. [6]

    Remote attestation for low-end embedded de- vices: the prover’s perspective

    Ferdinand Brasser, Ahmad-Reza Sadeghi, and Gene Tsudik. Remote attestation for low-end embedded de- vices: the prover’s perspective. InDAC, 2016

    work page 2016

  7. [7]

    Brasser et al

    F. Brasser et al. Tytan: Tiny trust anchor for tiny devices. In DAC, 2015

    work page 2015

  8. [8]

    Temporal consistency of integrity-ensuring computations and applications to embedded systems security

    Xavier Carpent, Karim Eldefrawy, Norrathep Rat- tanavipanon, and Gene Tsudik. Temporal consistency of integrity-ensuring computations and applications to embedded systems security. In ASIACCS, 2018

    work page 2018

Show all 66 references
  1. [9]

    Temporal consistency of integrity-ensuring computations and applications to embedded systems security

    Xavier Carpent, Karim Eldefrawy, Norrathep Rat- tanavipanon, and Gene Tsudik. Temporal consistency of integrity-ensuring computations and applications to embedded systems security. In Proceedings of the 2018 on Asia Conference on Computer and Communications Security, pages 313...

    2018

  2. [10]

    ERASMUS: Efficient remote attestation via self-measurement for unattended settings

    Xavier Carpent, Norrathep Rattanavipanon, and Gene Tsudik. ERASMUS: Efficient remote attestation via self-measurement for unattended settings. In Design, Automation and Test in Europe (DATE), 2018

    2018

  3. [11]

    Remote attestation of iot devices via SMARM: Shuffled measurements against roving malware

    Xavier Carpent, Norrathep Rattanavipanon, and Gene Tsudik. Remote attestation of iot devices via SMARM: Shuffled measurements against roving malware. In IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 2018

    2018

  4. [12]

    Iot- fuzzer: Discovering memory corruptions in iot through app-based fuzzing

    Jiongyi Chen, Wenrui Diao, Qingchuan Zhao, Chaoshun Zuo, Zhiqiang Lin, XiaoFeng Wang, Wing Cheong Lau, Menghan Sun, Ronghai Yang, and Kehuan Zhang. Iot- fuzzer: Discovering memory corruptions in iot through app-based fuzzing. In NDSS, 2018

    2018

  5. [13]

    NuSMV 2: An opensource tool for symbolic model checking

    Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In In- ternational Conference on Computer Aided Verification, pages 359–36...

    2002

  6. [14]

    Nusmv 2: An opensource tool for symbolic model checking

    Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In In- ternational Conference on Computer Aided Verification, pages 359–36...

    2002

  7. [15]

    Sanc- tum: Minimal hardware extensions for strong software isolation

    Victor Costan, Ilia Lebedev, and Srinivas Devadas. Sanc- tum: Minimal hardware extensions for strong software isolation. In 25th{USENIX} Security Symposium ({USENIX} Security 16), 2016

    2016

  8. [16]

    A large-scale analysis of the security of embedded firmwares

    Andrei Costin, Jonas Zaddach, Aurélien Francillon, and Davide Balzarotti. A large-scale analysis of the security of embedded firmwares. In 23rd{USENIX} Security Sym- posium ({USENIX} Security 14), pages 95–110, 2014

    2014

  9. [17]

    Vrased: A verified hardware/software co-design for re- mote attestation

    Ivan De Oliveira Nunes, Karim Eldefrawy, Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. Vrased: A verified hardware/software co-design for re- mote attestation. USENIX Security’19 (To appear). Pre-print available at: https://arxiv.org/abs/ 1811.00175, 2019

    2019 arXiv

  10. [18]

    Litehax: lightweight hardware- assisted attestation of program execution

    Ghada Dessouky, Tigist Abera, Ahmad Ibrahim, and Ahmad-Reza Sadeghi. Litehax: lightweight hardware- assisted attestation of program execution. In 2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pages 1–8. IEEE, 2018

    2018

  11. [19]

    Lo-fat: Low-overhead control 14 flow attestation in hardware

    Ghada Dessouky, Shaza Zeitouni, Thomas Nyman, An- drew Paverd, Lucas Davi, Patrick Koeberl, N Asokan, and Ahmad-Reza Sadeghi. Lo-fat: Low-overhead control 14 flow attestation in hardware. In Proceedings of the 54th Annual Design Automation Conference 2017 , page 24. ACM, 2017

    2017

  12. [20]

    Spot 2.0—a framework for ltl and ω-automata manipulation

    Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Lau- rent Xu. Spot 2.0—a framework for ltl and ω-automata manipulation. In International Symposium on Automated Technology for Verification and Analysis, pages 122–129. Springer, 2016

    2016

  13. [21]

    HYDRA: hybrid design for remote attestation (using a formally verified microkernel)

    Karim Eldefrawy, Norrathep Rattanavipanon, and Gene Tsudik. HYDRA: hybrid design for remote attestation (using a formally verified microkernel). In Wisec. ACM, 2017

    2017

  14. [22]

    SMART: Secure and minimal architecture for (establishing dynamic) root of trust

    Karim Eldefrawy, Gene Tsudik, Aurélien Francillon, and Daniele Perito. SMART: Secure and minimal architecture for (establishing dynamic) root of trust. InNDSS. Internet Society, 2012

    2012

  15. [23]

    SMART: Secure and minimal architecture for (establishing a dynamic) root of trust

    Karim Eldefrawy et al. SMART: Secure and minimal architecture for (establishing a dynamic) root of trust. In NDSS, 2012

    2012

  16. [24]

    A minimalist approach to re- mote attestation

    Aurélien Francillon et al. A minimalist approach to re- mote attestation. In DATE, 2014

    2014

  17. [25]

    openMSP430, 2009

    Olivier Girard. openMSP430, 2009

    2009

  18. [26]

    Ironclad apps: End-to-end security via automated full- system verification

    Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad apps: End-to-end security via automated full- system verification. In OSDI, volume 14, pages 165–181, 2014

    2014

  19. [27]

    SeED: secure non-interactive attestation for embedded devices

    Ahmad Ibrahim, Ahmad-Reza Sadeghi, and Shaza Zeitouni. SeED: secure non-interactive attestation for embedded devices. In ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec), 2017

    2017

  20. [28]

    Intel Software Guard Extensions (Intel SGX)

    Intel. Intel Software Guard Extensions (Intel SGX)

  21. [29]

    Verilog2SMV: A tool for word-level verification

    Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, and Roberto Sebastiani. Verilog2SMV: A tool for word-level verification. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016, pages 1156–1159. IEEE, 2016

    2016

  22. [30]

    Establishing the genuinity of remote computer systems

    Rick Kennell et al. Establishing the genuinity of remote computer systems. In USENIX, 2003

    2003

  23. [31]

    seL4: Formal verification of an OS kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elka- duwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceed- ings of the ACM...

    2009

  24. [32]

    TrustLite: A security architec- ture for tiny embedded devices

    Patrick Koeberl, Steffen Schulz, Ahmad-Reza Sadeghi, and Vijay Varadharajan. TrustLite: A security architec- ture for tiny embedded devices. In EuroSys. ACM, 2014

    2014

  25. [33]

    Koeberl et al

    P. Koeberl et al. TrustLite: A security architecture for tiny embedded devices. In EuroSys, 2014

    2014

  26. [34]

    Kovah et al

    X. Kovah et al. New results for timing-based attestation. In IEEE S&P ’12, 2012

    2012

  27. [35]

    Formal verification of a realistic compiler

    Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009

    2009

  28. [36]

    McCune, and Adrian Perrig

    Yanlin Li, Jonathan M. McCune, and Adrian Perrig. Viper: Verifying the integrity of peripherals’ firmware. In CCS. ACM, 2011

    2011

  29. [37]

    Sancus 2.0: A low-cost security architecture for iot devices

    Job Noorman, Jo Van Bulck, Jan Tobias Mühlberg, Frank Piessens, Pieter Maene, Bart Preneel, Ingrid Ver- bauwhede, Johannes Götzfried, Tilo Müller, and Felix Freiling. Sancus 2.0: A low-cost security architecture for iot devices. ACM Trans. Priv. Secur., 20(3):7:1–7:33, July 2017

    2017

  30. [38]

    Towards systematic design of collective remote attestation protocols

    Ivan De Oliveira Nunes, Ghada Dessouky, Ahmad Ibrahim, Norrathep Rattanavipanon, Ahmad-Reza Sadeghi, and Gene Tsudik. Towards systematic design of collective remote attestation protocols. In ICDCS, 2019

    2019

  31. [39]

    Secure code update for embedded devices via proofs of secure erasure

    Daniele Perito and Gene Tsudik. Secure code update for embedded devices via proofs of secure erasure. In ESORICS, 2010

    2010

  32. [40]

    Petroni et al

    Jr. Petroni et al. Copilot — A coprocessor-based kernel runtime integrity monitor. In USENIX, 2004

    2004

  33. [41]

    Tamper resistance mechanisms for secure embedded systems

    Srivaths Ravi, Anand Raghunathan, and Srimat Chakrad- har. Tamper resistance mechanisms for secure embedded systems. In VLSI Design, 2004. Proceedings. 17th Inter- national Conference on, pages 605–611. IEEE, 2004

    2004

  34. [42]

    Scuba: Secure code update by attestation in sensor networks

    Arvind Seshadri, Mark Luk, Adrian Perrig, Leendert van Doorn, and Pradeep Khosla. Scuba: Secure code update by attestation in sensor networks. In ACM workshop on Wireless security, 2006

    2006

  35. [43]

    Seshadri et al

    A. Seshadri et al. SW ATT: Software-based attestation for embedded devices. In IEEE S&P ’04, 2004

    2004

  36. [44]

    Seshadri et al

    A. Seshadri et al. Pioneer: Verifying code integrity and enforcing untampered code execution on legacy systems. In ACM SOSP, 2005

    2005

  37. [45]

    Trusted platform module (tpm), 2017

    Trusted Computing Group. Trusted platform module (tpm), 2017. 15

    2017

  38. [46]

    Trusted Computing Group (TCG). Website. http://www.trustedcomputinggroup.org, 2015

    2015

  39. [47]

    Atrium: Runtime attestation resilient under memory attacks

    Shaza Zeitouni, Ghada Dessouky, Orlando Arias, Dean Sullivan, Ahmad Ibrahim, Yier Jin, and Ahmad-Reza Sadeghi. Atrium: Runtime attestation resilient under memory attacks. In Proceedings of the 36th International Conference on Computer-Aided Design, pages 384–391. IEEE Press, 2017

    2017

  40. [48]

    Hacl*: A verified modern cryptographic library

    Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. Hacl*: A verified modern cryptographic library. In Proceed- ings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1789–1806. ACM, 2017. APPENDIX A Sub-Mo...

    2017

  41. [49]

    EXEC is 0 whenever an FSM transitions to NotExec state

  42. [50]

    EXEC remains 0 until a transition leaving NotExec state is triggered

  43. [51]

    EXEC is 1 in all other states

  44. [52]

    Figure 6 represents a verified model enforcing LTLs 4-6, corresponding to the high-level property EP2- Ephemeral Atomicity

    Sub-modules composition: Since all PoX properties must simultaneously hold, the value of EXEC produced by VAPE is the conjunction (logical AND) of all sub- modules’ individualEXEC flags. Figure 6 represents a verified model enforcing LTLs 4-6, corresponding to the high-level pro...

  45. [53]

    The system reached state S0 in which the software stored in ER started executing from its first instruction ( PC = ERmin)

  46. [54]

    In the interval between S0 and S1 PC remained executing instructions within ER, there were no interrupts, no resets, and DMA remained inactive

    The system eventually reached a state S1 when ER fin- ished executing (PC = ERmax). In the interval between S0 and S1 PC remained executing instructions within ER, there were no interrupts, no resets, and DMA remained inactive

  47. [55]

    In the interval between S0 and S2 the memory regions of METADATA and ER were not modified

    The system eventually reached a state S2 when XProve started executing (PC = CRmin). In the interval between S0 and S2 the memory regions of METADATA and ER were not modified

  48. [56]

    The first two properties to be noted are LTL 12 and LTL 11

    In the interval between S0 and S2 the OR memory region was only modified by ER’s software execution (PC∈ ER∨¬ Modify_Mem(OR)). The first two properties to be noted are LTL 12 and LTL 11. LTL 12 establishes the default state of EXEC is 0. LTL 11 enforces that the only possible wa...

  49. [57]

    So far we have argued that to have a token H that reflects EXEC = 1 the code contained in ER must have executed suc- cessfully

    On the other hand, it is impossible to execute instructions of XProve (PC∈ CR) without leaving ER, because LTL 9 guarantees that ER and CR do not overlap, or EXEC = 0. So far we have argued that to have a token H that reflects EXEC = 1 the code contained in ER must have execute...

  50. [58]

    Setup: Adv is given oracle access to SW-Att calls

  51. [59]

    Challenge: A random challenge C hal← ${0,1}l is gener- ated and given to Adv

  52. [60]

    Response: Adv responds with a pair (M, σ), where σ is ei- ther forged by Adv, or is the result of calling SW-Att at some arbitrary time t

  53. [61]

    7.2 RA Security Definition: An RA scheme is considered secure if for all PPT adversaries Adv, there exists a negligible function negl such that: Pr[Adv, RA-game]≤ negl (l) Proof

    Adv wins if and only if M ⁄= AR(t) and σ = HMAC(KDF (K ,C hal),M). 7.2 RA Security Definition: An RA scheme is considered secure if for all PPT adversaries Adv, there exists a negligible function negl such that: Pr[Adv, RA-game]≤ negl (l) Proof. Assume that AdvPoX is an adversa...

  54. [62]

    Let X(t) denote the content in memory region X at time t

    METADATA⊂ AR; Doing so ensures that all sensitive memory regions used by VAPE are included among the inputs to VRASED’s attestation. Let X(t) denote the content in memory region X at time t. AdvRA can then be constructed using AdvPoX as follows:

  55. [63]

    AdvRA receives C hal from the challenger in step (2) of RA security game of Definition 7

  56. [64]

    It then calls AdvPoX in Case1.1

    At arbitrary timet, AdvRA has 3 options to writeAR(t) = ARAdv and call AdvPoX: (a) Modify ER(t)⁄= S or OR(t)⁄= O or METADATA (t)⁄= METADATA V rf. It then calls AdvPoX in Case1.1. (b) Modify ER to be different from the range chosen by V rf. Therefore, METADATA (t)⁄= METADATA V ...

  57. [65]

    By construc- tion M⁄= ARAdv = AR(t), as required by Definition 7

    AdvRA replies to the challenger with the pair (M,HAdv), where M corresponds to the values of S, O and METADATA V rf, matching HAdv and OAdv generated by AdvPoX. By construc- tion M⁄= ARAdv = AR(t), as required by Definition 7

  58. [66]

    exec.entry

    Challenger will accept (M,HAdv) with the same non-negligible probability that AdvPoX has of producing ( HAdv,OAdv) such that XVerify(HAdv,OAdv,S ,C hal,·) = 1. C Executable Limitations We now discuss the limitations of our approach on the exe- cutable types. Shared libraries. ...

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.