发表机构
Princeton University; MIT CSAIL; EPFL（普林斯顿大学; 麻省理工学院计算机科学与人工智能实验室; 洛桑联邦理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对RTL仿真中污点逻辑开销过大的问题，提出CEGAR-T框架，自动合成最小化插桩开销且无误报的污点逻辑，在RISC-V核上大幅降低插桩和仿真开销。
AI 中文摘要
寄存器传输级（RTL）仿真被广泛用于硬件制造前的测试。为了测试与安全相关的信息流属性，如机密性和完整性，可以自动向设计添加污点逻辑以跟踪信息如何流经设计。然而，由最先进技术（如CellIFT）插桩的污点逻辑使得基于仿真的测试成本过高：在我们对Mega-BOOM（136K个单元）的评估中，它使插桩后的设计达到原始单元数量的5.81倍，并导致143.72倍的仿真减速。污点逻辑可以简化以提高仿真速度，但这将不可避免地牺牲其精度。这种轻量级、不精确的污点逻辑会引入误报，并可能最终导致检查这些误报的额外开销。本文探讨了在设计中究竟哪里需要精度以克服误报开销的研究问题。它提出了CEGAR-T，一个自动合成污点逻辑的框架，该框架在保证无误报（相对于精确的CellIFT基线）的同时最小化污点逻辑插桩开销。我们已实现CEGAR-T，并在开源RISC-V核上针对时序侧信道安全的指令集安全问题上进行了评估。在所有评估的核上，CEGAR-T将插桩和仿真开销的几何平均值分别从5.64倍降低到1.42倍，从34.65倍降低到1.79倍，且不损害CellIFT基线的精度优势。
英文摘要
Register-Transfer Level (RTL) simulation is widely used to test hardware before it is fabricated. To allow testing for security related information flow properties, such as confidentiality and integrity, taint logic can be automatically added to the design to track how information flows through it. However, taint logic instrumented by the state-of-the-art, such as CellIFT, makes simulation-based testing prohibitively expensive: On our evaluation of Mega-BOOM (136K cells), it increases the instrumented design to 5.81x the original cell count and causes a 143.72x simulation slowdown. The taint logic could be simplified to improve simulation speed, but it will inevitably trade off its precision. This lightweight, imprecise taint logic will introduce false positives and may eventually result in even more overhead to check these false positives. This paper explores the research question of where precision is actually needed in the design to overcome the overhead of false positives. It presents CEGAR-T, a framework that automatically synthesizes taint logic that minimizes the taint-logic instrumentation overhead while guaranteeing no false positives (relative to the precise CellIFT baseline). We have implemented CEGAR-T and evaluated it on the safe instruction set problem for timing side-channel security across open-source RISC-V cores. Over all evaluated cores, CEGAR-T reduces both instrumentation and simulation overhead, in geometric-mean, from 5.64x to 1.42x and from 34.65x to 1.79x, respectively, without compromising the precision benefit of the CellIFT baseline.
