In the rapidly evolving semiconductor industry, where research, design, verification, and manufacturing are intricately linked, the potential of Large Language Models to revolutionize hardware design and security verification is immense. The primary challenge, however, lies in the complexity of hardware-specific issues that are not adequately addressed by the natural language or software code knowledge typically acquired during the pretraining stage. Additionally, the scarcity of datasets specific to the hardware domain poses a significant hurdle in developing a foundational model. Addressing these challenges, this paper introduces Hardware Phi-1.5B, an innovative large language model specifically tailored for the hardware domain of the semiconductor industry. We have developed a specialized, tiered dataset—comprising small, medium, and large subsets—and focused our efforts on pretraining using the medium dataset. This approach harnesses the compact yet efficient architecture of the Phi-1.5B model. The creation of this first pre-trained, hardware domain-specific large language model marks a significant advancement, offering improved performance in hardware design and verification tasks and illustrating a promising path forward for AI applications in the semiconductor sector.

The increasing complexity of System-on-Chip (SoC) designs and the rise of third-party vendors in the semiconductor industry have led to unprecedented security concerns. Traditional formal methods struggle to address software-exploited hardware bugs, and existing solutions for hardware-software co-verification often fall short. This paper presents Microscope, a novel framework for inferring software instruction patterns that can trigger hardware vulnerabilities in SoC designs. Microscope enhances the Structural Causal Model (SCM) with hardware features, creating a scalable Hardware Structural Causal Model (HW-SCM). A domain-specific language (DSL) in SMT-LIB represents the HW-SCM and predefined security properties, with incremental SMT solving deducing possible instructions. Microscope identifies causality to determine whether a hardware threat could result from any software events, providing a valuable resource for patching hardware bugs and generating test input. Extensive experimentation demonstrates Microscope’s capability to infer the causality of a wide range of vulnerabilities and bugs located in SoC-level benchmarks.

Due to the globalization of the semiconductor supply chain, chip fabrication now involves multiple parties, including intellectual property (IP) vendors and Electronic Design Automation (EDA) tool vendors. Involving multiple entities and valuable IP naturally raises security and privacy concerns. Various frameworks and tools, such as the IEEE 1735 standard for IP protection, have been developed to mitigate the risk of theft. However, existing solutions fail to address all the threats envisioned by the zero-trust model. We propose a novel zero-trust formal verification framework that requires only two essential parties: IP users and IP vendors. This framework leverages secure multiparty computation to ensure the security and privacy of the hardware verification process. Our proposed solution allows IP users and IP vendors to independently convert the hardware design and assertions into conjunctive normal form (CNF), and then apply privacy-preserving SAT solving to verify the conformance of the design to the specification. This paper introduces a domain-specific secure decision procedure, hw-ppSAT, designed to overcome the scalability challenges of using SAT solving in hardware design verification. Our approach also leverages property-based hardware optimizations and domain-specific heuristics to enhance the verification process. We showcase the framework's effectiveness through its application to several open-source benchmarks.

Platooning of connected vehicles is a solution geared toward improving traffic throughput, highway safety, driving comfort, and fuel efficiency. These vehicles are equipped with Cooperative Adaptive Cruise Controller (CACC) that integrates information from dedicated short-range communication (DSRC) radio and sensors for safe navigation. The possibility of malicious attacks such as Denial of Service (DoS) or False Data Injection (FDI) on sensor data or control inputs tends to affect reliability, and jeopardize the safety of connected vehicles. Thus, securing sensor data of these vehicles from DoS or FDI attacks is essential to avoid unwanted consequences. To withstand sensor attacks, resilient state estimators have been developed for networked cyber-physical systems (CPS). However, such estimators do not perform well as the number of compromised sensors of the system increases. As such, we propose a novel convex optimization based Resilient Distributed State Estimator (RDSE) that bounds the state estimation error, irrespective of the magnitude of the attack and the number of compromised sensors. We theoretically prove that the proposed estimator has similar performance compared to the state-of-the-art Distributed Kalman Filter (DKF) under attack free and noise free scenarios. While under attack, our RDSE outperforms the DKF and we provide a theoretical bound on state estimation error generated by RDSE during an attack. We also demonstrate the effectiveness of RDSE against FDI attacks in a platoon with five vehicles and compare its performance during attack against the DKF and the Resilient Distributed Kalman Filter (RDKF).

The performance of resilient state estimators developed for cyber-physical systems (CPSs) decreases as the number of compromised sensors of the system increases. Furthermore, some of these algorithms leverage computationally expensive optimization techniques to incorporate resiliency. As such, we propose a fast resilient distributed state estimator (FRDSE), which is a novel resilient distributed algorithm that produces bounded state estimation errors regardless of the magnitude of the attack and the number of compromised sensors. Our algorithm converges to the true state in an attack-free and noise-free scenario and it produces bounded estimation errors during an attack. Compared to existing algorithms, FRDSE is more computationally efficient. We provide theoretical guarantees on the convergence of FRDSE in attack-free scenario and prove its resiliency during an attack. We demonstrate the performance of our algorithm against false data injection (FDI) attack in a platoon of vehicles and compare its runtime against existing algorithms. We observe that on a platoon of eight vehicles, runtime of our algorithm is 0.102 s, much lower than the state-of-the-art solutions.

