HYDRA: HYbrid Design for Remote Attestation (Using a Formally Verified Microkernel)
This addresses the need for secure remote attestation in embedded and cyber-physical systems, offering a novel hybrid approach that is incremental by combining verified software with existing hardware methods.
The paper tackles the problem of remote attestation (RA) by introducing HYDRA, the first hybrid RA design that uses a formally verified microkernel (seL4) to achieve memory isolation and protection, reducing hardware modifications. The result shows that HYDRA can attest 10MB of memory in less than 500msec using a Speck-based MAC.
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.