Multi-property formal verification remains a significant challenge in the chip design industry. With hundreds of property goals to verify in a design, several questions arise regarding goal ordering and grouping of properties, sharing of information across proven properties, and other heuristics to improve the verification productivity. This paper introduces SISCO, a novel method for addressing multi-property verification in complex designs. SISCO unfolds properties to a certain depth, clusters them, reorders properties within each cluster, and then uses a modified version of IC3/Property Directed Reachability (PDR) algorithm for efficient verification. The method stores the invariants of proven properties and selectively shares them while solving undecided goals. Additionally, SISCO keeps track of counter-example traces of falsified goals to assist verification. Experimental results demonstrate that clustering and ordering help solve more goals while selective invariant sharing accelerates the process. SISCO achieves a significant average improvement of 4.73× in the runtime of individual goals compared to all invariant sharing.

Adversarial attacks pose severe threats to the integrity of deep neural networks (DNNs), especially in resource-constrained systems where traditional defenses are computationally expensive. While existing defenses in the black-box setting utilize hardware characteristics of adversarial attacks (like Hardware Performance Counter or HPC measurements), these defenses often involve repeating execution of multiple target model inferences to detect the attacks.In this work, we put forth a differing perspective: while detection strategies involving multiple target model inferences appear to be successful in isolation, they have unacceptable and inhibitory requirements. Precisely, we argue that these works require cleaning the micro-architectural state of hardware like the cache and the branch predictor after each inference. This in turn leads to performance degradation of not only the adversarial attack detector, but also of the overall system at large.In this work, we put forth a novel and lightweight detection strategy, MIRAGE, using HPCs that does not require cleaning the micro-architectural state of caches or branch predictors. We train a convolutional neural network (CNN) on these signals to classify inputs as benign or adversarial in a single shot, making our approach practical for online systems, while allowing full use of hardware optimizations for performance uplifts. Experiments on CIFAR-10 and MNIST datasets reveal that our methodology not only detects adversarial samples effectively with greater than 96% accuracy, but also imposes a minimal timing overhead of 60 ms and maintains high throughput. This makes our solution well-suited for embedded and edge-AI scenarios.

Besides enormous research efforts in the design of Physically Unclonable Functions (PUFs), its vulnerabilities are still being exploited using machine learning (ML) based model-building attacks. Due to inherent complicacy in exploring and manually converging to a strong PUF composition, the challenge of building ML-attack resistant PUFs continues. Hence, it becomes imperative to develop an automated framework that can formally assess the learnability of different PUF constructions and compositions to guide the designer to explore resilient PUFs. In this work, we present an automated analysis framework (PARLE-G), to formally represent and evaluate the Probably Approximately Correct (PAC) learnability of PUF constructions and their compositions. A high-level specification language PUF-G has been developed to structurally represent any PUF composition comprising a specified set of primitive components and composition operations. The tool takes a PUF design represented in PUF-G language as input and returns its PAC learnability result, identifying a suitable PAC learning algorithm and the PAC model parameters based on the input PUF design. PUF designs proven to be learnable by PARLE-G are segregated into different classes based on the asymptotic complexity of their learnability bounds. Such automated analysis helps a designer to make informed design choices, thereby strengthening a PUF construction from the architectural level.

Multi-property verification has emerged as a con-temporary challenge in the chip design industry. With designs now encompassing hundreds of properties, conventional sequential verification without information sharing is no longer preferred. Past attempts towards grouping or ordering properties based on cone-of-influence (COI) are typically ineffective for complex designs. This paper introduces PURSE, a novel approach that addresses this challenge by dynamically reordering properties for sequential and incremental solving. By identifying and prioritizing simpler properties, the process accelerates convergence. This article presents two dynamic reordering techniques guided by statistical data gathered from the IC3/Property Directed Reachability (PDR) proof engine. The study compares dynamic ordering strategies against static ordering and a default ordering based on design structure. Empirical results from various industrial designs demonstrate that our proposed methodology performs better in most cases, with up to 25% improvements in convergence.

