Augmented Symbolic Execution for Information Flow in Hardware Designs

TL;DR

SEIF is a novel methodology combining static analysis and symbolic execution to verify and explain information flow paths in hardware designs, enabling efficient security verification and path exploration.

Contribution

It introduces SEIF, a new approach that integrates static analysis with guided symbolic execution for precise information flow verification in hardware.

Findings

SEIF can explore 10-12 clock cycles deep in 4-6 seconds.

It accounts for 86-90% of paths in the static model.

SEIF can find multiple security violation paths.

Abstract

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.