Modern Systems-on-Chips (SoCs) integrate numerous insecure intellectual properties to meet design-cost and time-to-market constraints. Incorporating these SoCs into security-critical systems severely threatens users’ privacy. Traditional formal/simulation-based verification techniques detect vulnerabilities to some extent. However, these approaches face challenges in detecting unknown vulnerabilities and suffer from significant manual efforts, false alarms, low coverage, and scalability. Several fuzzing techniques have been developed to mitigate pre-silicon hardware verification limitations. Nevertheless, these techniques suffer from major challenges such as slow simulation platforms, extensive design knowledge requirements, and lacking consideration of untrusted inter-module communications. To overcome these shortcomings, we developed FormalFuzzer, an emulation-based hybrid framework by combining formal verification and fuzz testing, leveraging their own benefits. FormalFuzzer incorporates formal-verification-based pre-processing using template-based assertion generation to narrow down the search space for fuzz testing and appropriate mutation strategy selection by dynamic feedback derived from a security-oriented cost function. The cost function is developed using vulnerability databases and specifications, indicating the likelihood of triggering a vulnerability. A vulnerability is detected when the cost function reaches global or local minima. Our experiments on RISC-V-based Ariane SoC demonstrate the efficiency of proposed formal-verification-based pre-processing strategies and cost function-driven feedback on fuzzing in detecting both known and unknown vulnerabilities expeditiously.

The modern System-on-Chips (SoCs), with numerous complex and heterogeneous intellectual properties (IPs), and the inclusion of highly-sensitive assets, become the target of malicious attacks. However, security verification of these SoCs remains behind compared to the advances in functional verification, mostly because it is difficult to formally define the accurate threat model(s). Few recent studies have investigated the possibility of engaging fuzz testing for hardware-oriented vulnerability detection. However, they suffer from several limitations, i.e., lack of cross-layer co-verification, the need for expert knowledge, and the inability to capture detailed hardware interactions. In this paper, we propose SoCFuzzer, an automated SoC verification assisted by fuzz testing for detecting SoC security vulnerabilities. Unlike the previous HW-oriented fuzz testing studies, which mostly rely on traditional (code) coverage-based metrics, in SoCFuzzer, we develop (i) generic evaluation metrics for fuzzing the hardware domain, and (ii) security-oriented cost function. This relieves designers of making correlations between coverage metrics, test data, and possible vulnerabilities. The SoCFuzzer cost functions are defined high level, allowing us to follow the gray-box model, which requires less detailed and interactive information from the design-under-test. Our experiments on an open-source RISCV based SoC show the efficiency of these metrics and cost functions on fuzzing for generating cornerstone inputs to trigger the vulnerability conditions with faster convergence.

Modern System-on-Chip (SoC) designs containing sensitive information have become targets of malicious attacks. Unfortunately, current verification practices still undermine the importance of SoCs security verification due to extreme time-to-market constraints, lack of autonomous methodologies, and low coverage. This results in SoC designs moving forward to production with security holes, making them insecure and exploitable by adversaries. Traditional taint analysis and formal approaches are losing applicability to industrial applications due to labor-intensive, slow, and scalability issues. Some approaches apply fuzz testing for hardware vulnerability detection using state-of-the-art software fuzzers, also utilizing information flow tracking for better coverage. However, these approaches prove to be inefficient and cannot be applied to SoCs integrated with third-party IPs (3PIP) for several reasons: laborious white-box-based taint analysis, inconsiderate cross-layer co-verification, and lacking hardware-centric input mutations. This paper proposes Taintuzzer, a fuzzing-driven automated SoC security verification framework leveraging taint inference (feasible in gray-box verification) for detecting SoC security vulnerabilities. Unlike previous studies relying on traditional (code) coverage-related metrics, in TaintFuzzer, we develop (i) schemes for generating smart seeds, (ii) a security-oriented cost function, and (iii) run-time feedback for the mutation engine to choose the appropriate strategies to mutate stimuli targeting SoC modules. TaintFuzzer is powered by FPGA emulation of SoC, making it extremely fast and scalable, especially for cross-layer co-verification. TaintFuzzer's cost function and feedback enable dynamic tuning of mutation strategies to generate hardware-centric inputs. Our experiments with RISC-V-based SoC demonstrate the TaintFuzzer's effectiveness in detecting both known and unknown vulnerabilities in significantlv less time.

Buffer overflow is one of the most critical software vulnerabilities with numerous functional and security impacts on memory boundaries and program calls. An exploitable buffer overflow, which can be directly or indirectly triggered through external user domain inputs, is of a greater concern because it can be misused during run-time for adversarial intention. Although some existing tools offer buffer overflow detection to certain extents, there are major limitations, such as, poor detection coverage and ad-hoc/manual verification efforts due to inadequate predefined executions for static analysis and substantially large input subspace for dynamic verification. In this paper, to provide program verification in static time with high detection coverage, we propose an automated framework for Exploitable Buffer Overflow Detection by Information Flow Tracking (BOFT). We achieve this goal following three steps - first, BOFT analyzes the usage of arrays, pointers, and vulnerable application programming interface (APIs) in the program code and automatically inserts assertions required for buffer overflow detection. Second, BOFT instruments the program with taints for direct and indirect information flow tracking using an extensive set of formal expressions. Finally, it symbolically analyzes the instrumented code for maximum coverage and provides the list of exploitable buffer overflow vulnerabilities. BOFT is evaluated on standard benchmarks from SAMATE Juliet Test Suite (NIST) with a successful detection of ~94.87% (minimum) of exploitable buffer overflows with zero false positives.