Physically Unclonable Functions (PUFs) with large challenge space (also called Strong PUFs) are promoted for usage in authentications and various other cryptographic and security applications. In order to qualify for these cryptographic applications, the Boolean functions realized by PUFs need to possess a high nonlinearity (NL). However, with a large challenge space (usually$\geq 64$bits), measuring NL by classical techniques like the Walsh transformation is computationally infeasible. In this paper, we propose the usage of a heuristic-based measure called the non-homomorphicity test which estimates the cryptographic NL of Boolean functions with high accuracy in spite of not needing access to the entire challenge-response set. We also combine our analysis with a technique used in linear cryptanalysis, called Piling-up lemma, to measure the NL of popular PUF compositions. As a demonstration to justify the soundness of the metric, we perform extensive experimentation by first estimating the NL of constituent Arbiter/Bistable Ring PUFs using the non-homomorphicity test, and then applying them to quantify the same for their XOR compositions namely XOR Arbiter PUFs and XOR Bistable Ring PUF. Our findings show that the metric explains the impact of various parameter choices of these PUF compositions on the NL obtained and thus promises to be used as an important objective criterion for future efforts to evaluate PUF designs. While the framework is not representative of the machine learning robustness of PUFs, it can be a useful complementary tool to analyze the cryptanalytic strengths of PUF primitives.

Integrated circuit designs are evaluated at various corners defined by choices of the design and process parameters. Considering the large number of corners and the simulation cost of covering all the corners of a large design, it is desirable to identify a subset of the corners that can potentially expose corner case bugs. In an integrated analog coverage management framework, this choice may be influenced by those corners that take one or more component analog IPs close to their individual specification boundaries. Since the admissible state space of an analog IP is multi-dimensional, the same corner may not reach the extreme behaviors for each attribute of the specification, and one needs to identify a subset that covers the extremality. This paper shows that the underlying problem is NP-hard and presents an automated methodology for selecting the corners. A formal analog coverage specification is leveraged by our algorithm, which uses a Satisfiability Modulo Theory (SMT) solver to identify the appropriate corners from the output of multiple Monte Carlo (MC) simulations. The efficacy of the proposed approach is demonstrated over industrial test cases.

With increasing design complexity, the portability of tests across different designs and platforms becomes a key criterion for accelerating verification closure. The Portable Test and Stimulus Standard (PSS) is an emerging industry standard prepared by Accellera for system-on-chip verification and testing. It provides language constructs to create a target-agnostic representation of stimulus and test scenarios reused by various users across many levels of integration. In this article, we present CoVerPlan , a comprehensive verification framework built to explore the power of action inferencing on test models written in PSS. The proposed verification framework leverages a Boolean satisfiability problem planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random testbenches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties. We demonstrate the efficacy of our proposed framework over several case studies, like the Advanced Microcontroller Bus Architecture advanced peripheral bus protocol, a simple Reduced Instruction Set Computer processor, and a cache coherence protocol.

Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs.

This paper initiates the study of “Cryptophasia in Hardware” – a phenomenon that allows hardware circuits/devices with no pre-established secret keys to securely exchange secret information over insecure communication networks. The study of cryptophasia is motivated by the need to establish secure communication channels between lightweight resource-constrained devices incapable of securely storing cryptographic keys and/or executing resource-intensive cryptographic protocols. In this paper, we introduce a novel concept calledPhysically Related Functions(PReFs) that can exchange secret information in a secure and authenticated manner over insecure networks. This function can be visualized as an abstraction of Strong Physically Unclonable Functions (PUFs). Strong PUFs have the limitation in communicating between two identical devices, an issue that we address in the definition of PReFs. We describe a formal framework for analyzing the functional and security requirements of PReFs. In this framework, we present a lightweight (in terms of computation cost) yet provably secure authenticated key-exchange protocol that relies only on PReFs and makes no additional assumptions (such as secure storage of cryptographic keys). Finally, we present a proof-of-concept realization of PReFs in hardware over Digilent Cora Z7 – a low-cost development platform (consisting of an ARM Cortex processor and a Xilinx FPGA) that is particularly suitable for real-world IoT applications involving resource-constrained devices. We validate that our realization of PReFs satisfies all the properties warranted by our formal framework. We further demonstrate the efficacy of our proposed protocol by analyzing its performance (in terms of computational and communication latency) over the Digilent Cora Z7 platform.

