Protocols for a Two-Tiered Trusted Computing Base

A trusted computing base (TCB) is the minimum set of hardware and software components which are inherently trusted by a platform, and upon which more complex secure services can be built. The TCB is secure by definition, and it is typically implemented through hardened hardware components, which ensure that their secret data cannot be compromised. In this paper, we propose and investigate a two-tier TCB architecture that benefits both from a small hardened 'minimal' TCB, but also offers the possibility of integrating complex security services into an 'extended' TCB. Our design includes a collection of protocols to ensure (1) secure update of the components, (2) secure boot of the platform, (3) attestation, and (4) detection of powerful attackers that can corrupt memory regions together with a (highly probable) platform recovery mechanism after such an attack. The protocols have been formally modelled, and we provide a collection of security properties that have been verified using the automatic protocol verifier ProVerif.