Symbolic Execution for Hardware
Exploitable bugs in hardware designs present an enticing target to attackers. As demonstrated by the Spectre and Meltdown attacks, bugs in hardware designs can have wide-reaching consequences and can be difficult to patch post-deployment. By making symbolic execution feasible for large scale hardware designs, we provide a new, effective, and practical method for the hardware designer to use in the ever-present race to detect vulnerabilities before tape-out.
Publications
-
End-to-End Automated Exploit Generation for Diagnosing Processor Designs
R. Zhang, C. Deutschbein, P. Huang, C. Sturton
IEEE/ACM International Symposium on Microarchitecture
(MICRO) 2018.
Nominated for Best Paper award
-
A Recursive Strategy for Symbolic Execution to Find Exploits in Hardware Designs
R. Zhang, C. Sturton
ACM SIGPLAN International Workshop on Formal Methods and Security (FMS), co-located with PLDI 2018.
Funding
This material is based upon work supported by the National Science Foundation under Grants No. 1816637.
