論文の概要: The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
- arxiv url: http://arxiv.org/abs/2307.02192v3
- Date: Thu, 28 Mar 2024 07:52:02 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-29 22:02:51.236612
- Title: The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification
- Title(参考訳): FormAIデータセット: 形式検証のレンズによるソフトウェアセキュリティにおける生成AI
- Authors: Norbert Tihanyi, Tamas Bisztray, Ridhi Jain, Mohamed Amine Ferrag, Lucas C. Cordeiro, Vasileios Mavroeidis,
- Abstract要約: 本稿では,脆弱性分類を伴う112,000のAI生成Cプログラムの大規模なコレクションであるFormAIデータセットを提案する。
すべてのプログラムには、型、行番号、脆弱な関数名を示すソースコード内の脆弱性がラベル付けされている。
ソースコードは112,000のプログラムで利用でき、各プログラムで検出された脆弱性を含む別のファイルが付属する。
- 参考スコア(独自算出の注目度): 3.2925005312612323
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper presents the FormAI dataset, a large collection of 112, 000 AI-generated compilable and independent C programs with vulnerability classification. We introduce a dynamic zero-shot prompting technique constructed to spawn diverse programs utilizing Large Language Models (LLMs). The dataset is generated by GPT-3.5-turbo and comprises programs with varying levels of complexity. Some programs handle complicated tasks like network management, table games, or encryption, while others deal with simpler tasks like string manipulation. Every program is labeled with the vulnerabilities found within the source code, indicating the type, line number, and vulnerable function name. This is accomplished by employing a formal verification method using the Efficient SMT-based Bounded Model Checker (ESBMC), which uses model checking, abstract interpretation, constraint programming, and satisfiability modulo theories to reason over safety/security properties in programs. This approach definitively detects vulnerabilities and offers a formal model known as a counterexample, thus eliminating the possibility of generating false positive reports. We have associated the identified vulnerabilities with Common Weakness Enumeration (CWE) numbers. We make the source code available for the 112, 000 programs, accompanied by a separate file containing the vulnerabilities detected in each program, making the dataset ideal for training LLMs and machine learning algorithms. Our study unveiled that according to ESBMC, 51.24% of the programs generated by GPT-3.5 contained vulnerabilities, thereby presenting considerable risks to software safety and security.
- Abstract(参考訳): 本稿では、脆弱性分類付き112,000のAI生成可能な独立したCプログラムの大規模なコレクションであるFormAIデータセットを提案する。
本稿では,Large Language Models (LLM) を利用した多様なプログラムを生成するために構築された動的ゼロショットプロンプト技術を紹介する。
データセットはGPT-3.5-turboによって生成され、様々なレベルの複雑さを持つプログラムから構成される。
ネットワーク管理やテーブルゲーム、暗号化といった複雑なタスクを扱うプログラムもあれば、文字列操作のような単純なタスクを扱うプログラムもある。
すべてのプログラムには、型、行番号、脆弱な関数名を示すソースコード内の脆弱性がラベル付けされている。
この手法は, モデルチェック, 抽象解釈, 制約プログラミング, 満足度モジュロ理論を用いて, プログラムの安全性・セキュリティ特性を推論する, 効率的なSMTベース境界モデルチェッカー (ESBMC) を用いた形式的検証手法を用いて実現されている。
このアプローチは、脆弱性を確定的に検出し、反例として知られる形式的なモデルを提供し、偽陽性のレポートを生成する可能性を排除している。
特定された脆弱性を、CWE(Common Weakness Enumeration)番号に関連付けました。
我々は112,000のプログラムでソースコードを公開し、各プログラムで検出された脆弱性を含む別のファイルとともに、データセットをLLMと機械学習アルゴリズムのトレーニングに最適にする。
ESBMCによると、GPT-3.5で生成されたプログラムの51.24%が脆弱性を含んでおり、ソフトウェア安全性とセキュリティにかなりのリスクが生じる。
関連論文リスト
- HexaCoder: Secure Code Generation via Oracle-Guided Synthetic Training Data [60.75578581719921]
大規模言語モデル(LLM)は、自動コード生成に大きな可能性を示している。
最近の研究は、多くのLLM生成コードが深刻なセキュリティ脆弱性を含んでいることを強調している。
我々は,LLMがセキュアなコードを生成する能力を高めるための新しいアプローチであるHexaCoderを紹介する。
論文 参考訳(メタデータ) (2024-09-10T12:01:43Z) - Automated Repair of AI Code with Large Language Models and Formal Verification [4.9975496263385875]
次世代のAIシステムは強力な安全保証を必要とする。
本稿では,ニューラルネットワークと関連するメモリ安全性特性のソフトウェア実装について述べる。
これらの脆弱性を検出し、大きな言語モデルの助けを借りて自動的に修復します。
論文 参考訳(メタデータ) (2024-05-14T11:52:56Z) - Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling Vulnerabilities in Code Generated by Large Language Models [3.4887856546295333]
この研究は、最先端の大規模言語モデル(LLM)の比較分析を提供する。
中立なゼロショットプロンプトを使って単純なCプログラムを書く際に、脆弱性が発生する可能性を分析する。
論文 参考訳(メタデータ) (2024-04-29T01:24:14Z) - CodeAttack: Revealing Safety Generalization Challenges of Large Language Models via Code Completion [117.178835165855]
本稿では,自然言語入力をコード入力に変換するフレームワークであるCodeAttackを紹介する。
我々の研究は、コード入力に対するこれらのモデルの新たな、普遍的な安全性の脆弱性を明らかにした。
CodeAttackと自然言語の分布ギャップが大きくなると、安全性の一般化が弱くなる。
論文 参考訳(メタデータ) (2024-03-12T17:55:38Z) - Learning to Quantize Vulnerability Patterns and Match to Locate
Statement-Level Vulnerabilities [19.6975205650411]
さまざまな脆弱性パターンを表す量子化されたベクトルで構成される脆弱性コードブックが学習される。
推論の間、コードブックは、すべての学習パターンにマッチし、潜在的な脆弱性の存在を予測するために反復される。
提案手法は188,000以上のC/C++関数からなる実世界のデータセットに対して広範に評価された。
論文 参考訳(メタデータ) (2023-05-26T04:13:31Z) - A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。
我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。
本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
論文 参考訳(メタデータ) (2023-05-24T05:54:10Z) - CodeLMSec Benchmark: Systematically Evaluating and Finding Security
Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。
これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。
この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
論文 参考訳(メタデータ) (2023-02-08T11:54:07Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳(メタデータ) (2022-06-04T22:01:05Z) - VELVET: a noVel Ensemble Learning approach to automatically locate
VulnErable sTatements [62.93814803258067]
本稿では,ソースコード中の脆弱な文を見つけるための新しいアンサンブル学習手法であるVELVETを提案する。
我々のモデルは、グラフベースとシーケンスベースニューラルネットワークを組み合わせて、プログラムグラフの局所的およびグローバル的コンテキストを捕捉する。
VELVETは、合成データと実世界のデータに対して、それぞれ99.6%と43.6%の精度を達成している。
論文 参考訳(メタデータ) (2021-12-20T22:45:27Z) - Software Vulnerability Detection via Deep Learning over Disaggregated
Code Graph Representation [57.92972327649165]
この研究は、コードコーパスから安全でないパターンを自動的に学習するためのディープラーニングアプローチを探求する。
コードには解析を伴うグラフ構造が自然に認められるため,プログラムの意味的文脈と構造的規則性の両方を利用する新しいグラフニューラルネットワーク(GNN)を開発する。
論文 参考訳(メタデータ) (2021-09-07T21:24:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。