The seL4 refinement proof and access-control work establish functional correctness, authority confinement, integrity, and confidentiality for the microkernel and a correctly specified capability configuration.

1. assumption

   Initialization and hardware assumptions

   outside proof

   The inherited proof assumes the kernel is loaded correctly into a consistent state and the processor behaves correctly. HYDRA uses hardware secure boot for the first premise; no commercially available formally verified processor closes the second premise.

   Five implementation challenges and lessons

ROM verifies seL4, seL4 authenticates and starts the protected process, and that process rejects stale or unauthenticated requests before MACing a named memory interval of a target process and returning the checksum.

1. protocol

   Persisted pseudo-timestamp

   workaround

   Lacking a seL4 real-time-clock driver, the prototype loads a timestamp saved before reboot, validates the first new request's larger timestamp, starts a counter, and periodically persists their combination for later restarts.

   Five implementation challenges and lessons

The paper records decisions and unresolved platform dependencies that are easy to hide when a verified component is described as if it verified an entire system.

1. contribution

   Choose hybrid MAC attestation deliberately

   experience based

   Software-only timing attestation depends on disputed optimal-checksum assumptions and complete hardware attestation is not easily emulated; a challenge-response MAC fits the hybrid model, with Speck and BLAKE2S performing best among the tested software implementations.

   Five implementation challenges and lessons · Sabre Lite runtime breakdown, MAC comparison, and scaling
2. contribution

   Verified isolation does not eliminate all hardware

   experience based

   seL4 emulates most access-control properties previously supplied by processor logic, while immutable storage and authenticated boot are still required to ensure the intended kernel and attestation code start first.

   Mapping RA properties to access-control configuration C1-C3 · Five implementation challenges and lessons
3. contribution

   Board capabilities constrain assurance

   experience based

   A usable prototype needs configurable secure-boot ROM and drivers for security-critical devices. Sabre Lite's High Assurance Boot can authenticate a signed image, but the absent clock driver forced a weaker timestamp workaround.

   Five implementation challenges and lessons

The source reports an implemented hybrid design, conditional enforcement of the adopted RA properties, and platform-scale feasibility; its compressed format refers readers to the full HYDRA paper for a broader threat and security analysis.

1. claim

   Capability realization of RA properties

   configuration argument

   Exclusive executable/key, TCB, and VSpace capabilities plus highest scheduling priority are argued to realize key secrecy, no leaks, immutability at runtime, uninterruptibility, and controlled invocation, conditional on correct secure boot and code.

   Mapping RA properties to access-control configuration C1-C3
2. claim

   Sabre Lite feasibility

   measured

   The paper reports under 500 milliseconds for a 10 MB region with Speck, at least a one-third speed advantage for Speck and BLAKE2S over other tested MACs, and approximately linear runtime in memory size and process count.

   Sabre Lite runtime breakdown, MAC comparison, and scaling

Evidence consists of inherited seL4 proof results, an explicit property-to-capability mapping, the boot and protocol design, a commodity Sabre Lite implementation, and microbenchmarks decomposed into request verification, memory mapping, and MAC work.

1. evidence

   Runtime composition

   reported experiment

   MacMem consumes about 84 percent of time for a 1 MB region and about 90 percent for 10 KB in this version; request verification and memory mapping together remain below 20 percent.

   Sabre Lite runtime breakdown, MAC comparison, and scaling

seL4's proof covers the kernel, not the processor, boot ROM, board initialization, attestation code, cryptographic implementation, timestamp persistence, drivers, or the full composition. The paper also does not reproduce a complete adversarial model or end-to-end proof in four pages.

1. limitation

   Short companion, not the full HYDRA paper

   companion version

   This DSN-W article reports under 500 milliseconds and emphasizes lessons; the longer WiSec/arXiv version maps more assumptions, two platforms, and an expanded evaluation, including a later sub-250-millisecond Sabre Lite result. The records should not be conflated.

   Sabre Lite runtime breakdown, MAC comparison, and scaling · Full HYDRA design and evaluation