Modern hardware designs have grown increasingly efficient and complex.
However, they are often susceptible to Common Weakness Enumerations (CWEs).
This paper is focused on the formal verification of CWEs in a dataset of
hardware designs written in SystemVerilog from Regenerative Artificial
Intelligence (AI) powered by Large Language Models (LLMs). We applied formal
verification to categorize each hardware design as vulnerable or CWE-free. This
dataset was generated by 4 different LLMs and features a unique set of designs
for each of the 10 CWEs we target in our paper. We have associated the
identified vulnerabilities with CWE numbers for a dataset of 60,000 generated
SystemVerilog Register Transfer Level (RTL) code. It was also found that most
LLMs are not aware of any hardware CWEs; hence they are usually not considered
when generating the hardware code. Our study reveals that approximately 60% of
the hardware designs generated by LLMs are prone to CWEs, posing potential
safety and security risks. The dataset could be ideal for training LLMs and
Machine Learning (ML) algorithms to abstain from generating CWE-prone hardware
designs.

该研究针对以大型语言模型（LLMs）为动力的再生人工智能（AI）中，用 SystemVerilog 编写的硬件设计的 CWE 进行了形式验证。研究发现，大多数 LLMs 在生成硬件代码时并不知道任何硬件 CWE，因此未考虑其安全风险。该研究揭示了由 LLMs 生成的硬件设计约 60% 存在 CWE 风险，并提供了一个数据集，可用于训练 LLMs 和机器学习算法避免生成 CWE 风险的硬件设计。

所有人工，更少智能：形式验证透视下的 GenAI

All Artificial, Less Intelligence: GenAI through the Lens of Formal  Verification

Weaknesses in computer systems such as faults, bugs and errors in the
architecture, design or implementation of software provide vulnerabilities that
can be exploited by attackers to compromise the security of a system. Common
Weakness Enumerations (CWE) are a hierarchically designed dictionary of
software weaknesses that provide a means to understand software flaws,
potential impact of their exploitation, and means to mitigate these flaws.
Common Vulnerabilities and Exposures (CVE) are brief low-level descriptions
that uniquely identify vulnerabilities in a specific product or protocol.
Classifying or mapping of CVEs to CWEs provides a means to understand the
impact and mitigate the vulnerabilities. Since manual mapping of CVEs is not a
viable option, automated approaches are desirable but challenging.
We present a novel Transformer-based learning framework (V2W-BERT) in this
paper. By using ideas from natural language processing, link prediction and
transfer learning, our method outperforms previous approaches not only for CWE
instances with abundant data to train, but also rare CWE classes with little or
no data to train. Our approach also shows significant improvements in using
historical data to predict links for future instances of CVEs, and therefore,
provides a viable approach for practical applications. Using data from MITRE
and National Vulnerability Database, we achieve up to 97% prediction accuracy
for randomly partitioned data and up to 94% prediction accuracy in temporally
partitioned data. We believe that our work will influence the design of better
methods and training models, as well as applications to solve increasingly
harder problems in cybersecurity.

本文介绍了一种基于 Transformer 学习框架的新方法 (V2W-BERT)，通过自然语言处理、链接预测和迁移学习等思想，自动将 Common Vulnerabilities and Exposures (CVE) 映射到 Common Weakness Enumerations (CWE)，准确地解决了在网络安全方面的问题，可应用于寻找软件漏洞和缓解网络攻击。