Hardware accelerators (HAs) underpin high-performance and energy-efficient digital systems. Correctness of these systems thus depends on the correctness of constituent HAs. Self-consistency-based pre-silicon verification techniques, like A-QED (Accelerator Quick Error Detection), provide a quick and provably thorough HA verification framework that does not require extensive design-specific properties or a full functional specification. However, A-QED is limited to verifying HAs which are non-interfering – i.e., they produce the same result for a given input independent of its context within a sequence of inputs. We present a new technique called G-QED (Generalized QED) which goes beyond non-interfering HAs while retaining A-QED’s benefits. Our extensive results as well as a detailed industrial case study show that: G-QED is highly thorough in detecting critical bugs in well-verified designs that otherwise escape traditional verification flows while simultaneously improving verification productivity 18-fold (from 370 person days to 21 person days). These results are backed by theoretical guarantees of soundness and completeness.

The security of hardware intellectual properties (IPs) has become a significant concern, as the opportunity for piracy, reverse engineering, and malicious modification is increasing. Hardware obfuscation has been studied as a potent method to protect against all these attack vectors. However, most of the existing obfuscation techniques have been successfully compromised, where many inherent functional or structural vulnerabilities in these techniques are utilized to reveal the obfuscation key or retrieve the original design. In this article, we introduce LeGO, a learning-guided obfuscation framework that overcomes known vulnerabilities in a scalable and systematic manner, leading to a robust and lightweight locking mechanism. The proposed framework is guided by our security evaluation process that performs a thorough assessment of an obfuscated IP against various attacks and identifies the vulnerabilities. It then judiciously selects and applies a set of design modification steps or rules that can eliminate these vulnerabilities. Such a rule-based obfuscation process has the distinctive capability to address all existing as well as emerging attacks through the learning of appropriate design transformation steps that prevent these attacks. We present an efficient strategy to apply these rules on a design, while resolving any conflict. Our evaluation of the LeGO framework on a set of ISCAS85 and open-source IP benchmarks has shown promising results in terms of robustness against diverse attacks with an average of area, power, and delay overhead of 39%, 45%, and 15%, respectively.

Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique which uses Bounded Model Checking for pre-silicon verification of HAs. A-QED checks an HA for self-consistency, i.e., whether identical inputs within a sequence of operations always produce the same output. Under modest assumptions, A-QED is both sound and complete. However, as is well-known, large design sizes significantly limit the scalability of formal verification, including A-QED. We overcome this scalability challenge through a new decomposition technique for A-QED, called A-QED with Decomposition (A-QED$^2$). A-QED$^2$ systematically decomposes an HA into smaller, functional sub-modules, called sub-accelerators, which are then verified independently using A-QED. We prove completeness of A-QED$^2$; in particular, if the full HA under verification contains a bug, then A-QED$^2$ ensures detection of that bug during A-QED verification of the corresponding sub-accelerators. Results on over 100 (buggy) versions of a wide variety of HAs with millions of logic gates demonstrate the effectiveness and practicality of A-QED$^2$.

Physically Unclonable Function (PUF) circuits are promising low-overhead hardware security primitives, but are often gravely susceptible to machine learning–based modeling attacks. Recently, chaotic PUF circuits have been proposed that show greater robustness to modeling attacks. However, they often suffer from unacceptable overhead, and their analog components are susceptible to low reliability. In this article, we propose the concept of a conditionally chaotic PUF that enhances the reliability of the analog components of a chaotic PUF circuit to a level at par with their digital counterparts. A conditionally chaotic PUF has two modes of operation: bistable and chaotic , and switching between these two modes is conveniently achieved by setting a mode-control bit (at a secret position) in an applied input challenge. We exemplify our PUF design framework for two different PUF variants—the CMOS Arbiter PUF and a previously proposed hybrid CMOS-memristor PUF, combined with a hardware realization of the Lorenz system as the chaotic component. Through detailed circuit simulation and modeling attack experiments, we demonstrate that the proposed PUF circuits are highly robust to modeling and cryptanalytic attacks, without degrading the reliability of the original PUF that was combined with the chaotic circuit, and incurs acceptable hardware footprint.

We present A-QED (Accelerator-Quick Error Detection), a new approach for pre-silicon formal verification of stand-alone hardware accelerators. A-QED relies on bounded model checking -- however, it does not require extensive design-specific properties or a full formal design specification. While A- QED is effective for both RTL and high-level synthesis (HLS) design flows, it integrates seamlessly with HLS flows. Our A-QED results on several hardware accelerator designs demonstrate its practicality and effectiveness: 1. A-QED detected all bugs detected by conventional verification flow. 2. A-QED detected bugs that escaped conventional verification flow. 3. A-QED improved verification productivity dramatically, by 30X, in one of our case studies (1 person-day using A-QED vs. 30 person-days using conventional verification flow). 4. A-QED produced short counterexamples for easy debug (37X shorter on average vs. conventional verification flow).

With the large-scale adaptation of a "horizontal" business model, modern semiconductor supply chain is plagued by recycled and counterfeit ICs, including flash memory chips. Since flash memory modules have an inherently finite lifespan, detection of recycled flash memory chips before their deployment in safety-critical systems is important to prevent disastrous consequences. The state-of-art detection methods can detect flash memory modules between 0.05% to 3.00% of their lifespan as minimum usage duration, depending on the details of the flash memory chip. In this paper, we propose a versatile machine learning assisted detection methodology to improve the minimum usage duration accuracy between 0.05% to 0.96% of their lifespan, and also to accurately associate a flash memory IC with its manufacturer. Through detailed experimentation and comparison of detection results obtained using three popular supervised machine learning techniques (Support Vector Machines, Logistic Regression and Artificial Neural Networks), we demonstrate that usage of features composed of multiple characteristics of a given chip, rather than just a single property of a chip (as used in previous works), improves detection accuracy.

Cyclic logic encryption currently constitutes the most robust technique against Boolean satisfiability (SAT) based attacks on logic encryption; however, recent "Cyclic SAT" (CycSAT) attacks have overcome this resistance to a large scale. In this paper we develop an improved version of cyclic logic encryption using a common permutation network (the "Beneš network"). The cyclic nature is implemented by channeling some of the keys of the permutation network through the permutation network itself, and feeding them back to the target nodes instead of direct connection. It is observed that although the standalone Beneš network is highly susceptible to SAT based attacks, the proposed architecture has the two properties required for it to be immune to SAT attack, namely oscillatory and stateful. We also show that the procedure of enumerating cycles without node duplicity ("simple cycles") during the preprocessing step of CycSAT attacks, as considered in some previous works, is not technically correct; instead, we should consider cycles without edge duplicity. We then prove that the number of cycles without edge duplicity in our proposed technique grows as Ω(n!(n – 1)!), where n is the number of feedback paths. The logic synthesis tool distributes the different stages of our proposed network across the obfuscated circuit, thereby making it immune to trivial netlist tracing based detection and removal attacks. The robustness of the technique to the CycSAT attack has been validated for ISCAS-85 benchmark circuits.