PaperlayerView exact revision on arXiv

Source-linked AI summary

(Security) Assertions by Large Language Models

Rahul Kande, Hammond Pearce, Benjamin Tan, Brendan Dolan-Gavitt, Shailja Thakur, Ramesh Karri, Jeyavijayan Rajendran

arXiv:2306.14027v2cs.CRcs.AI

TL;DR

Writing security assertions is error-prone and difficult to scale, and natural-language descriptions of security properties are not automatically used to generate assertions. The authors evaluate an out-of-the-box LLM with a framework and benchmark suite, varying prompt context and comparing generated assertions with golden references. 93.55% accuracy was achieved by the best prompt configuration, compared with 26.54% average accuracy across 2,268 prompt configurations.

Abstract

from arXiv · show

The security of computer systems typically relies on a hardware root of trust. As vulnerabilities in hardware can have severe implications on a system, there is a need for techniques to support security verification activities. Assertion-based verification is a popular verification technique that involves capturing design intent in a set of assertions that can be used in formal verification or testing-based checking. However, writing security-centric assertions is a challenging task. In this work, we investigate the use of emerging large language models (LLMs) for code generation in hardware assertion generation for security, where primarily natural language prompts, such as those one would see as code comments in assertion files, are used to produce SystemVerilog assertions. We focus our attention on a popular LLM and characterize its ability to write assertions out of the box, given varying levels of detail in the prompt. We design an evaluation framework that generates a variety of prompts, and we create a benchmark suite comprising real-world hardware designs and corresponding golden reference assertions that we want to generate with the LLM.

I. INTRODUCTION

Hardware vulnerabilities can be difficult to fix after fabrication, while security assertions can support early vulnerability detection. The paper investigates out-of-the-box LLM generation of hardware security assertions and contributes an evaluation framework, benchmarks, and prompt studies.

A. Implications of Vulnerable Hardware

  • Hardware vulnerabilities discovered after fabrication cannot usually be fixed, and software patches can incur performance overheads.Field vulnerabilities can also cause information leakage or reputational damage.Source: A. Implications of Vulnerable Hardware · p. 1

B. State-Of-The-Art Hardware Verification

  • Hardware fuzzing and other verification techniques may rely on golden reference models or assertions, whose generation requires manual effort and design knowledge.Such generation is described as error-prone and difficult to scale.Source: B. State-Of-The-Art Hardware… · p. 1

C. Assertion-Checking

  • Assertions encode design properties for simulation, formal verification, or runtime checking and can detect vulnerabilities before a design is fully developed.They can also detect issues arising when components are composed and guide hardware fuzzers.Source: C. Assertion-Checking · p. 1

D. Limitations of Assertion-Checking

  • Security assertions are difficult to write because they require security expertise and design knowledge, making the work error-prone, time-consuming, and hard to scale.Mining can produce irrelevant or difficult checks, and security properties often require reasoning about the absence of weaknesses rather than expected functional behavior.Source: D. Limitations of Assertion-Checking · p. 1

E. Goals and Contributions

  • The paper investigates whether LLMs can generate security assertions from natural-language comments and surrounding design context, with the aim of making assertion-based security checking easier to adopt.The authors describe this as a route toward earlier vulnerability detection.Source: E. Goals and Contributions · p. 2
  • The authors contribute an evaluation framework and benchmark suite, studies of LLM assertion generation and prompt types, and an open-source release.The framework can fix a limited set of syntax and typographical issues.Source: E. Goals and Contributions · p. 2

A. Security Assertions

  • For BM1, a correct register-lock assertion must identify the security behavior, select the right signals, and check the lock value from the previous cycle when data changes.More complex assertions may involve more signals and parameter values, as in BM7.Source: A. Security Assertions · p. 2

B. Large Language Models for Code Generation

The paper considers LLMs that generate code from prompts and situates its work among automated assertion-generation approaches. It evaluates natural-language-to-SystemVerilog generation without training or closely related project assertions, using a benchmark suite with varied design context.

