硬件在设计制造之前通常通过寄存器传输级（RTL）仿真进行验证。为了测试与安全相关的信息流属性（如机密性和完整性），可以在设计中自动添加污点逻辑来跟踪信息如何流动。然而，最先进的污点逻辑仪器（如CellIFT）使基于仿真的测试开销过高：在Mega-BOOM（13.6万个单元）上，它使仪器化设计达到原始单元数的5.81倍，并导致143.72倍的仿真速度下降。简化污点逻辑可提高仿真速度，但不可避免地会牺牲精度。这种轻量级、不精确的污点逻辑会引入误报，最终可能导致更高的开销来检查这些误报。本文探讨了“精度实际上在哪里是必要的”这一研究问题，以克服误报带来的开销。它提出了CEGAR-T框架，该框架自动合成污点逻辑，在保证无假阳性（相对于精确的CellIFT基线）的同时最小化污点逻辑仪器开销。作者实现了CEGAR-T，并在开源RISC-V核心的时序侧信道安全指令集问题上进行了评估。在所有评估的核心上，CEGAR-T将仪器开销和仿真开销分别从几何平均5.64倍降至1.42倍、从34.65倍降至1.79倍，同时不损失CellIFT基线的精度效益。这项研究为预硅硬件安全验证提供了高效的自动化方案，显著降低了使用精确信息流跟踪的门槛。

本研究针对 Intel 神经网络计算棒 2 (NCS2) 中的 Myriad X VPU，开展了系统性的单脉冲电磁故障注入 (EMFI) 实验。作者在 OpenVINO 运行时上运行了三个 ImageNet 训练的卷积神经网络（ResNet-18、ResNet-50、VGG-11），通过 1536 次热点定位测试和约 16000 次参数搜索测试，观察到单脉冲引发的四种可重复故障输出类别：无精度变化、微小静默数据损坏 (SDC)、重大持久性退化（在后续推理中持续存在直至模型重新加载），以及设备挂起需 USB 断电重启。其中，重大退化类在特征热点处以 18%–31% 的概率发生，导致 Top-1 精度降至 5% 以下，且该状态在所有后续推理中保持，直到显式重新加载模型——这种机制无法被任何推理 API 级别的检测手段捕获。更关键的是，即使在模型已加载但设备空闲时注入脉冲，也能触发该退化状态，表明仅靠加载时的完整性检查不足以防范。论文讨论了按严重程度分级的缓解策略，重点是可应用层实现且无需修改设备固件或 OpenVINO 运行时的措施。该工作填补了公开文献中对商用神经推理加速器在瞬态硬件干扰下故障响应的系统性表征空白，对部署在安全关键边缘场景的 AI 系统具有重要参考价值。

该论文是系列正式验证分析掩码NTT（数论变换）硬件安全性论文的第7篇，针对后量子密码（PQC）硬件中的侧信道泄漏问题。论文证明了在任意深度k级流水线中，采用新鲜中间掩码和每级PF-PINI(≤2)小工具（gadgets）的掩码NTT实现，每个观察值的原像基数上界为2·q^{2k-2}（通过Lean 4机器检验，无漏洞）。在标准语义解释（除以总掩码元组空间大小q^{2k-1}）下，每个观察值的条件概率上界为2/q，与流水线深度k无关。主要贡献包括：1) k级组合定理，推广了之前2级结果，证明只有最后一级的PF-PINI参数影响界限；2) 证明Montgomery归约满足PF-PINI(2)且最大重数严格为2；3) 将各组件整合为端到端界限；4) 通过Lean验证的假设违反条件锚定先前的经验性和结构性Adams Bridge分析。该工作为掩码PQC硬件提供了可扩展的理论安全界，并经过正式验证。