|
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
Abstract
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.
Technical Program