Title: HYDRA: HYbrid Design for Remote Attestation (Using a Formally Verified Microkernel),
Abstract: Remote Attestation (RA) allows a trusted entity (verifier) to securely
measure internal state of a remote untrusted hardware platform (prover). RA can
be used to establish a static or dynamic root of trust in embedded and
cyber-physical systems. It can also be used as a building block for other
security services and primitives, such as software updates and patches,
verifiable deletion and memory resetting. There are three major classes of RA
designs: hardware-based, software-based, and hybrid, each with its own set of
benefits and drawbacks. This paper presents the first hybrid RA design, called
HYDRA, that builds upon formally verified software components that ensure
memory isolation and protection, as well as enforce access control to memory
and other resources. HYDRA obtains these properties by using the formally
verified seL4 microkernel. (Until now, this was only attainable with purely
hardware-based designs.) Using seL4 requires fewer hardware modifications to
the underlying microprocessor. Building upon a formally verified software
component increases confidence in security of the overall design of HYDRA and
its implementation. We instantiate HYDRA on two commodity hardware platforms
and assess the performance and overhead of performing RA on such platforms via
experimentation; we show that HYDRA can attest 10MB of memory in less than
500msec when using a Speck-based message authentication code (MAC) to compute a
cryptographic checksum over the memory to be attested.