A rest stop on the unending road to provable security

Abstract

During the past decade security research has offered persuasive arguments that the road to provable security is unending, and further that there’s no rest stop on this road; e.g., there is no security property one can prove without making assumptions about other, often unproven, system properties. In this paper I suggest what a useful first rest stop might look like, and illustrate one possible place for it on the road to provable security. Specifically, I argue that a small and simple verifier can establish software root of trust (RoT) on an untrusted system unconditionally; i.e., without secrets, trusted hardware modules, or bounds on the adversary power; and the verifier’s trustworthiness can be proven without dependencies of other unverified computations. The foundation for proving RoT establishment unconditionally already exists, and the proofs require only the availability of randomness in nature and correct specifications for the untrusted system. In this paper, I also illustrate why RoT establishment is useful for obtaining other basic properties unconditionally, such as secure initial state determination, verifiable boot, and on-demand firmware verification for I/O devices.