Security verification of hardware-enabled attestation protocols

Hardware-software security architectures can significantly improve the security provided to computer users. However, we are lacking a security verification methodology that can provide design-time verification of the security properties provided by such architectures. While verification of an entire hardware-software security architecture is very difficult today, this paper proposes a methodology for verifying essential aspects of the architecture. We use attestation protocols proposed by different hardware security architectures as examples of such essential aspects. Attestation is an important and interesting new requirement for having trust in a remote computer, e.g., in a cloud computing scenario. We use a finite-state model checker to model the system and the attackers, and check the security of the protocols against attacks. We provide new actionable heuristics for designing invariants that are validated by the model checker and thus used to detect potential attacks. The verification ensures that the invariants hold and the protocol is secure. Otherwise, the protocol design is updated on a failure and the verification is re-run.