(Security) Assertions by Large Language Models
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911949756825600 |
|---|---|
| author | Kande, Rahul Pearce, Hammond Tan, Benjamin Dolan-Gavitt, Brendan Thakur, Shailja Karri, Ramesh Rajendran, Jeyavijayan |
| author_facet | Kande, Rahul Pearce, Hammond Tan, Benjamin Dolan-Gavitt, Brendan Thakur, Shailja Karri, Ramesh Rajendran, Jeyavijayan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_14027 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | (Security) Assertions by Large Language Models Kande, Rahul Pearce, Hammond Tan, Benjamin Dolan-Gavitt, Brendan Thakur, Shailja Karri, Ramesh Rajendran, Jeyavijayan Cryptography and Security Artificial Intelligence 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. |
| title | (Security) Assertions by Large Language Models |
| topic | Cryptography and Security Artificial Intelligence |
| url | https://arxiv.org/abs/2306.14027 |