Specifying and verifying hardware for tamper-resistant software
Specifying and verifying hardware for tamper-resistant software
复制标题
指定和验证防篡改软件的硬件
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
M. Horowitz
中科院分区：
文献类型：
--
作者：
D. Lie;John C. Mitchell;C. Thekkath;M. Horowitz
我们通过识别“理想化”模型来指定支持耐篡改软件的硬件体系结构，该模型为单个用户程序提供了抽象的操作。将此理想化的模型与包括对抗操作系统的动作的具体“实际”模型进行了比较。通过使用有限状态枚举工具（模型检查器）来比较理想化和实际模型的执行来验证该体系结构。在这种方法中，如果系统可以输入一个模型与另一个模型进行验证不一致的状态，则会发生软件篡改，我们检测到了重播攻击方案并能够验证解决问题的解决方案的安全性。我们的方法还能够验证架构中的所有操作是否需要，并在操作系统上提出一系列约束，以确保用户的能力。
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 a 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.