Trusting Trusted Hardware: Towards a Formal Model for Programmable Secure Coprocessors

Abstract

Secure coprocessors provide a foundation for many exciting electronic commerce applications, as previ-ous work [20, 21] has demonstrated. As our recent work [6, 13, 14] has explored, building a high-end secure coprocessor that can be easily programmed and deployed by a wide range of third parties can be an important step toward realizing this promise. But this step requires trusting trusted hardware| and achieving this trust can be difficult in the face of a problem and solution space that can be surpris-ingly complex and subtle. Formal methods provide one means to express, ver-ify, and analyze such solutions (and would be re-quired for such a solution to be certified at FIPS 140-1 Level 4). This paper discusses our current efforts to apply these principles to the architecture of our secure coprocessor. We present formal state-ments of the security goals our architecture needs to provide; we argue for correctness by enumerating the architectural properties from which these goals can be proven; we argue for conciseness by showing how eliminating properties causes the goals to fail; but we discuss how simpler versions of the architec-ture can satisfy weaker security goals. We view this work as the beginning of developing formal models to address the trust challenges aris-ing from using trusted hardware for electronic commerce.