B. Large Language Models for Code Generation

C. Automating Assertion Generation

  • Unlike prior approaches, the paper maps natural-language designer intent to SystemVerilog security assertions without training, simulation, or assertions from closely related projects, and automatically evaluates their usefulness.Prior chatbot work manually checked correctness and was not security-specific.Source: C. Automating Assertion Generation · p. 3

III. EVALUATION FRAMEWORK: ASSESSING LLMS FOR ASSERTION GENERATION

  • The evaluation framework prompts an LLM to generate assertions, simulates them alongside golden references, and checks whether both trigger for the same input values.Its components are a benchmark suite, prompt generator, assertion-file generator, simulator, and scoreboard.Source: §III · p. 3

A. Benchmark Suite

  • The benchmark suite contains two manually crafted designs and eight modules derived from Hack@DAC competitions and OpenTitan, spanning hardware vulnerability categories.The categories include debug and test, interfaces and on-chip fabric, access control, and power, clock, thermal, and reset concerns.Source: A. Benchmark Suite · p. 3

1) Design source code:

  • For each benchmark, the source context is provided in three forms: no design information, bug-free design code, or code containing the vulnerability.The source files are trimmed and simplified to fewer than 100 lines while retaining logic relevant to the target vulnerability.Source: 1) Design source code · p. 3

2) Golden reference assertion:

The benchmarks pair target assertions with reference assertions and prompt data that vary the natural-language description, examples, and assertion beginnings. These variants let the evaluation examine how prompt detail and context relate to generated assertions.

2) Golden reference assertion:

  • Each benchmark has a reference SVA: BM1–BM8 use manually crafted assertions, while BM9 and BM10 reuse OpenTitan verification assertions.The benchmark table identifies each target assertion, vulnerability, and corresponding CWE classification.Source: 2) Golden reference assertion · p. 3, Table I · p. 4

3) Prompt data:

  • The prompt generator combines benchmark prompt data to produce prompts with varying detail for querying the LLM.The prompt data includes comment strings, example assertions, and beginnings of the target assertion.Source: 3) Prompt data · p. 4
  • Prompt comments range from very brief descriptions with generic signals and omitted timing to detailed descriptions specifying exact values and timing.BriefCom supplies correct signal names and values but omits timing; DetailedCom also replaces common terms with exact values and includes timing information.Source: 3) Prompt data · pp. 4–5
  • The prompt data includes example assertions ranging from none or an unrelated trivial assertion to simpler or similar target-like assertions.BasicEx is a simpler target-like SVA with different signal names and values; DetailedEx is similar to the target assertion but uses different signal names and values.Source: 3) Prompt data · p. 5
  • Assertion beginnings vary from an empty string to short or normal starting words, providing different amounts of target-assertion context.The short and normal beginnings contain one to three and three to eight starting words, respectively.Source: 3) Prompt data · p. 5

4) Testbench:

The framework uses a parameterized testbench to drive combinations of assertion inputs across clock cycles. A counter supplies signal values and holds them for the required number of cycles.

4) Testbench:

  • The testbench drives all signals involved in each assertion through all possible value combinations.The authors built the benchmark testbenches from a manually developed template.Source: 4) Testbench · p. 5
  • The template parameterizes the number of DUT signal bits and the base-2 logarithm of the clock cycles needed to verify an assertion.These parameters determine the counter width and its range.Source: 4) Testbench · p. 5
  • Counter bits drive the DUT signals, while the least-significant log2NoClocks bits keep those signal values unchanged for the required clock cycles.The counter increments from 0 through 2^CTR_WIDTH − 1.Source: 4) Testbench · p. 5

B. Prompt Generator

The prompt generator builds benchmark-specific prompts from templates, combining design code, module context, an assertion clue, and an assertion beginning. It varies examples, comments, and wording to create multiple prompt configurations.

