An official website of the United States government
Hardware security verification in hardware design has been identified as a significant bottleneck due to complexity and time-to-market constraints. Assertion-Based Verification is a recognized solution to this challenge; however, assertion generation relies on expertise and labor. While LLMs show promise as automated tools, existing approaches often rely on complex prompt engineering, requiring expert validation. The challenge lies in identifying effective methods for constructing training datasets that enhance LLMs' hardware performance. We introduce HADA (Hardware Assertion through Data Augmentation), a novel framework to train hardware debug specific expert LLM by leveraging its ability to integrate knowledge from formal verification tools, hardware security knowledge database, and version control system. Our results demonstrate that integrating multi-source data significantly enhances the effectiveness of hardware security verification, with each addressing the limitations of the others.
more »
« less
This content will become publicly available on July 1, 2026
Application of A Verification Complexity Framework
Abstract Complexity is a core characteristic of concern for systems engineering practice. Verification, while a pervasive process in the engineering of systems, has been given relatively less research focus in terms of its complexity than system complexity has. We have proposed the Verification Complexity Framework as a formal definition of verification complexity to initiate a dialogue on distinguishing verification complexity from system complexity. The framework is designed to cover both static and dynamic complexity through the time axis and the hierarchical complexity layers, covering from external effects to the verification structures. This framework provides a common vocabulary for verification complexity, where both its definition and measurements can be discussed. In this paper, we showcase the application of VCF to a notional project.
more »
« less
- Award ID(s):
- 2205468
- PAR ID:
- 10653086
- Publisher / Repository:
- Wiley
- Date Published:
- Journal Name:
- INCOSE International Symposium
- Volume:
- 35
- Issue:
- 1
- ISSN:
- 2334-5837
- Page Range / eLocation ID:
- 297 to 309
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Knox is a new framework that enables developers to build hardware security modules (HSMs) with high assurance through formal verification. The goal is to rule out all hardware bugs, software bugs, and timing side channels. Knox's approach is to relate an implementation's wire-level behavior to a functional specification stated in terms of method calls and return values with a new definition called information-preserving refinement (IPR). This definition captures the notion that the HSM implements its functional specification, and that it leaks no additional information through its wire-level behavior. The Knox framework provides support for writing specifications, importing HSM implementations written in Verilog and C code, and proving IPR using a combination of lightweight annotations and interactive proofs. To evaluate the IPR definition and the Knox framework, we verified three simple HSMs, including an RFC 6238-compliant TOTP token. The TOTP token is written in 2950 lines of Verilog and 360 lines of C and assembly. Its behavior is captured in a succinct specification: aside from the definition of the TOTP algorithm, the spec is only 10 lines of code. In all three case studies, verification covers entire hardware and software stacks and rules out hardware/software bugs and timing side channels.more » « less
-
null (Ed.)In systems engineering, verification activities evaluate the extent to which a system under development satisfies its requirements. In large systems engineering projects, multiple firms are involved in the system development, and hence verification activities must be coordinated. Self-interest impedes the implementation of verification strategies that are beneficial for all firms while encouraging each firm to choose a verification strategy beneficial to itself. Incentives for verification activities can motivate a single firm to adopt verification strategies beneficial to all firms in the project, but these incentives must be offered judiciously to minimize unnecessary expenditures and prevent the abuse of goodwill. In this paper, we use game theory to model a contractor-subcontractor scenario, in which the subcontractor provides a component to the contractor, who further integrates it into their system. Our model uses belief distributions to capture each firm’s epistemic uncertainty in their component’s state prior to verification, and we use multiscale decision theory to model interdependencies between the contractor and subcontractor’s design. We propose an incentive mechanism that aligns the verification strategies of the two firms and using our game-theoretic model, we identify those scenarios where the contractor benefits from incentivizing the subcontractor’s verification activities.more » « less
-
Synopsis Examples of behavioral strategizing exist throughout the animal kingdom, but the quantification and analysis of these complex behavioral patterns remain a challenge. Classic research in this realm often relies either on methods that intentionally simplify complexity or that focus on a subset of abundant behaviors. Unfortunately, these approaches can sometimes eliminate informative details of behavioral strategizing. Here, we demonstrate the utility of a systems-based approach to characterize behavioral patterns in a way that captures the complexity of behavioral strategies and tactics while supporting the generation of relevant, system-specific hypotheses. We accomplish this aim by building upon classic ideas of strategy and tactic, refocusing the theory on behavioral traits, and extending the framework to make sense of patterns of behavior use. In doing so, we outline a more expansive definition of the behavioral tactic, and we provide a methodological roadmap for quantifying multi-behavior and multi-agent tactics. Our goal is to craft a framework for the study of behavioral patterns and encourage researchers to embrace the complexity in their systems. To this end, we provide a case study of territoriality in downy woodpeckers as proof of concept for a network-based systems approach to understanding behavioral strategies.more » « less
-
System modeling language (SysML) diagrams generated manually by system modelers can sometimes be prone to errors, which are time-consuming and introduce subjectivity. Natural language processing (NLP) techniques and tools to create SysML diagrams can aid in improving software and systems design processes. Though NLP effectively extracts and analyzes raw text data, such as text-based requirement documents, to assist in design specification, natural language, inherent complexity, and variability pose challenges in accurately interpreting the data. In this paper, we explore the integration of NLP with SysML to automate the generation of system models from input textual requirements. We propose a model generation framework leveraging Python and the spaCy NLP library to process text input and generate class/block definition diagrams using PlantUML for visual representation. The intent of this framework is to aid in reducing the manual effort in creating SysML v1.6 diagrams—class/block definition diagrams in this case. We evaluate the effectiveness of the framework using precision and recall measures. The contribution of this paper to the systems modeling domain is two-fold. First, a review and analysis of natural language processing techniques for the automated generation of SysML diagrams are provided. Second, a framework to automatically extract textual relationships tailored for generating a class diagram/block diagram that contains the classes/blocks, their relationships, methods, and attributes is presented.more » « less
