Sciweavers

Share
SP
2003
IEEE

Specifying and Verifying Hardware for Tamper-Resistant Software

10 years 5 months ago
Specifying and Verifying Hardware for Tamper-Resistant Software
We specify a hardware architecture that supports tamper-resistant software by identifying an “idealized” hich 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.
David Lie, John C. Mitchell, Chandramohan A. Thekk
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where SP
Authors David Lie, John C. Mitchell, Chandramohan A. Thekkath, Mark Horowitz
Comments (0)
books