Solver-Aided Constant-Time Hardware Verification
Solver-Aided Constant-Time Hardware Verification
复制标题
DOI：
10.1145/3460120.3484810
复制
发表时间：
2021-11
期刊：
影响因子：
--
通讯作者：
K. V. Gleissenthall;Rami Gökhan Kici;D. Stefan;Ranjit Jhala
中科院分区：
文献类型：
--
作者：
K. V. Gleissenthall;Rami Gökhan Kici;D. Stefan;Ranjit Jhala
我们提出了Xenon，这是一种求解器的交互式方法，用于正式验证Verilog硬件在恒定时间内执行。 Xenon通过大大减少通过新的恒定时间反例的概念来定位验证故障的根本原因所需的努力，从而将其缩放到现实的硬件设计，Xenon使用该概念合成了交互式验证循环中最小的保密假设。为了减少验证时间，氙气通过模块摘要利用Verilog代码中的模块化，从而避免了跨多个模块实例化的重复工作。我们展示了氙的假设合成和摘要如何使我们能够验证不同种类的电路，包括高度模块化的AES-256实施，其中模块化将验证从六个小时降低到三秒钟，而Scarvside-Channel强化了RISC-V Micro-Controlter，其riSc-V微控制器的验证大小超过了先前经过数量级的设计。在一项小型研究中，我们还发现氙气可以帮助非专家用户正确，更快地完成验证任务，速度比以前的最新工具更快。
We present Xenon, a solver-aided, interactive 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 synthesize a minimal set of secrecy assumptions in an interactive verification loop. To reduce verification time Xenon exploits modularity in Verilog code via module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable us to verify different kinds of circuits, including a highly modular AES- 256 implementation where modularity cuts verification from six hours to under three seconds, and the ScarVside-channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude. In a small study, we also find that Xenon helps non-expert users complete verification tasks correctly and faster than previous state-of-art tools.