Automated Rule Checking for Hardware Security
System-on-chips (SoCs) are increasingly being used in high assurance electronic systems such as military, space, automotive, banks, health care, etc. These systems have strict security requirements because their failure can damage major financial infrastructure, endanger personal privacy, and undermine the viability of whole business sector. It has been demonstrated that the security of SoCs can be compromised using information leakage, timing and power side-channel attacks, exploitation of design-for-test (DFT) structures, and fault-injection attacks. These attacks can effectively bypass the security mechanisms built in the software level and put chips or systems at risk. Further, due to the globalization of the semiconductor design and fabrication process, SoCs are vulnerable to malicious modifications, referred to as hardware Trojans, during design process (from RTL to Gate level to Physical Design) and manufacturing phase. Apart from the vulnerabilities exposed by these attacks, many security vulnerabilities in SoCs can be unintentionally created by design mistakes and the designer’s lack of understanding of security problems. Further, computer-aided design (CAD) tools can introduce additional vulnerabilities in the SoC unintentionally. The objective of this projectl is to develop a comprehensive framework for automated rule checking for hardware security, for analyzing the security issues and vulnerabilities in SoC designs, including potential untrusted third-party IPs, from RTL to layout.
In this project, we aim to
- Develop novel and efficient security properties and security-aware design rules to systematically identify security issues and vulnerabilities during pre-silicon design and verification stage
- Assess how critical the vulnerability is with design-level metrics, rules, and threat levels
- Allow design-level fixes, with automation and integrated tool sets for asset protection and address security vulnerabilities as early as possible in the design process
- Provide guidance to the designers for risk versus effort assessment based on the security level
Sponsors: DARPA, ANSYS, DoD
CAD Framework for Detecting and Mitigating Security Vulnerabilities in High-level Synthesis
High-level Synthesis (HLS) is an effective solution to cope with the ever-growing demand for increasing design and verification productivity of semiconductor design flow, especially with the emergence of artificial intelligence (AI) hardware and FPGA-as-a-service. It offers unparalleled possibility of speeding up the time-to-market by allowing the design and verification engineers to implement efficiently complex algorithms as well as custom logics design in higher levels of abstraction, e.g., C/C++. HLS is increasingly being adopted by government (e.g., DARPA CRAFT program) and commercial (e.g., Nvidia, Qualcomm, Intel, and Mentor Graphics) entities. Although, many research endeavors have been directed to optimize and increase the efficiency of HLS (e.g., GRC Task 2807.001, 2506.001), none have investigated potential security vulnerabilities introduced by HLS and to identify and mitigate these vulnerabilities automatically. Security vulnerabilities introduced by HLS during transformation could be exploited to leak sensitive information and perform other possible attacks e.g., denial of service, reduction in reliability, etc.
In this project, we plan to (1) investigate potential security issues introduced by the high-level synthesis (HLS) process, (2) develop CAD framework to identify these security vulnerabilities in an automated manner, and (3) develop secure high-level coding practices and countermeasures (similar to Cert-C) to help prevent such vulnerabilities during HLS.
Current Sponsors: SRC
Automated Verification and Debugging using Formal Methods
In our past projects, we proposed a novel verification technique using Gröbner basis theory to formulate the equivalence checking problem as an ideal membership testing in the algebraic domain and achieve an efficient verifier. This approach is capable of identifying bugs in a deterministic way since word-level representations are utilized.
Existing equivalence checking techniques utilize Gröbner basis theory to produce a remainder to indicate the presence of a potential bug. However, bug localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests are not effective and can be infeasible for complex arithmetic circuits. In our past projects, we developed an automated test generation and bug localization technique for debugging arithmetic circuits. Our approach is able to automatically generate directed tests by suitable assignments of input variables to make the reminder non-zero. The generated tests are guaranteed to activate the unknown bugs. We also proposed a bug detection and correction technique by utilizing the patterns of remainder terms as well as the intersection of regions activated by the generated tests. In her recent work, we have addressed the scalability concerns associated with equivalence checking that leads to an explosion in size of the remainder when the design is faulty. We developed an incremental equivalence checking method which is capable of localizing and correcting hard-to-detect bugs irrespective of their location in the design. In our current project, we plan to use Grobner basis theory for approximate hardware generation and its automatic debugging.
- Automated test generation for debugging multiple bugs in arithmetic circuits
- Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis Reduction
Design Automation of Modeling IoT Devices
Design of IoT devices starts with a high-level model of Internet-of-Things (IoT) devices as well as their constraints. Modeling of heterogeneous IoT devices, as well as their connectivity, is a major challenge due to the huge complexity coupled with the diversity of the computing models. After models and constraints are finalized, they should be validated and converted to actual hardware using efficient design exploration, fast prototyping, and effective design transformations. This modeling and validation would lead to the development of novel Electronic Design Automation (EDA) tools to enable automated generation of executable models and prototypes for CMOS as well as post-CMOS technologies. My research aims for correct-by-construction design automation methodology. In this project, we design EDA tools that generate high-level models based on the design constraints and perform verification of transformation steps from models to hardware chips. The automated framework would enable design exploration, automatic software generation, high-level synthesis, quick prototyping, and automatic patching. It is also extremely important to have EDA tools that can check for all vulnerabilities in all phases of the design since it may be infeasible to patch later. The tools must be able to predict various vulnerabilities such as reverse engineering, and fault injection attacks with warnings and possible solutions.
- Security-aware FSM Design Flow for Identifying and Mitigating Vulnerabilities to Fault Attacks
- FSM Anomaly Detection Using Formal Analysis
Verification of IoT System-on-Chips
Modern SoC design technology has been a centerpiece in computing system architecture because of diverse applications such as smartphones, tablets, automotive systems, medical instruments, etc. It is very important to design robust and trustworthy SoCs. In this project, we plan to explore the following avenues to verify IoT SoCs, 1) use of analytics, formal validation, as well as machine learning techniques for scalable validation, and 2) streamlined architecture for effective post-silicon and in-field control and requirements update. Faster bug localization is one of the most important steps in design validation. A major problem with design validation is that we do not know whether a bug exists, and how to quickly detect and fix it. In this project, we use machine learning to implement verification tools that automatically detect the source of errors based on prior knowledge and verification efforts. The goal of this research is to reduce validation efforts by avoiding debugging known failures. In this project, we also plan to generate test patterns using machine learning. While directed tests can check for known errors, machine learning can extend to scope for both known and unknown (e.g., known errors with minor or major variations) SoC functional vulnerabilities.
We also aim for effective utilization of three widely used formal methods (equivalence checking, model checking, and theorem proving) for scalable validation techniques. Effective in-field debug should be performed in the case of buggy fabricated silicon. Post-silicon validation and debug is critical for IoT applications, where the device may need to be updated during its long lifetime, or in response to changing functional needs or new requirements.
Current Sponsor: Cisco
Post-Silicon Validation and Debug
Post-silicon validation is widely acknowledged as a major
In our past project, we proposed novel post-silicon validation techniques to ensure the correct behavior of silicon designs based on coverage analysis. Currently, there is no effective way to collect coverage of certain properties and events directly and independently on silicon. We explored how to utilize on-chip
There is an inherent conflict between increasing the observability and trust. Although designing effective debug infrastructures can drastically reduce the post-silicon validation and debug efforts by increasing the observability, the extra observability can facilitate integrity issues such as trace buffer attack and scan-based side channel attack. We plan to explore designing debug infrastructures that they do not violate any integrity constraints.