Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
Abstracts - 3rd USENIX Workshop on Electronic Commerce

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

Sean W. Smith and Vernon Austel
IBM T.J. Watson Research Center


Secure coprocessors provide a foundation for many exciting electronic commerce applications, as previous work [Yee94,YeTy95] has demonstrated. As our recent work [IBM97,SPW98,SmWe98] 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 surprisingly complex and subtle.

Formal methods provide one means to express, verify, and analyze such solutions (and would be required 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 statements 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 architecture can satisfy weaker security goals

We view this work as the beginning of developing formal models to address the trust challenges arising from using trusted hardware for electronic commerce.

  • View the full text of this paper in HTML form and PDF form.

  • If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.

  • To become a USENIX Member, please see our Membership Information.

?Need help? Use our Contacts page.

Last changed: 9 Apr 2002 ml
Technical Program
Workshop Index