EXERTv2: Exhaustive Integrity Analysis for Information Flow Security with FSM Integration
EXERTv2: Exhaustive Integrity Analysis for Information Flow Security with FSM Integration
复制标题
DOI：
10.1007/s41635-023-00141-3
复制
发表时间：
2023-12
期刊：
影响因子：
--
通讯作者：
Jiaming Wu;Domenic Forte
中科院分区：
文献类型：
--
作者：
Jiaming Wu;Domenic Forte
硬件信息流分析可检测微架构设计缺陷、测试/调试设计 (DfT/D) 后门和硬件木马所导致的安全漏洞。尽管信息流违规可以通过多种可能的方式表现出来，但先前的研究仅集中于检测此类漏洞的存在，并且没有提出彻底激活所有漏洞点并减少误报的方法。在本文中，我们提出了 EXERTv2，这是一种新颖的分析框架，它结合了 ATPG、SAT 和 FSM 分析以及 FSM 集成，以检测信息流违规并执行详尽的分析，报告易受攻击的控制点的完整的完整性违规输入模式集。与原始版本的 EXERT 相比，EXERTv2 的显着贡献在于其集成 FSM 的算法，简化了约束多个 FSM 的过程。 FSM 分析和集成尤其将设计中所有 FSM 的行为视为一个整体，这可以离线执行，有助于解决现有方法中的可扩展性限制，同时保持详尽。我们还演示了 EXERT 在故障注入漏洞分析和攻击应用中的用法。作为概念验证，EXERTv2 在 Trust-Hub 的多个特洛伊木马基准测试和另外两个密码上进行了评估。它可以检测罕见的特洛伊木马触发器（激活概率为 1.4243e70），在几分钟内生成所有激活模式，并且与 Cadence Jasper 安全路径验证 (SPV) 相比，运行时间快 15 到 110 倍。 EXERT 还应用于更大的 RISC-V 基准测试，以识别有或没有导致特权升级的错误注入的指令序列。
Hardware information flow analysis detects security vulnerabilities resulting from microarchitectural design flaws, design-for-test/debug (DfT/D) backdoors, and hardware Trojans. Though information flow violations can be manifested through a multitude of possible ways, prior research has only focused on detecting the existence of such vulnerabilities and no approach has been proposed to exhaustively activate all vulnerable points and reduce false positives. In this paper, we propose EXERTv2, a novel analysis framework that combines ATPG, SAT, and FSM analysis as well as FSM integration to detect information flow violations and perform exhaustive analysis that reports the complete set of integrity-violating input patterns for vulnerable control points. Compared with the original version of EXERT, the significant contribution of EXERTv2 is its algorithm for integrating FSMs, which simplifies the process of constraining multiple FSMs. The FSM analysis and integration, in particular, consider the behavior of all the FSMs in the design as a whole, which can be performed offline and helps resolve scalability limitations in prior approaches while remaining exhaustive. We also demonstrate EXERT’s usage in the application of fault injection vulnerability analysis and attacks. As a proof-of-concept, EXERTv2 is evaluated on multiple Trojan benchmarks from Trust-Hub and two additional ciphers. It detects rare Trojan triggers (activation probability1.4243e70), generates all activation patterns within minutes, and shows a 15to 110faster runtime compared with Cadence Jasper Security Path Verification (SPV). EXERT is also applied to a larger RISC-V benchmark to identify instruction sequences with and without fault injection that result in privilege escalation.