The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification

要約

このペーパーでは、脆弱性分類を備えた、AI によって生成された 112,000 個のコンパイル可能な独立した C プログラムの大規模なコレクションである FormAI データセットについて説明します。
大規模言語モデル (LLM) を利用して多様なプログラムのセットを生成するように構築された、動的なゼロショット プロンプト手法を紹介します。
データセットは GPT-3.5-turbo によって生成され、さまざまな複雑さのレベルのプログラムで構成されています。
ネットワーク管理、テーブル ゲーム、暗号化などの複雑なタスクを処理するプログラムもあれば、文字列操作などの単純なタスクを処理するプログラムもあります。
すべてのプログラムには、ソース コード内で見つかった脆弱性のラベルが付けられ、タイプ、行番号、脆弱な関数名が示されます。
これは、効率的な SMT ベースの有界モデル チェッカー (ESBMC) を使用した形式的検証手法を採用することによって実現されます。ESBMC は、モデル チェック、抽象解釈、制約プログラミング、および充足可能性モジュロ理論を実行して、プログラム内の安全性/セキュリティ特性を推論します。
このアプローチは脆弱性を明確に検出し、反例として知られる正式なモデルを提供するため、誤検知レポートが生成される可能性が排除されます。
データセットのこの特性により、さまざまな静的および動的分析ツールの有効性を評価するのに適しています。
さらに、特定された脆弱性を、関連する Common Weakness Enumeration (CWE) 番号に関連付けました。
当社では、112,000 のプログラムのソース コードを公開しており、そのソース コードには、個々のプログラムで検出された脆弱性 (場所や関数名など) を詳細に記載した包括的なリストが添付されており、LLM や機械学習アルゴリズムのトレーニングに最適なデータセットとなっています。

要約(オリジナル)

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 a diverse set of 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 such as 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 performs 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. This property of the dataset makes it suitable for evaluating the effectiveness of various static and dynamic analysis tools. Furthermore, we have associated the identified vulnerabilities with relevant Common Weakness Enumeration (CWE) numbers. We make the source code available for the 112,000 programs, accompanied by a comprehensive list detailing the vulnerabilities detected in each individual program including location and function name, which makes the dataset ideal to train LLMs and machine learning algorithms.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google