| Title | Accelerating SoC Security Verification and Vulnerability Detection Through Symbolic Execution |
| Publication Type | Conference Paper |
| Year of Publication | 2022 |
| Authors | Tang, Shibo, Wang, Xingxin, Gao, Yifei, Hu, Wei |
| Conference Name | 2022 19th International SoC Design Conference (ISOCC) |
| Keywords | C++ languages, codes, compiler security, compositionality, Costs, formal verification, Hardware, hardware security, KLEE, Metrics, model checking, pubcrawl, Resiliency, Scalability, secure SoC design, Symbiosis, symbolic execution, system-on-chip |
| Abstract | Model checking is one of the most commonly used technique in formal verification. However, the exponential scale state space renders exhaustive state enumeration inefficient even for a moderate System on Chip (SoC) design. In this paper, we propose a method that leverages symbolic execution to accelerate state space search and pinpoint security vulnerabilities. We automatically convert the hardware design to functionally equivalent C++ code and utilize the KLEE symbolic execution engine to perform state exploration through heuristic search. To reduce the search space, we symbolically represent essential input signals while making non-critical inputs concrete. Experiment results have demonstrated that our method can precisely identify security vulnerabilities at significantly lower computation cost. |
| DOI | 10.1109/ISOCC56007.2022.10031481 |
| Citation Key | tang_accelerating_2022 |
Accelerating SoC Security Verification and Vulnerability Detection Through Symbolic Execution