VERIAL: Verification-Enabled Runtime Integrity Attestation of Linux

Runtime attestation is a way to gain confidence in the current state of a remote target.

Layered attestation is a way of extending that confidence from one component to another.

Introspective solutions for layered attestation require strict isolation.

The seL4 is uniquely well-suited to offer kernel properties sufficient to achieve such isolation.

I design, implement, and evaluate introspective measurements and the layered runtime attestation of a Linux kernel hosted by the seL4.

VERIAL can detect diamorphine-style rootkits with performance cost comparable to previous work.