B. Prompt Generator

  • Templates generate prompt strings, while the generator also selects LLM parameter values for each benchmark.The prompt generator automates prompt creation using templates.Source: B. Prompt Generator · pp. 5–6
  • Each prompt combines a design source, module context from the golden assertion file, an assertion clue, and an assertion beginning.The clue appends an example assertion and a comment string describing the target assertion.Source: B. Prompt Generator · p. 6
  • Prompts vary the wording between “assert that” and “property to check that” and use an assertion beginning to prime code completion.The example illustrates how the prompt combines the design source, module, assertion clue, and beginning string.Source: B. Prompt Generator · p. 6

C. Assertion File Generator

The assertion file generator applies a limited set of automatic syntax and typographical repairs, then substitutes processed assertions into files for simulation. The simulator produces violation traces for comparison against golden assertions.

C. Assertion File Generator

  • The generator applies a limited set of lexical fixes to common minor mistakes, preserving original assertions when repairs could affect performance.R1 and R4 are applied directly because leaving them unfixed causes compilation errors; R2 and R3 are applied to copies.Source: C. Assertion File Generator · p. 6
  • The framework’s automated fixes target syntax and typographical issues.Table II is identified as the list of fixes used by the framework.Source: C. Assertion File Generator · p. 6, Table II · p. 6

D. Simulator

  • The simulator runs generated assertion files with corresponding testbenches and records violation traces for processed and golden assertions.Table III is labeled as reporting assertions generated, compiled, simulated, and correct.Source: D. Simulator · pp. 6–7, Table III · p. 7

E. Scoreboard

The framework evaluates code-davinci-002 on hardware assertion benchmarks by comparing generated assertions with golden references and varying prompt configurations. Accuracy varies substantially across prompts, while detailed examples and comments perform best on average.

E. Scoreboard

  • The scoreboard marks a generated assertion correct when it triggers violations for the same input sets as the golden reference.It parses and compares violation data from simulation logs.Source: E. Scoreboard · p. 7

A. Study Overview

  • The study evaluates code-davinci-002 and uses code-cushman-001, codegen-2b-ft, and ChatGPT to demonstrate framework scalability.code-davinci-002 is identified as the primary model for the experiments.Source: A. Study Overview · p. 7

B. Evaluation Setup

  • Each benchmark yields 378 unique prompt strings and six parameter combinations per string, producing 2,268 queries per benchmark.The prompt strings combine comment, example, design-source, and assertion-beginning variants.Source: B. Evaluation Setup · pp. 7–8

C. RQ1: Can LLMs generate hardware assertions?

1) Example assertions and comment strings:

  • No-example prompts performed poorly across benchmarks, while short example-comment combinations had exceptions on BM3 and BM4.The authors suggest that absent context may leave the model unsure whether to generate an assertion or ordinary design code.Source: 1) Example assertions and comment… · pp. 8–9
  • Detailed examples with detailed comments led the accuracy pairs at 72.16%, 39.2%, and 24.62%, respectively, across benchmarks.The paper attributes detailed comments’ performance to specifying signal names and timing information.Source: 1) Example assertions and comment… · p. 9

2) Design source codes and comment strings:

The results show that detailed comment strings generally improve assertion generation, while synonym choices and assertion beginnings have limited impact overall. Assertion beginnings can still help when a property needs a construct such as SystemVerilog generate.

2) Design source codes and comment strings:

  • Comment strings provide assertion details more directly than design source code, where relevant information can be distributed across modules and mixed with other logic.The results also note that GoldenDUT and BuggyDUT can support correct assertions with BriefCom, though complex designs make information harder to infer from source code.Source: 2) Design source codes and comment… · p. 9
  • 48.79%, 45.59%, and 48.83% correct simulated assertions were achieved by (GoldenDUT, DetailedCom), (BuggyDUT, DetailedCom), and (EmptyDUT, DetailedCom), respectively.The authors attribute DetailedCom's performance to providing all information required for the target assertion.Source: 2) Design source codes and comment… · p. 9
  • GoldenDUT prompts averaged 48.79%, 19.69%, and 15.8% accuracy with DetailedCom, BriefCom, and VeryBriefCom, respectively.The results suggest that either the source code or comment should provide the benchmark-design and target-assertion information; detailed comments were more effective, while using design source code could reduce user input.Source: 2) Design source codes and comment… · p. 9