Automotive systems have always been designed with safety in mind. In this regard, the functional safety standard, ISO 26262, was drafted with the intention of minimizing risk due to random hardware faults or systematic failure in design of electrical and electronic components of an automobile. However, growing complexity of a modern car has added another potential point of failure in the form of cyber or sensor attacks. Recently, researchers have demonstrated that vulnerability in vehicle's software or sensing units could enable them to remotely alter the intended operation of the vehicle. As such, in addition to safety, security should be considered as an important design goal. However, designing security solutions without the consideration of safety objectives could result in potential hazards. Consequently, in this paper we propose the notion of security for safety and show that by integrating safety conditions with our system-level security solution, which comprises of a modified Kalman filter and a Chi-squared detector, we can prevent potential hazards that could occur due to violation of safety objectives during an attack. Furthermore, with the help of a car-following case study, where the follower car is equipped with an adaptive-cruise control unit, we show that our proposed system-level security solution preserves the safety constraints and prevent collision between vehicle while under sensor attack.

The introduction of automation in cyber-physical systems (CPS) has raised major safety and security concerns. One attack vector is the sensing unit whose measurements can be manipulated by an adversary through attacks such as denial of service and delay injection. To secure an autonomous CPS from such attacks, we use a challenge response authentication (CRA) technique for detection of attack in active sensors data and estimate safe measurements using the recursive least square algorithm. For demonstrating effectiveness of our proposed approach, a car-follower model is considered where the follower vehicle's radar sensor measurements are manipulated in an attempt to cause a collision.

Part II of this paper series focuses on automation of the extended proof-carrying hardware intellectual property (PCHIP) framework for data secrecy protection in third-party IPs, which was presented in part I. Specifically, we introduce: 1) VeriCoq-IFT, an automated PCHIP framework for information flow policies and 2) VeriCoq-H, a hierarchy-preserving Verilog-to-Coq converter. VeriCoq-IFT aims to: 1) automate the process of converting designs from an HDL to the Coq formal language; 2) generate security property theorems ensuring compliance with information flow policies; 3) construct proofs for such theorems; and 4) check their validity in a design, with minimal user intervention. VeriCoq-H, on the other hand, seeks to convert the entire functionality of a Verilog design to its Coq representation while preserving design hierarchy. It facilitates the development of hierarchical proofs and enables the construction of hybrid module libraries containing the HDL code and the corresponding reusable lemmas for each module. Applicability of our automated VeriCoq-IFT framework is demonstrated by evaluating trustworthiness of two DES encryption circuits and several genuine and Trojan-infested advanced encryption standard (AES) designs, along with the utility of VeriCoq-H in preventing malicious modification of sensitive data, such as the secret key of an encryption circuit.

The wide usage of hardware intellectual property (IP) cores and software programs from untrusted third-party vendors has raised security concerns for computer system designers. The existing approaches, designed to ensure the trustworthiness of either the hardware IP cores or to verify software programs, rarely secure the entire computer system. The semantic gap between the hardware and the software lends to the challenge of securing computer systems. In this paper, we propose a new unified framework to represent both the hardware infrastructure and the software program in the same formal language. As a result, the semantic gap between the hardware and the software is bridged, enabling the development of system-level security properties for the entire computer system. Our unified framework uses a cross-domain formal verification method to protect the entire computer system within the scope of proof-carrying hardware. The working procedure of the unified framework is demonstrated with a sample embedded system which includes an 8051 microprocessor and an RC5 encryption program. In our demonstration, we show that the embedded system is trusted if the system level security properties are provable. Supported by the unified framework, the system designers/integrators will be able to formally verify the trustworthiness of the computer system integrated with hardware and software both from untrusted third-party vendors.

Proof-carrying hardware intellectual property (PCHIP) is a previously proposed framework for ensuring trustworthiness of third-party hardware IP through the development of formal proofs for security properties designed to prevent introduction of malicious behavior. Based on this framework, we introduce new approaches for assuring that the secrecy of internal information in a hardware design is not compromised by design flaws or malicious hardware Trojans. Specifically, we devise two PCHIP-based information flow tracking approaches, which enhance the formal PCHIP framework with secrecy tags and/or sensitivity levels in order to provide mechanisms for proving that sensitive information does not reach undesired sites. To assist in the development of data secrecy properties, we also introduce the concept of theorem generation functions, which enable generation of security theorems independent of the target circuit, thereby paving the way for proof automation. In addition, we enhance the PCHIP framework with a hierarchy-preserving methodology and we show its utility in preventing malicious data modification, which may indirectly result in sensitive information leakage, such as by modifying the secret key in a cryptographic core. This enhanced PCHIP framework also enables development of hybrid module libraries, which contain hardware description language code along with proofs of lemmas for these modules. These module libraries can then be used for hierarchically proving security properties in higher level designs, thereby reducing the proof development burden in the general PCHIP framework. Efforts toward automation of the proposed methodologies, as well as evaluation of their effectiveness in identifying design flaws or hardware Trojans in various cryptographic hardware designs are presented in part II of this paper series.

The wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with considerable reduction in verification effort.

Reusable hardware Intellectual Property (IP) based System-on-Chip (SoC) design has emerged as a pervasive design practice in the industry today. The possibility of hardware Trojans and/or design backdoors hiding in the IP cores has raised security concerns. As existing functional testing methods fall short in detecting unspecified (often malicious) logic, formal methods have emerged as an alternative for validation of trustworthiness of IP cores. Toward this direction, we discuss two main categories of formal methods used in hardware trust evaluation: theorem proving and equivalence checking. Specifically, proof-carrying hardware (PCH) and its applications are introduced in detail, in which we demonstrate the use of theorem proving methods for providing high-level protection of IP cores. We also outline the use of symbolic algebra in equivalence checking, to ensure that the hardware implementation is equivalent to its design specification, thus leaving little space for malicious logic insertion.