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 ubiquitous presence and utilization of System-on-Chips (SoCs) have made them critical to our daily life. As SoCs become more complex to meet multiple applications, their susceptibility to security threats has also increased. The comprehensive security assurance of an SoC system requires a deep knowledge of the design and security-critical assets that must be protected. As SoC applications vary, the assets vary in number, type, importance-level, and form based on the various hardware blocks that construct the SoC and their complex interactions. Some assets are distinctive in their definition and characteristics, making them easily identifiable, such as encryption/decryption keys, logic locking keys, etc. However, other assets, such as system bus control registers that are internal to the design, require a more complex design analysis. Automatic identification of these security assets at the pre-silicon stage can help designers take the necessary precautions to protect them. Equipped with the security assets, designers can then incorporate techniques to protect these security assets against various threats such as information leakage, side-channel leakage, access control violations, and more. This paper presents the variation among security assets based on hardware design and defines specific attributes to help classify them. Then, we introduce SAIF, an automated framework that can help identify security assets for a design at the register-transfer level (RTL). We introduce a set of metrics into SAIF to perform comprehensive vulnerability analysis and identify security assets that are prone to specific vulnerabilities. Lastly, we report our findings on the effectiveness of SAIF for various open-source hardware designs and finalists of the National Institute of Standards and Technology (NIST) lightweight crypto standardization process such as ASCON, GIFT-COFB & Romulus. We show that SAIF can automatically identify critical security assets in a design with high accuracy and performance. Moreover, we analyze the security implication of the identified secondary assets to show their importance in pre-silicon security verification.

The globalization of the System-on-Chip (SoC) design process has made hardware designs prone to many security vulnerabilities. One of the most critical security vulnerabilities is information leakage (IL), which allows an attacker to gain access to a design’s secret information. IL vulnerabilities can result from unintended design flaws or the intentional insertion of malicious functionality into the design. Such vulnerabilities should be identified at the early design stages to secure a hardware design. Property-driven security verification has emerged as a promising method of verifying that such security vulnerabilities do not exist. This verification technique requires developing an appropriate set of assertions to formally represent the properties. However, forming a comprehensive set of assertions that can cover all potential vulnerabilities in design is challenging. Assertion generation cannot be done manually due to the large complexity of designs, lack of security experts as well as the existence of untrusted observable points in the design. In this work, we propose AGILE, a framework to automatically generate security assertions for property-driven verification to identify IL-based vulnerabilities. The experimental results show that the assertions provided by AGILE can detect both intentional and unintentional IL paths in the input design. We demonstrate the effectiveness of AGILE on the NIST standard, Trust-Hub, and OpenCores benchmarks. Moreover, we use code coverage analysis to evaluate the accessibility of the generated assertions to the source code. The analytical result indicates that by utilizing the assertions generated by AGILE, security coverage of the design under verification (DUV) can be improved significantly.

Due to the increasing size and complexity of system-on-chips (SoCs), new threats and vulnerabilities are emerging, mainly related to flaws at the system level. Due to the lack of decisive security requirements and properties from the perspective of the SoC designer, the system-level verification process, whose violation may lead to exploiting a hardware vulnerability, is not studied comprehensively. To enable more comprehensive verification of system-level properties, this paper presents a framework known asHUnTer(Hardware Underath Trigger) for identifying sets of instructions (sequences) at the processor unit (PU) that reveal the underlying hardware vulnerabilities. HUnTer automates (i) threat modeling, (ii) threat-based formal verification, (iii) generating counterexamples, and (iv) generating snippet code to exploit the vulnerability. Furthermore, the HUnTer framework defines a unique security coverage metric (HUnT_Coverage) to measure the performance and effectiveness of vulnerability exploits. To demonstrate the high effectiveness of the proposed framework, we conduct a wide variety of case studies using the HUnTer framework on RISC-V-based open-source SoC architecture and attains the security coverage of 86% as an average for 11 benchmarks of the Trust-Hub database.

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.

