Specifying and Verifying Hardware for Tamper-Resistant Software
- David Lie ,
- John Mitchell ,
- Chandu Thekkath ,
- Mark Horowitz
Proceedings of the 2003 IEEE Symposium on Security and Privacy |
Published by Institute of Electrical and Electronics Engineers, Inc.
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.
© 2003 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.