A prover should produce an unforgeable token that convinces a verifier of its measured state; malware must not make a compromised state appear expected, and request handling should resist malicious triggering and replay.

1. requirement group

   Minimal RA properties

   enumerated

   The adopted requirements are exclusive access to attestation key K, no leakage of key-derived intermediates, immutable attestation code, uninterruptible execution, controlled entry and exit, and authenticated fresh verifier requests.

   Remote-attestation objective and minimal security properties

Remote or local attackers may control all ordinary application software and communication before and after attestation. They cannot physically tamper, induce hardware faults, extract K through side channels, or interrupt seL4 or the protected attestation process.

1. assumption

   Provisioning and boot trust

   assumed

   The prover and verifier share a pre-provisioned secret K. ROM authenticates the boot image, seL4 verifies the initial attestation process, and the initial capability distribution exactly implements the paper's configuration.

   ROM, seL4, attestation algorithm, clock, and secure-boot requirements · Key storage and prototype timestamp mechanism
2. assumption

   seL4 proof assumptions

   outside verified kernel

   The inherited functional-correctness claim assumes correct ARM assembly, conforming untampered hardware, correct cache and TLB management, correct boot code, disabled or trusted DMA, and absence of timing side channels.

   Assumptions outside the seL4 functional-correctness proof

PR-Att receives exclusive access to the attestation binary and K, its thread-control block, and its virtual address space, plus exclusive write authority over the clock; all later processes receive lower priority and only minimal capabilities.

1. method

   Atomic high-priority execution

   enforced if code conforms

   Making PR-Att the initial, highest-priority user process and preventing later processes from raising priority is used to establish uninterruptibility; protecting its TCB and address space supplies controlled invocation and no-leak isolation.

   Derivation of HYDRA access-control configuration C1-C4 · Informal mapping from nine implementation features to RA requirements

A request names a timestamp, target process, memory interval, and MAC. PR-Att rejects stale or unauthenticated requests, maps the target range into its own address space, MACs request context and bytes under K, and returns the report.

1. protocol

   Boot and setup sequence

   implemented

   A ROM loader verifies the signed seL4 image, seL4 authenticates PR-Att, and PR-Att creates the remaining user processes with non-overlapping virtual spaces and no capability-grant endpoint that could leak its authority.

   ROM, seL4, attestation algorithm, clock, and secure-boot requirements · seL4 v1.3 implementation, process configuration, and code size
2. protocol

   Request freshness and DoS mitigation

   prototype approximation

   The design calls for a protected real-time clock. Because seL4 lacked a driver, the prototype combines a persisted prior timestamp, the first validated request, and a protected timer counter; a secure counter is an alternative with weaker delayed-message detection.

   Key storage and prototype timestamp mechanism

The paper claims conditional RA security and practical performance. Kernel isolation is machine-checked upstream; the mapping from HYDRA code and configuration to the required RA properties is an informal paper argument.

1. claim

   Satisfaction of minimal RA properties

   informally derived from verified component

   Nine boot, priority, memory, TCB, capability, and clock features are mapped to exclusive K access, no leaks, immutability, uninterruptibility, controlled invocation, and verifier authentication.

   Informal mapping from nine implementation features to RA requirements
2. claim

   Reduced bespoke hardware requirement

   design comparison

   Unlike earlier hybrid designs that modify microcontroller access controls, HYDRA pushes isolation and scheduling into seL4; it still needs hardware-enforced secure boot, immutable trust material, and a reliable clock or counter.

   Derivation of HYDRA access-control configuration C1-C4 · ROM, seL4, attestation algorithm, clock, and secure-boot requirements
3. claim

   Commodity-platform feasibility

   measured

   The Sabre Lite prototype reports under 250 milliseconds to attest 10 MB with a Speck-based MAC, while ODROID-XU4 reports under 100 milliseconds with keyed BLAKE2S; memory and process-count costs scale approximately linearly in the tested ranges.

   Sabre Lite runtime breakdown, scaling, and MAC comparisons · ODROID-XU4 platform results

Support combines upstream Isabelle/HOL proofs for seL4, manual configuration and code obligations for HYDRA, two C implementations on commodity boards, and runtime measurements decomposed into request verification, memory mapping, and MAC computation.

1. evidence

   Prototype scale

   implemented

   On seL4 1.3, the complete build with helper libraries and network stack is reported as 105,360 C lines and 574 KB, while HYDRA-specific code excluding helpers is about 2,800 lines and the base seL4 kernel is 215 KB.

   seL4 v1.3 implementation, process configuration, and code size
2. evidence

   Runtime breakdown and scaling

   reported experiment

   On Sabre Lite, MAC computation accounts for roughly 89 percent of the 1 MB time and 92 percent of the 20 KB time; memory mapping remains below one fifth of MAC time in the tested sizes, and process-count scaling is approximately linear.

   Sabre Lite runtime breakdown, scaling, and MAC comparisons

HYDRA inherits verified isolation only where the actual boot chain, hardware, capability configuration, and code satisfy seL4 assumptions. PR-Att, cryptography, timestamp persistence, network stack, device drivers, and the end-to-end RA theorem are not machine-checked by this work.

1. limitation

   Physical, DMA, and side-channel boundary

   explicitly out of scope

   Physical attackers, hardware faults, key extraction, timing leakage, and untrusted DMA are excluded. The paper notes that helper networking code is acceptable to the objective only if an I/O MMU prevents DMA attacks.

   Remote, local, and excluded physical adversaries · Assumptions outside the seL4 functional-correctness proof
2. limitation

   No same-platform baseline

   experimental limitation

   SMART and TrustLite could not run on the same off-the-shelf boards because of their hardware and microcontroller requirements, so the evaluation establishes HYDRA feasibility but not a controlled performance comparison against those systems.

   Sabre Lite runtime breakdown, scaling, and MAC comparisons