We present SEIF, a methodology that combines static analysis with symbolic execution to verify and explicate information flow paths in a hardware design. SEIF begins with a statically built model of the information flow through a design and uses guided symbolic execution to recognize and eliminate non-flows with high precision or to find corresponding paths through the design state for true flows. We evaluate SEIF on two open-source CPUs, an AES core, and the AKER access control module. SEIF can exhaustively explore 10-12 clock cycles deep in 4-6 seconds on average, and can automatically account for 86-90% of the paths in the statically built model. Additionally, SEIF can be used to find multiple violating paths for security properties, providing a new angle for security verification.

翻译：我们提出SEIF方法，该方法将静态分析与符号执行相结合，用于验证和阐明硬件设计中的信息流路径。SEIF首先构建设计的信息流静态模型，然后通过引导式符号执行以高精度识别并消除非信息流，或为真实信息流找到对应的设计状态路径。我们在两个开源CPU、一个AES核心以及AKER访问控制模块上评估了SEIF。SEIF能在平均4-6秒内穷举探索10-12个时钟周期深度，并能自动解释静态模型中86-90%的路径。此外，SEIF可用于发现违反安全属性的多条路径，为安全验证提供新视角。