Summary: * TPM at the root of trust. * CPU state cleared to known-good using SKINIT to reset a core. * "Formally verified" kernel/stack. * Dafny, a safe lan

Summary: * TPM at the root of trust. * CPU state cleared to known-good using SKINIT to reset a core. * "Formally verified" kernel/stack. * Dafny, a safe language to write it in. * Verifiable machine code, like Google's NaCl (verifiable x86 subset in fact) That's great, but there's still a bunch of issues this doesn't solve, and it's a stretch to call this "end-to-end" or "full-system". No, the issues aren't goals of the paper, but that's my concern - this is asserting software stack guarantees which the human-side and hardware-side can't provide: * Compulsion. This relies on a remote chain of trust, which can easily be subverted without your knowledge if the platform owner and another actor collude (or are compelled) to generate a chained cert which allows access to your system. * Every CPU I've seen which declares an instruction or register is a big "reset switch" for a core doesn't actually do that. Usually a ton of state is left the same as before reset. This leaks information across reset, and can be used to subvert the post-reset core if it isn't careful to manually erase anything it relies on. For example, cache data, TLB entries and even most general purpose registers tend not to be reset. * Subverting the memory subsystem results in the CPU executing arbitrary code which wasn't what you provided, undetectably, out of reset. * It is not possible to formally verify an entire platform. This is somewhat unfair of me, but it feels like this is securing the software stack far beyond the capability of the hardware to provide those guarantees. * Every CPU has bugs which result in information leakage or privilege escalation. It helps that this is only running a verifiable x86 subset, but I've seen plenty of bugs resulting from rare instruction pairing/ordering. Usually they just deadlock a core, but sometimes result in escalation. So it's great work, but it's an advance way beyond what the rest of the system (human and hardware) can guarantee.