Kaki Ryan
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Research Subjects
Research Interests
Kaki Ryan has a total of 2 co-authors. Here are the top co-authors by number of shared publications:
- Cynthia Sturton
University of North Carolina at Chapel Hill
2 shared publications - Matthew Gregoire
University of North Carolina at Chapel Hill, Chapel Hill, USA
1 shared publication
Latest Publications
- Open Access
- 6 August 2025
- Published by Association for Computing Machinery (ACM)
- p. 195-211
SYL Q-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching
- 6 August 2025
- Published by Association for Computing Machinery (ACM)
- p. 195-211
Open AccessSYL Q-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching
- Open Access
- 29 October 2023
- Published by Association for Computing Machinery (ACM)
- p. 1-9
SEIF: Augmented Symbolic Execution for Information Flow in Hardware Designs
We present SEIF, an exploratory methodology for information flow verification based on symbolic execution. SEIF begins with a statically built overapproximation of the information flow through a design and uses guided symbolic execution to provide a more precise picture of how information flows from a given set of security critical signals. SEIF can recognize and eliminate non-flows with high precision and for the true flows can find the corresponding paths through the design state with high coverage. We evaluate SEIF on two open-source CPUs, an AES core, and the AKER access control module. SEIF can be used to find counterexamples to information flow properties, and also to explore all flows originating from a source signal of interest. SEIF accounts for 86–90% of statically identified possible flows in three open-source designs. SEIF’s search strategies enable exploring the designs for 10-12 clock cycles in 4-6 seconds on average, demonstrating that this new exploratory style of information flow analysis can be practical.
- 29 October 2023
- Published by Association for Computing Machinery (ACM)
- p. 1-9
Open AccessSEIF: Augmented Symbolic Execution for Information Flow in Hardware Designs
We present SEIF, an exploratory methodology for information flow verification based on symbolic execution. SEIF begins with a statically built overapproximation of the information flow through a design and uses guided symbolic execution to provide a more precise picture of how information flows from a given set of security critical signals. SEIF can recognize and eliminate non-flows with high precision and for the true flows can find the corresponding paths through the design state with high coverage. We evaluate SEIF on two open-source CPUs, an AES core, and the AKER access control module. SEIF can be used to find counterexamples to information flow properties, and also to explore all flows originating from a source signal of interest. SEIF accounts for 86–90% of statically identified possible flows in three open-source designs. SEIF’s search strategies enable exploring the designs for 10-12 clock cycles in 4-6 seconds on average, demonstrating that this new exploratory style of information flow analysis can be practical.