About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
USENIX EC 1998
Conference paper
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.