The S-PUF and Sn-PUF designs (proposed in IN-DOCRYPT2019) are one of the contemporary composite strong PUF candidates of the Delay-PUF family that exhibit two distinguishing and notable attributes – (i) it is one of the few PUF constructions which is guided by theoretical analysis of the Strict Avalanche Criteria (SAC) property and not by ad-hoc choices; and (ii) though its construction is quite similar to XOR PUFs, it has very good reliability property unlike the former design due to the introduction of Maiorana-McFarland (M-M) Bent Function. These make Sn-PUF to be a very good candidate for strong PUF proposals and an interesting target from the point of view of attackers. In this work, we testify that a novel reliability based machine learning attack can be launched in this architecture against the original authors’ claim. Though it is challenging to launch a classical or reliability based ML attack directly, we leverage the bias introduced by the AND operation in the M-M bent function due to its non-linearity property. Our proposed novel attack framework, SACReD, is able to break $S_{8}, S_{10}$ and $S_{12}-$PUF designs, which were originally assumed to be secure, by taking only 400K Challenge-Response Pairs.

In this research work, we aim to formalize the analysis of Physically Unclonable Functions (PUF) constructions. First, we present a testability analysis scheme that leverages the correlation spectra properties of Boolean functions to assess the quality of a collection of PUF instances of the same make by comparing its correlation spectra with that of a collection of known good PUF instances. Further, in the research, we propose a CAD framework that automatically assesses the learnability of a PUF construction in the PAC Learning model. To represent a PUF design, we propose a formal PUF representation language capable of representing any PUF construction or composition upfront. Next, we present a non-linearity assisted reliability based ML attack on a contemporary PUF construction, named Sn-PUF. We leverage the non-linearity of the Bent function to launch a reliability-based ML attack, that is able to break upto S12-PUF.

Fault attacks belong to a potent class of implementation-based attacks that can compromise a crypto-device within a few milliseconds. Out of the large numbers of faults that can occur in the device, only a very few are exploitable in terms of leaking the secret key. Ignorance of this fact has resulted in countermeasures that have either significant overhead or inadequate protection. This article presents a framework, referred to as FaultDroid, for automated vulnerability analysis of fault attacks. It explores the entire fault attack space, identifies the single/multiple fault scenarios that can be exploited by a differential fault attack, rank-orders them in terms of criticality, and provides design guidance to mitigate the vulnerabilities at low cost. The framework enables a designer to automatically evaluate the fault attack vulnerabilities of a block cipher implementation and then incorporate efficient countermeasures. FaultDroid uses a formal model of fault attacks on a high-level specification of a block cipher and hence is equally applicable to both software and hardware implementation of the cipher. As case studies, we employ FaultDroid to comprehensively evaluate the fault scenarios in several common ciphers—AES, CLEFIA, CAMELLIA, SMS4, SIMON, PRESENT, and GIFT—and assess their vulnerability.

Coverage monitoring is fundamental to design verification. Coverage artifacts are well developed for digital integrated circuits and these aim to cover the discrete state space and logical behaviors of the design. Analog designers are similarly concerned with the operating regions of the design and its response to an infinite and dense input space. Analog variables can influence each other in far more complex ways as compared to digital variables, consequently, the notion of cross coverage, as introduced in the analog context for the first time in this paper, is of high importance in analog design verification. This paper presents the formal syntax and semantics of analog cross coverage artifacts, the methods for evaluating them using our tool kit, and most importantly, the insights that can be gained from such cross coverage analysis.

