SecIC3: Customizing IC3 for Hardware Security Verification

TL;DR

SecIC3 is a specialized hardware model checking algorithm based on IC3, designed to efficiently verify security properties like non-interference by exploiting the structure of self-composed designs, achieving significant speedups.

Contribution

This paper introduces SecIC3, a novel IC3-based verification method that leverages self-composition structure for hardware security, with implementations demonstrating substantial performance improvements.

Findings

SecIC3 reduces verification time by up to 49.3x.

It effectively exploits self-composition structure for security verification.

Experimental results show significant speedups over baseline methods.

Abstract

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.