3) Synonym strings:

  • Excluding NoEx combinations, synonym combinations achieved 27%–30% accuracy, with little impact from synonym choice when a comment was included.NoEx combinations performed poorly; the authors attribute this to prompts without examples averaging under 2% correct assertions, rather than to the synonym used.Source: 3) Synonym strings · p. 10

4) Assertion beginnings:

  • NormalBeg, ShortBeg, and EmptyBeg achieved 27.51%, 27.17%, and 24.65% correct simulated assertions, respectively, performing similarly on most benchmarks.For BM4 and BM8, NormalBeg and ShortBeg provided the genvar hint needed for assertions requiring a generate construct.Source: 4) Assertion beginnings · p. 10
  • EmptyBeg was sufficient for most benchmarks, while a construct cue such as genvar improved performance for assertions requiring nontrivial constructs.NormalBeg performed best on average because of its results on BM4 and BM8.Source: 4) Assertion beginnings · p. 10

5) Temperature and frequency penalty values:

Results vary with benchmark and prompt configuration: detailed comments yield the strongest reported accuracy, while prompt components differ in importance. The evaluation also finds that performance varies across LLM engines and that generated assertions can contain compilation and logic errors.

5) Temperature and frequency penalty values:

  • For BM3, temp=0.9 yielded >75% correct assertions, but <25% for BM9, showing parameter performance varies by benchmark.At frequency penalty=1, temp=0.9 had 34.25% accuracy versus 25.32% for temp=0.4; lower temperatures often produced syntactically correct assertions with incorrect logical conditions.Source: 5) Temperature and frequency penalty… · p. 10
  • Frequency-penalty values differed by <5% in average accuracy at a given temperature, although BM7 ranged from 0.23% to 6.56% across settings.The reported takeaway is that frequency penalties of 0 or 0.5 were more likely than 1 to generate correct assertions in most cases.Source: 5) Temperature and frequency penalty… · p. 10

6) Best performing configurations:

  • 93.55% accuracy with DetailedCom, versus 26.54% across prompt configurations; BriefCom and VeryBriefCom reached 61.9% and 57.89%, while NoEx peaked at 50%.DetailedCom supplies detailed assertions in comments; NoEx configurations provide no example assertion.Source: Table IV · p. 11, 6) Best performing configurations · p. 11

7) Relative importance of prompt’s components:

  • Example-assertion and comment types strongly affect correctness, while design source, synonym strings, and assertion beginnings have nearly equal distributions.Temperature and frequency penalty generally had less impact, except on some benchmarks such as BM7.Source: 7) Relative importance of prompt’s… · p. 11
  • Among the last 427 configurations that failed to generate correct assertions, >90% used VeryBriefCom and <12% used DetailedEx.The remaining configuration types were nearly equally likely to occur in that group.Source: 7) Relative importance of prompt’s… · p. 11

E. Scalability To Other LLM Engines

  • With one most-contextual query, code-davinci-002 generated correct assertions for 9 of 10 benchmarks, versus 7 for code-cushman-001, 4 for codegen-2b-ft, and 5 for ChatGPT.The query used GoldenDUT, DetailedEx, DetailedCom, NormalBeg, temperature 0.4, and frequency penalty 0.Source: E. Scalability To Other LLM Engines · p. 11, Table V · p. 12

F. Other Observations

  • Multiple assertions in one response can provide essential checks, add redundant checks, or make an otherwise correct response incorrect.The authors note that a semicolon cannot be the stop sequence because it limits generation to one assertion.Source: F. Other Observations · p. 12
  • Most incorrect assertions have syntax, variable, or index errors; additional irrelevant logic can cause compilation errors, while incorrect logic or timing may still simulate.The authors could not provide an exhaustive error list, but describe the recurring errors as useful for improving future models.Source: F. Other Observations · p. 12