Fault attacks are potent physical attacks on crypto-devices. A single fault injected during encryption can reveal the cipher's secret key. In a hardware realization of an encryption algorithm, only a tiny fraction of the gates is exploitable by such an attack. Finding these vulnerable gates has been a manual and tedious task requiring considerable expertise. In this paper, we propose SOLOMON, the first automatic fault attack vulnerability detection framework for hardware designs. Given a cipher implementation, either at RTL or gate-level, SOLOMON uses formal methods to map vulnerable regions in the cipher algorithm to specific locations in the hardware thus enabling targeted countermeasures to be deployed with much lesser overheads. We demonstrate the efficacy of the SOLOMON framework using three ciphers: AES, CLEFIA, and Simon.

Physically Unclonable Functions (PUFs) are widely adopted in various lightweight authenticating devices due to their unique fingerprints - providing uniform, unpredictable and reliable nature of responses. However, with the growth of machine learning (ML) attacks in recent times, it is imperative that the PUFs need to be resilient to such modeling attacks as well. Consequently, analyzing the learnability of PUFs has initiated a new branch of study leading to establishing provable guarantees (and PAC-learnability) of various PUF designs. However, these derivations are often carried out manually while implementing the design and thereby cannot automatically adjust the changes in PUF designs or its various compositions. In this paper, for the first time, we present an automated framework, called PUF-G, to reason about the PAC-learnability of PUF designs from an architectural level. To enable this, we propose a formal PUF representation language by which any architectural PUF design and its compositions can be specified upfront. This PUF specification can be automatically analyzed through a CAD framework by translating the same to an interim model and then deriving the PAC-learnability bounds from the model. Such a tool will help the designer to explore various compositional architectures of PUFs and its resilience to ML attacks automatically before converging on a strong PUF design for implementation. We also show the efficacy of our proposed framework over a wide range of PUF architectures while automatically deriving their learnability guarantees. As a matter of independent interest, the framework presents the first reported proofs to show that Interpose-PUF (newly proposed), MUX-PUF, FF-APUF, FF-XOR APUF and DA-PUF, are all PAC-learnable.

Most cipher implementations are vulnerable to a class of cryptanalytic attacks known as fault injection attacks. To reveal the secret key, these attacks make use of faults induced at specific locations during the execution of the cipher. Countermeasures for fault injection attacks require these vulnerable locations in the implementation to be first identified and then protected. However, both these steps are difficult and error-prone and, hence, it requires considerable expertise to design efficient countermeasures. Incorrect or insufficient application of the countermeasures would cause the implementation to remain vulnerable, while inefficient application of the countermeasures could lead to significant performance penalties to achieve the desired fault-attack resistance. In this paper, we present a novel framework called SAFARI for automatically synthesizing fault-attack resistant implementations of block ciphers. The framework takes as input the security requirements and a high-level specification of the block cipher. It automatically detects the vulnerable locations from the specification, applies an appropriate countermeasure based on the user-specified security requirements, and then synthesizes an efficient, fault-attack protected, RTL, or C code for the cipher. We take AES, CAMELLIA, and CLEFIA as case studies and demonstrate how the framework would explore different countermeasures, based on the vulnerability of the locations, the output format, and the required security margins. We then evaluate the efficacy of SAFARI in hardware and software to the design overhead incurred and the fault coverage.

Mixed-signal components, such as low dropouts (LDOs) and phase locked loops (PLLs), are widely used inside the on-chip power management fabric of low power integrated system-on-chip (SoC) designs. The digital brain of the power management logic that is responsible for regulating the power delivery to different power domains in the chip has to consider the real time latencies of the analog components, which otherwise leads to functional errors in the domains being driven. The latencies may be viewed as contracts between the digital and the analog. This article presents an approach for generating assertions for protecting such mixed-signal latency contracts and using them to rule out timing bugs in the power management logic. Our tool flow enables the verification of the power management fabric, combining a novel mixed-signal assertion checking method in a simulation setting, and a full formal verification method for the digital brain of the power management logic. To the best of our knowledge, this is the first framework where assertions are used for binding analog latency contracts on the digital logic of power management.

