|
Published Articles >> Table of Contents >> Abstract
2003 IEEE Symposium on Security and Privacy
p. 166
Specifying and Verifying Hardware for Tamper-Resistant Software
David Lie, Stanford University
John Mitchell, Stanford University
Chandramohan A. Thekkath, Stanford University
Mark Horowitz, Stanford University
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SECPRI.2003.1199335
Send link to a friend
| Abstract |
|
We specify a hardware architecture that supports tamper-resistant software by identifying an "idealized" model, which gives the abstracted actions available to a single user program. This idealized model is compared to a concrete "actual" model that includes actions of an adversarial operating system. The architecture is verified by using a finite-state enumeration tool (a model checker) to compare executions of the idealized and actual models. In this approach, software tampering occurs if the system can enter a state where one model is inconsistent with the other. In performing the verification, we detected an replay attack scenario and were able to verify the security of our solution to the problem. Our methods were also able to verify that all actions in the architecture are required, as well as come up with a set of constraints on the operating system to guarantee liveness for users.
|
 Additional Information
|
Citation:
David Lie, John Mitchell, Chandramohan A. Thekkath, Mark Horowitz,
"Specifying and Verifying Hardware for Tamper-Resistant Software,"
sp,
p. 166,
2003 IEEE Symposium on Security and Privacy,
2003
|
|
