From CySeP, we have Gligor's verifier that yields unconditional security for root-of-trust:
Speaker: Prof. Virgil D. Gligor (Carnegie Mellon University, PA, USA)
Title: A Rest Stop on the (Never Ending) Road to Provable Security
Abstract: During the past decade security research has offered persuasive arguments that the road to provable security is never ending, 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 seminar I describe what a useful first rest stop might look like, and illustrate one possible place for it on the road to provable security. Specifically, I show that a 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. I will illustrate the theory foundation for proving RoT establishment unconditionally, and show that the proofs require only the availability of randomness in nature and correct specifications for the untrusted system. The verifier is trustworthy as it requires only the off-line ability to construct nonces from strings of truly random bits and evaluate a new computation primitive – the randomized polynomials -- and then perform an on-line measurement of the untrusted system's evaluation of randomized polynomials and its response time. The optimal code for randomized polynomials on the instruction sets of real processors is discussed is some detail. I also illustrate why RoT establishment is useful for obtaining other basic properties unconditionally, such as secure initial state determination and verifiable boot -- a stronger notion than secure and trusted boot. Verifiable boot can be viewed as an instance of the FlipIt game between a defender and an adversary, where the defender wins the game by discovering the presence of malware surreptitiously inserted by the adversary into the system, unconditionally.
From CySeP, we have Gligor's verifier that yields unconditional security for root-of-trust: