Click here to flash read.
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.
No creative common's license