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

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.