Skip to main content
USENIX
  • Conferences
  • Students
Sign in

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home ยป Trusting Trusted Hardware: Towards a Formal Model for Programmable Secure Coprocessors
Tweet

connect with us

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

Authors: 

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.

Sean W. Smith, IBM T.J. Watson Research Center

Vernon Austel, IBM T.J. Watson Research Center

BibTeX
@inproceedings {261132,
author = {Sean W. Smith and Vernon Austel},
title = {Trusting Trusted Hardware: Towards a Formal Model for Programmable Secure Coprocessors},
booktitle = {3rd USENIX Workshop on Electronic Commerce (EC 98)},
year = {1998},
address = {Boston, MA},
url = {https://www.usenix.org/conference/3rd-usenix-workshop-electronic-commerce/trusting-trusted-hardware-towards-formal-model},
publisher = {USENIX Association},
month = aug,
}
Download

Links

Paper: 
http://usenix.org/publications/library/proceedings/ec98/full_papers/smith/smith.pdf
Paper (HTML): 
http://usenix.org/publications/library/proceedings/ec98/full_papers/smith/smith_html/smith.html
  • Log in or    Register to post comments

© USENIX

  • Privacy Policy
  • Contact Us