Symbolic execution of hardware designs is a path-based analysis that can deliver high quality coverage and security verification results. Unfortunately, the technique has historically struggled with the path explosion problem and, despite recent advances, remains expensive. We present SylQ-SV, a dedicated SystemVerilog symbolic execution engine that uses SMT query caching to improve execution times, reducing run time by up to 17% over the state of the art. SylQ-SV provides language support for all necessary SystemVerilog constructs, including SystemVerilog Assertions, to provide end-to-end verification workflows of the open-source designs most commonly appearing in the literature. We evaluate SYLQ-SV on the OR1200 CPU, the OpenTitan SoC with Ibex core, and two SoC designs from the HACK@DAC competitions (with PULPissimo core and CVA6 core, respectively). We make the SylQ-SV source code and all data used in the evaluation publicly available.

We introduce a symbolic execution-based framework to generate the environment constraints needed to formally verify a hardware design. The core of the approach is a new search strategy that leverages piecewise composition, a divide-and-conquer algorithm introduced in prior work, to guide symbolic execution toward paths more likely to generate needed environment constraints. In our preliminary evaluation using the decoder module of the OpenTitan SoC, the framework finds the needed constraints without overconstraining the environment.

Symbolic execution is a path-based symbolic analysis that is emerging as a versatile and effective method for security verification of hardware designs. In this paper we describe symbolic execution, explain why it is so well suited to the hardware design space, and present our recent work designing symbolic execution for the security verification of hardware designs.

Hardware security creates a hardware-based security foundation for secure and reliable operation of systems and applications used in our modern life. The presence of design for security, security assurance, and general security design life cycle practices in product life cycle of many large semiconductor design and manufacturing companies these days indicates that the importance of hardware security has been very well observed in industry. However, the high cost, time, and effort for building security into designs and assuring their security - due to using many manual processes - is still an important obstacle for economy of secure product development. This paper presents several promising directions for automation of design for security and security assurance practices to reduce the overall time and cost of secure product development. First, we present security verification challenges of SoCs, possible vulnerabilities that could be introduced inadvertently by tools mapping a design model in one level of abstraction to its lower level, and our solution to the problem by automatically mapping security properties from one level to its lower level incorporating techniques for extension and expansion of the properties. Then, we discuss the foundation necessary for further automation of formal security analysis of a design by incorporating threat model and common security vulnerabilities into an intermediate representation of a hardware model to be used to automatically determine if there is a chance for direct or indirect flow of information to compromise confidentiality or integrity of security assets. Finally, we discuss a pre-silicon-based framework for practical and time-and-cost effective power-side channel leakage analysis, root-causing the side-channel leakage by using the automatically generated leakage profile of circuit nodes, providing insight to mitigate the side-channel leakage by addressing the high leakage nodes, and assuring the effectiveness of the mitigation by reprofiling the leakage to prove its acceptable level of elimination. We hope that sharing these efforts and ideas with the security research community can accelerate the evolution of security-aware CAD tools targeted to design for security and security assurance to enrich the ecosystem to have tools from multiple vendors with more capabilities and higher performance.