FinalFilter: Asserting Security Properties of a Processor at Runtime
FinalFilter: Asserting Security Properties of a Processor at Runtime
复制标题
FinalFilter：在运行时断言处理器的安全属性
作者：
C. Sturton;Matthew Hicks;Samuel T. King;Jonathan M. Smith
在一个理想的世界里，构建一个可证明正确和安全的处理器是可能的。然而，当今处理器的复杂性使这一理想遥不可及。现代处理器的完整验证仍然是棘手的。静态验证甚至一个简单的安全属性-例如，“硬件特权升级永远不会发生”-仍然超出了形式验证的最新技术水平。测试可以补充正式的验证方法，但测试是不完整的，硬件中的漏洞，使其容易受到继续逃避测试套件。此外，狡猾的恶意行为者可以逃避典型的测试覆盖度量。最近的努力，包括三位作者的努力，已经探索了在设计文件上使用静态分析（例如，硬件描述级源代码或门级网表）来发现可疑电路。这些技术依赖于分析来定义指示可能的特洛伊木马的模式，然后在设计中搜索匹配该模式的实例。然而，与模式不匹配的恶意电路将被遗漏，打开漏洞的无意错误也会被遗漏。当弱点被发现时，硬件已经在最终用户手中，容易受到攻击。在没有完整的正确性证明的情况下，需要的是最终的过滤器：一种运行时验证技术，在部署后工作，以检测和响应在执行期间发生的安全属性违规。在本文中，我们使用我们的工具FinalFilter作为案例研究来说明最终过滤器的情况。
& IN AN IDEAL world, it would be possible to build a provably correct and secure processor. However, the complexity of today’s processors puts this ideal out of reach. The complete verification of a modern processor remains intractable. Statically verifying even a simple security property—for example, “hardware privilege escalation never occurs”—remains beyond the state of the art in formal verification. Testing can complement formal verification methods, yet testing is incomplete and bugs in the hardware that leave it vulnerable continue to elude test suites. Further, a crafty malicious actor can evade typical testing coverage metrics. Recent efforts, including that of three of the authors, have explored the use of static analysis on the design files (e.g., hardware description level source code or gate-level netlists) to find suspicious circuitry. These techniques rely on heuristics to define patterns that indicate a likely trojan and then search for instances in the design that match the pattern. However, malicious circuitry that does not match the pattern will be missed, as will inadvertent bugs that open vulnerabilities. By the time the weakness is uncovered, the hardware is already in the end user’s hands and vulnerable to attack. In the absence of a full proof of correctness, what is needed is a final filter: a runtime verification technique that works—postdeployment—to detect and respond to security property violations as they occur during execution. In this article, we make the case for final filters using our tool, FinalFilter, as a case study.
识别处理器动态验证的安全关键属性
DOI：
10.1145/3037697.3037734
发表时间：
2017
期刊：
Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems
影响因子：
--
作者：
Zhang, Rui;Stanley, Natalie;Griggs, Christopher;Chi, Andrew;Sturton, Cynthia
通讯作者：
Sturton, Cynthia