Security verification of hardware-enabled attestation protocols

Tianwei Zhang, Jakub Szefer, Ruby B. Lee

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012
Pages47-54
Number of pages8
DOIs
StatePublished - Dec 1 2012
Event2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012 - Vancouver, BC, Canada
Duration: Dec 1 2012Dec 5 2012

Publication series

NameProceedings - 2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012

Other

Other2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012
CountryCanada
CityVancouver, BC
Period12/1/1212/5/12

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Security verification of hardware-enabled attestation protocols'. Together they form a unique fingerprint.

  • Cite this

    Zhang, T., Szefer, J., & Lee, R. B. (2012). Security verification of hardware-enabled attestation protocols. In Proceedings - 2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012 (pp. 47-54). [6472491] (Proceedings - 2012 IEEE/ACM 45th International Symposium on Microarchitecture Workshops, MICROW 2012). https://doi.org/10.1109/MICROW.2012.16