The weakest link in cryptosystems is quite often due to the implementation rather than the mathematical underpinnings. A vast majority of attacks in the recent past have targeted programming flaws and bugs to break security systems. Due to the complexity, empirically verifying such systems is practically impossible, while manual verification as well as testing do not provide adequate guarantees. In this article, we leverage model checking techniques to prove the functional correctness of an elliptic curve cryptography (ECC) library with respect to its formal specification. We demonstrate how the huge state space of the C library can be aptly verified using a hierarchical assume-guarantee verification strategy. To test the scalability of this approach, we verify the correctness of five NIST-specified elliptic curve implementations. We also verify the newer curve25519 elliptic curve, which is finding multiple applications, due to its higher security and simpler implementation. The 192-bit NIST elliptic curve took 1 day to verify. This was the smallest curve we verified. The largest curve with a 521-bit prime field took 26 days to verify. Curve25519 took 1.5 days to verify.

Fault attacks recover secret keys by exploiting faults injected during the execution of a block cipher. However, not all faults are exploitable and every exploitable fault is associated with an offline complexity to determine the key. The ideal fault attack would recover maximum key bits with minimum offline effort. Finding the ideal fault attack for a block cipher is a laborious manual task, which can take several months to years before such an attack is discovered.

With the growing complexity and gradually shrinking power requirements in the system-on-chip designs, sophisticated global power management policies (which orchestrate the switching between power states of multiple power domains) are commonplace. Recent research has paved some novel ways to verify the sophisticated on-chip architectural power management decisions and analyze the verification coverage. However, one of the primary challenges in verifying such power management architectures stems from the mixed implementation of such strategies, where the local power controllers are in hardware and the global power management is implemented in software/firmware. There has been lack of effort to build a unified and automated framework for power intent verification and coverage analysis for generic power management logics. This paper tries to develop an end-to-end automated framework enabled by a tool named POWER-TRUCTOR for power intent validation.

This paper presents a verification framework that attempts to bridge the disconnect between high-level properties capturing the architectural power management strategy and the implementation of the power management control logic using low-level per-domain control signals. The novelty of the proposed framework is in demonstrating that the architectural power intent properties developed using high-level artifacts can be automatically translated into properties over low-level control sequences gleaned from UPF specifications of power domains, and that the resulting properties can be used to formally verify the global on-chip power management logic. The proposed translation uses a considerable amount of domain knowledge and is also not purely syntactic, because it requires formal extraction of timing information for the low-level control sequences. We present a tool, called POWER-TRUCTOR which enables the proposed framework, and several test cases of significant complexity to demonstrate the feasibility of the proposed framework.

The architectural power intent of a design defines the intended global power states of a power-managed integrated circuit. Verification of the implementation of power management logic involves the task of checking whether only the intended power states are reached. Typically, the number of global power states reachable by the global power management strategy is significantly lesser than the possible number of global power states. In this paper, we present a formal method for determining the set of reachable global power states in a power-managed design. Our approach demonstrates how this task can be further constrained as required by the verification engineer. We highlight the efficacy of the proposed methods over several test-cases.

Recent research has indicated ways of using UPF specifications for extracting valid low-level control sequences to express the transitions between the power states of individual domains. Today there is a disconnect between the high-level architectural power management strategy which relates multiple power domains and these low-level assertions for controlling individual power domains. In this paper we attempt to bridge this disconnect by leveraging the low-level per-domain assertions for translating architectural power intent properties into global assertions over low-level signals. We show that the inter-domain properties created in this manner can be formally verified over the global power management logic.