A. Completeness of Benchmark Suite

The benchmark suite contains ten realistic assertion benchmarks, but its reference assertions and prompt comments represent human-selected rather than exhaustive ways to express security intent. Generated errors span syntax, variable, indexing, logic, and timing problems.

A. Completeness of Benchmark Suite

  • The ten realistic benchmarks cover a range of properties, while broader CWE types and vulnerabilities remain for future exploration.The authors based most reference assertions on their assessment of example vulnerabilities and CWE types.Source: A. Completeness of Benchmark Suite · p. 13
  • Generated errors include invalid Verilog syntax, invalid variables, and incorrect variable indices.Examples include malformed temporal operators and incorrect signal or bit selections.Source: A. Completeness of Benchmark Suite · p. 13
  • Other generated errors add logic after an assertion, alter its condition, include unwanted logic, or use incorrect timing.The examples include an identity condition, an extra implication, and a two-cycle delay.Source: A. Completeness of Benchmark Suite · p. 13
  • The reference assertions are only one possible way to capture each security property, and the prompt comments cover only a small subset of possible expressions.Both choices were based on human judgment and could be explored further.Source: A. Completeness of Benchmark Suite · p. 13

B. Simulation Testbench

The evaluation uses exhaustive simulation against golden reference assertions, while the paper identifies practical scope boundaries for deploying its framework. With sufficient prompt context, code-davinci-002 reaches up to 93.55% accuracy across the benchmarks.

B. Simulation Testbench

  • Simulation testbenches exhaustively checked equivalence to golden references, reducing signal widths for scale and assuming triggering behavior holds across the width change.For example, 32-bit signals were treated as 2-bit signals; a generated assertion could still express security intent better than its reference and be marked incorrect by the mismatch criterion.Source: B. Simulation Testbench · p. 13
  • The testbench manually determined required clock-cycle coverage, and a 1,000-second timeout handled generated assertions that could cause simulation to hang.All reference assertions ran in under 100 seconds; timed-out assertions were marked correct when their functional behavior matched the reference.Source: B. Simulation Testbench · p. 13

C. Use-cases of our Framework

  • Using the framework as-is in production requires security expertise, and selecting relevant module signals and prompt context remains open.The authors suggest invariant mining as one possible aid.Source: C. Use-cases of our Framework · p. 13
  • The work focuses on concurrent assertions in separate SVA files, leaving immediate assertions embedded in hardware designs for future work.When golden references are absent, generated assertions could be formally proven or checked through regression testing, with violations requiring manual analysis.Source: C. Use-cases of our Framework · p. 14

D. Future Work

  • Table VI summarizes follow-on research using LLMs or extracting security properties that appeared after this work's arXiv release.The paper presents the table as a snapshot of the emerging research area.Source: D. Future Work · p. 14, Table VI · p. 14

VI. CONCLUSION

  • 93.55% accuracy across all benchmarks was achieved by code-davinci-002 given sufficient prompt context.The authors also report 26.54% average accuracy across 2,268 prompts with varying context.Source: §VI · p. 14

APPENDIX

The appendix figures report accuracy across prompt variations, including wording, examples, design context, and sampling settings; the supplied captions do not state which variations perform best.

A. ACCURACY OF DIFFERENT PROMPTS

  • Figure 9 examines accuracy across synonym-string combinations, while Figure 10 varies assertion-beginning strings.The captions identify the prompt components compared, but give no outcome values.Source: Figure 9 · p. 15, Figure 10 · p. 15
  • Figure 11 varies example assertions with comment strings, and Figure 12 varies design source code with comment strings.The captions do not report a winning combination.Source: Figure 11 · p. 16, Figure 12 · p. 16
  • Figure 13 compares accuracy across temperature and frequency-penalty combinations.The corresponding performance results are discussed in Section IV-D.Source: Figure 13 · p. 16, A. ACCURACY OF DIFFERENT PROMPTS · p. 16
Loading 2306.14027v2…