Clepsydra: Modeling timing flows in hardware designs
Clepsydra: Modeling timing flows in hardware designs
复制标题
DOI：
10.1109/iccad.2017.8203772
复制
发表时间：
2017-11
期刊：
影响因子：
--
通讯作者：
Armaiti Ardeshiricham;Wei Hu;R. Kastner
中科院分区：
文献类型：
--
作者：
Armaiti Ardeshiricham;Wei Hu;R. Kastner
侧信道安全攻击的出现挑战了关于什么数据是公开可用的经典假设。事实一再证明，通过测量硬件设计完成时间收集的信息进行统计分析可以揭示机密信息。尽管基于时间的侧信道泄漏很容易被利用来破坏数据隐私，但传统的硬件验证工具尚不适合评估这些漏洞。为了使硬件设计过程熟悉正式的安全评估，我们引入了一个通过HDL代码跟踪基于时间的信息流的模型。基于该模型，我们开发了Clepsydra，这是一种自动生成电路的工具，用于在两个不同通道的硬件设计中跟踪时序流和通用逻辑流。通过EDA工具可以对Clepsydra产生的电路进行分析，以检测时序泄漏或正式证明恒定的执行时间。我们提出了关于所提出模型的可靠性和精度的证明，以及使用Clepsydra在各种硬件单元（包括加密核心，总线架构，缓存和算术模块）上验证安全属性的结果。
Emergence of side channel security attacks has challenged the classic assumptions regarding what data is publicly available. As demonstrated repeatedly, statistical analysis of information collected by measuring completion time of hardware designs can reveal confidential information. Even though timing-based side channel leakage can be easily exploited to breach data privacy, conventional hardware verification tools are not yet suited to assess these vulnerabilities. To acquaint the hardware design process with formal security evaluations, we introduce a model for tracking timing-based information flows through HDL codes. Based on this model, we have developed Clepsydra, a tool for automatically generating circuitry for tracking timing flows and generic logical flows within hardware designs in two distinct channels. The circuit generated by Clepsydra can be analyzed by EDA tools to detect timing leakage or formally prove constant execution time. We present proofs regarding soundness and precision of the proposed model along with results of employing Clepsydra to verify security properties on a variety of hardware units including crypto cores, bus architectures, caches and arithmetic modules.