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可用于发现违反安全属性的多条路径，为安全验证提供新视角。