The guarantees concern software-controlled attacks on a low-end MCU and hold only when the stated machine, compiler, cryptographic, and hardware boundaries are satisfied.

1. threat model

   Software adversary

   defined

   The adversary controls all untrusted software and writable data, can relocate malware, and can control DMA, but cannot modify protected ROM or directly bypass HW-Mod.

   Adversarial capabilities, axioms A1-A7, and exclusions · RA security game and SW-Att boundary
2. assumption

   Axioms A1-A7

   assumed

   The proof trusts accurate PC, memory, DMA, reset, and interrupt signals, plus compiler register cleanup and semantic preservation from verified C to assembly.

   Adversarial capabilities, axioms A1-A7, and exclusions · Soundness and security proof chain
3. limitation

   Excluded attacks and components

   explicitly excluded

   Physical attacks, induced hardware faults, physical side channels, and verification of the complete MCU implementation are outside the proved model.

   Adversarial capabilities, axioms A1-A7, and exclusions

The design composes a trusted software attestation routine with hardware state machines that watch execution and force reset on policy violations.

1. component

   SW-Att

   partially machine checked

   HACL* HMAC-SHA256 derives a challenge-specific key and authenticates the requested memory region; HACL* supplies inherited F* proofs, while mapping those guarantees into VRASED's model is manual.

   RA security game and SW-Att boundary
2. component

   HW-Mod

   model checked

   Hardware monitors observe program-counter, memory, interrupt, DMA, and reset signals; FSMs enforce LTL policies and reset the MCU when a policy is violated.

   LTL, NuSMV, Verilog2SMV, and composition workflow · LTL enforcement for access control, atomicity, confidentiality, DMA, and reset
3. definition

   Required properties P1-P7

   defined

   Key access control, no leakage, secure reset, functional correctness, immutability, atomicity, and controlled invocation are the bridge from components to remote-attestation guarantees.

   Secure-attestation properties P1-P7

The paper makes formal claims about a stated model, an empirical claim about concrete overhead, and a priority claim about first-of-kind verification.

1. claim

   End-to-end soundness

   machine checked within model

   SW-Att returns a temporally consistent HMAC of the attested memory as it existed when attestation began, conditional on the stated model and trusted boundaries.

   End-to-end soundness definition · Soundness and security proof chain
2. claim

   End-to-end security

   proved conditional

   A polynomial-time software adversary cannot forge a valid report for a different memory state except with negligible probability, assuming a secure HMAC and the machine/compiler axioms.

   RA security game and SW-Att boundary · Soundness and security proof chain
3. claim

   Practical overhead

   experimentally supported

   The standard FPGA design adds 6.3% logic cells and reports approximately 3.6 million cycles, or 450 ms at 8 MHz, to attest 4 KB.

   Verification results, overhead, and performance

The evidence combines inherited software proofs, model-checked hardware properties, compositional reasoning, public artifacts, and FPGA measurements.

1. evidence

   Formal verification path

   machine checked and proved

   NuSMV checks the hardware LTL properties and composition; Spot checks stated LTL implications; the final HMAC security reduction is a conditional paper proof rather than a wholly machine-checked proof.

   LTL, NuSMV, Verilog2SMV, and composition workflow · Soundness and security proof chain
2. evidence

   Prototype and measurements

   implemented and measured

   The authors synthesize an OpenMSP430-based implementation for a Basys3 Artix-7 FPGA and report model-checker resources, hardware cost, memory, and attestation time.

   OpenMSP430 and FPGA implementation · Verification results, overhead, and performance
3. artifact

   Public code and proof artifacts

   publicly available

   The public repository includes source, build instructions, Verilog modules, verification specifications, scripts, and soundness/security proof material; this map has not pinned a commit or independently reproduced it.

   Public implementation, build instructions, verification specifications, and proof artifacts

The strongest guarantees apply to the formalized module and model; moving from verified source and FSMs to a concrete MCU/FPGA system introduces trusted steps.

1. limitation

   Compiler and timing preservation

   assumed

   msp430-gcc is trusted to preserve functional semantics and register cleanup; preservation of HACL* timing properties by the compiler and MCU is also assumed.

   Adversarial capabilities, axioms A1-A7, and exclusions · Soundness and security proof chain
2. limitation

   MCU core and integration

   unverified integration

   The whole OpenMSP430 core and its concrete integration are not verified; implementers must establish that each target MCU satisfies the abstract signal and reset axioms.

   Adversarial capabilities, axioms A1-A7, and exclusions · Author response clarifying the verified module, integration assumptions, and prototype changes
3. limitation

   Physical and availability attacks

   out of scope

   Physical hardware attacks are excluded, and the base design does not authenticate verifier requests; the paper discusses an optional authenticated variant to reduce request-flooding risk.

   Adversarial capabilities, axioms A1-A7, and exclusions · Soundness and security proof chain

Later researchers examined the gap between VRASED's formal model and its concrete openMSP430 instantiation, and the VRASED repository records a scoped response and prototype changes.

1. counterevidence

   Mind the Gap analysis

   independently reported

   The 2022 study reports attacks against concrete implementations and argues that formal guarantees do not automatically transfer across unmodeled assumptions and integration steps.

   Independent description of VRASED's formal model, trusted boundaries, and research lineage · Independent adversarial analysis of gaps between formal models and concrete implementations
2. response

   VRASED repository response

   author response

   The maintainers state that reported issues do not falsify properties of the verified RA module; they distinguish integration violations, out-of-model hardware changes, and an unverified fork, and report changes to the sample instantiation.

   Author response clarifying the verified module, integration assumptions, and prototype changes