A number of security vulnerability assessments require accurate and fast extraction of the finite state machines (FSMs) in the circuit. FSM should be accurately extracted for watermark insertion, FSM-based logic locking, fault injection assessment of control paths in a system-on-chip (SoC), information leakage assessment, and reverse engineering at gate-level. Unfortunately, as of today, there are no good solutions available that can provide very fast and accurate extraction of FSMs from the flattened netlist to perform effective security assessment. The difficulty of developing such a solution lies in precisely identifying FSM state flip-flops present in a netlist that contains numerous circuit flip-flops. In this paper, we propose to develop a framework called FSMx to extract FSMs from highly unstructured synthesized designs. FSMx utilizes graph theory to identify FSM state registers from other registers. FSMx automatically extracts gate-level state transition graphs (STGs) for each of the detected FSM state registers. Experimental results demonstrate that FSMx efficiently recovers FSMs from synthesized netlists with various complexity and size in less than 7 minutes in the worst case of NIST AES 128-bit design with 12,976 gates on a personal desktop.

With the increasing complexity, modern system-onchip (SoC) designs are becoming more susceptible to security attacks and require comprehensive security assurance. However, establishing a comprehensive assurance for security often involves knowledge of relevant security assets. Since modern SoCs contain myriad confidential assets, the identification of security assets is not straightforward. The number and types of assets change due to numerous embedded hardware blocks within the SoC and their complex interactions. Some security assets are easily identifiable because of their distinct characteristics and unique definitions, while others remain in the blind-spot during design and verification and can be utilized as potential attack surfaces to violate confidentiality, integrity, and availability of the SoC. Therefore, it is essential to automatically identify security assets in an SoC at pre-silicon design stages to protect them and prevent potential attacks. In this paper, we propose an automated CAD framework called SAF to identify an SoC's security assets at the register transfer level (RTL) through comprehensive vulnerability analysis under different threat models. Moreover, we develop and incorporate metrics with SAF to quantitatively assess multiple vulnerabilities for the identified security assets. We demonstrate the effectiveness of SAF on MSP430 micro-controller and CEP SoC benchmarks. Our experimental results show that SAF can successfully and automatically identify an SoC's most vulnerable underlying security assets for protection.

Optical probing, though developed as silicon debugging tools from the chip backside, has shown its capability of extracting secret data, such as cryptographic keys and user identifications, from modern system-on-chip devices. Existing optical probing countermeasures are based on detecting any device modification attempt or abrupt change in operating conditions during asset extraction. These countermeasures usually require additional fabrication steps and cause area and power overheads. In this article, we propose a novel low-overhead design methodology to prevent optical probing. It leverages additional operational logic gates, termed as “CONCEALING-Gates,” inserted as neighbor gates of the logic gates connected to the nets carrying asset signals. The switching activity of the asset carrying logic is camouflaged with the switching activity of the concealing-gate. The input signal and placement in the layout of the concealing-gates must be selected in such a way that they remain equally effective in preventing different variants of optical probing, i.e., electro-optical frequency mapping and Electro-optical probing. The methodology is suitable for the existing ASIC/FPGA design flow and fabrication process, since designing new standard logic cells is not required. We have performed a comprehensive security evaluation of the concealing-gates using a security metric developed based on the parameters that are crucial for optical probing. The attack resiliency of the logic cells, protected by concealing-gates, is evaluated using an empirical study-based simulation methodology and experimental validation. Our analysis has shown that in the presence of concealing-gates, logic cells achieve high resiliency against optical contactless probing techniques.

Security of a system-on-chip (SoC) can be weakened by exploiting the inherent and potential vulnerabilities of the intellectual property (IP) cores used to implement the design as well as the interaction among the IPs. These vulnerabilities not only increase the security verification effort but also can increase design complexity and time-to-market. If the design and verification engineers are equipped with a comprehensive set of security properties at the early stage of a design process, SoC security validation effort can be greatly reduced. In this paper, we propose a property-driven approach to design a secure SoC. Our goal is to develop a comprehensive set of reusable and architecture-agnostic properties acting as security-aware design rules and guidelines. Moreover, we develop metrics from these properties to facilitate quantitative security assessment. Finally, we present design examples to demonstrate the efficacy of our approach under different threat models.