求解器辅助的恒定时间电路验证
Solver-Aided Constant-Time Circuit Verification
摘要：
我们提出了氙，求解器辅助的方法，正式验证Verilog硬件在恒定时间执行。Xenon通过一种新的恒定时间反例概念，大大减少了定位验证失败根本原因所需的工作量，从而扩展到实际的硬件设计，Xenon使用该反例自动合成一组最小的保密假设。Xenon通过模块摘要的概念进一步利用Verilog代码中的模块性，从而避免多个模块实例化之间的重复工作。我们展示了氙的假设合成和总结如何使各种电路的验证，包括AES，高度模块化的AES-256实现，其中模块化将验证从6小时减少到3秒以下，以及ScarV，一种时序通道硬化的RISC-V微控制器，其大小超过以前验证的设计一个数量级。
英文摘要：
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exploits modularity in Verilog code via a notion of module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable the verification of a variety of circuits including AES, a highly modular AES-256 implementation where modularity cuts verification from six hours to under three seconds, and ScarV, a timing channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
