Recent years have seen significant advances in using formal verification to check hardware security properties. Of particular practical interest are checking confidentiality and integrity of secrets, by checking that there is no information flow between the secrets and observable outputs. A standard method for checking information flow is to translate the corresponding non-interference hyperproperty into a safety property on a self-composition of the design, which has two copies of the design composed together. Although prior efforts have aimed to reduce the size of the self-composed design, there are no state-of-the-art model checkers that exploit their special structure for hardware security verification. In this paper, we propose SecIC3, a hardware model checking algorithm based on IC3 that is customized to exploit this self-composition structure. SecIC3 utilizes this structure in two complementary techniques: symmetric state exploration and adding equivalence predicates. We implement SecIC3 on top of two open-source IC3 implementations and evaluate it on a non-interference checking benchmark consisting of 10 designs. The experiment results show that SecIC3 significantly reduces the time for finding security proofs, with up to 49.3x proof speedup compared to baseline implementations.

翻译：近年来，利用形式化验证技术检验硬件安全属性取得了显著进展。其中具有重要实践意义的课题是通过检查秘密信息与可观测输出之间是否存在信息流，来验证秘密信息的机密性与完整性。检验信息流的标准方法是将对应的非干扰超属性转化为设计自组合上的安全性属性，该自组合由两个相同设计副本组合而成。尽管先前研究致力于缩减自组合设计的规模，但目前尚无利用其特殊结构进行硬件安全验证的先进模型检测器。本文提出SecIC3——一种基于IC3框架并针对自组合结构定制化的硬件模型检测算法。SecIC3通过两种互补技术利用该结构：对称状态探索与等价谓词添加。我们在两个开源IC3实现基础上构建了SecIC3，并在包含10个设计的非干扰检验基准集上进行评估。实验结果表明，SecIC3能显著缩短安全证明的生成时间，与基线实现相比最高可获得49.3倍的证明加速比。