論文の概要: A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

• arxiv url: http://arxiv.org/abs/2305.14752v2
• Date: Thu, 27 Jun 2024 18:40:19 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-01 22:23:58.512400
• Title: A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
• Title（参考訳）: ソフトウェアセキュリティの新しい時代 - 大規模言語モデルと形式的検証による自己修復ソフトウェアを目指して
• Authors: Norbert Tihanyi, Ridhi Jain, Yiannis Charalambous, Mohamed Amine Ferrag, Youcheng Sun, Lucas C. Cordeiro,
• Abstract要約: 本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。 我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。 本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
• 参考スコア（独自算出の注目度）: 8.733354577147093
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. Initially, we employ Bounded Model Checking (BMC) to identify vulnerabilities and extract counterexamples. These counterexamples are supported by mathematical proofs and the stack trace of the vulnerabilities. Using a specially designed prompt, we combine the original source code with the identified vulnerability, including its stack trace and counterexample that specifies the line number and error type. This combined information is then fed into an LLM, which is instructed to attempt to fix the code. The new code is subsequently verified again using BMC to ensure the fix succeeded. We present the ESBMC-AI framework as a proof of concept, leveraging the well-recognized and industry-adopted Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained transformer model to detect and fix errors in C programs, particularly in critical software components. We evaluated our approach on 50,000 C programs randomly selected from the FormAI dataset with their respective vulnerability classifications. Our results demonstrate ESBMC-AI's capability to automate the detection and repair of issues such as buffer overflow, arithmetic overflow, and pointer dereference failures with high accuracy. ESBMC-AI is a pioneering initiative, integrating LLMs with BMC techniques, offering potential integration into the continuous integration and deployment (CI/CD) process within the software development lifecycle.
• Abstract（参考訳）: 本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。 当初は、脆弱性を特定し、反例を抽出するために境界モデルチェック(BMC)を使用しました。 これらの反例は、数学的証明と脆弱性のスタックトレースによってサポートされている。 特別に設計されたプロンプトを用いて、元のソースコードと識別された脆弱性を組み合わせ、そのスタックトレースと、行番号とエラータイプを指定する逆例を含む。 この組み合わせた情報はLLMに送られ、コードを修正するように指示される。 その後、新しいコードがBMCを使用して再検証され、修正が成功する。 我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と、トレーニング済みのトランスフォーマーモデルを利用して、Cプログラム、特に重要なソフトウェアコンポーネントのエラーを検出し、修正する。 我々は,各脆弱性分類を用いて,FormAIデータセットからランダムに選択された5万個のCプログラムに対するアプローチを評価した。 本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。 ESBMC-AIは先駆的なイニシアチブで、LCMとBMCの技術を統合することで、ソフトウェア開発ライフサイクルにおける継続的インテグレーションとデプロイメント(CI/CD)プロセスへの潜在的な統合を提供します。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Agent-Driven Automatic Software Improvement [55.2480439325792]
  本提案は,Large Language Models (LLMs) を利用したエージェントの展開に着目して,革新的なソリューションの探求を目的とする。 継続的学習と適応を可能にするエージェントの反復的性質は、コード生成における一般的な課題を克服するのに役立ちます。 我々は,これらのシステムにおける反復的なフィードバックを用いて,エージェントの基盤となるLLMをさらに微調整し,自動化されたソフトウェア改善のタスクに整合性を持たせることを目指している。
  論文  参考訳（メタデータ） (2024-06-24T15:45:22Z)
• Verifying components of Arm(R) Confidential Computing Architecture with ESBMC [6.914213030256384]
  Realm Management Monitor (RMM) はArm Confidential Computing Architecture (Arm CCA) において重要なファームウェアコンポーネントである これまでの研究は、RMMの仕様とプロトタイプ参照実装の検証に形式的検証技術を適用していた。 本稿では,SMT(Satifiability Modulo Theories)ベースのソフトウェアモデルチェッカーであるESBMCの適用について述べる。
  論文  参考訳（メタデータ） (2024-06-05T09:09:37Z)
• Automated Repair of AI Code with Large Language Models and Formal Verification [4.9975496263385875]
  次世代のAIシステムは強力な安全保証を必要とする。 本稿では,ニューラルネットワークと関連するメモリ安全性特性のソフトウェア実装について述べる。 これらの脆弱性を検出し、大きな言語モデルの助けを借りて自動的に修復します。
  論文  参考訳（メタデータ） (2024-05-14T11:52:56Z)
• Automating SBOM Generation with Zero-Shot Semantic Similarity [2.169562514302842]
  Software-Bill-of-Materials (SBOM)は、ソフトウェアアプリケーションのコンポーネントと依存関係を詳述した総合的なインベントリである。 本稿では,破壊的なサプライチェーン攻撃を防止するため,SBOMを自動生成する手法を提案する。 テスト結果は説得力があり、ゼロショット分類タスクにおけるモデルの性能を示す。
  論文  参考訳（メタデータ） (2024-02-03T18:14:13Z)
• The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification [3.2925005312612323]
  本稿では,脆弱性分類を伴う112,000のAI生成Cプログラムの大規模なコレクションであるFormAIデータセットを提案する。 すべてのプログラムには、型、行番号、脆弱な関数名を示すソースコード内の脆弱性がラベル付けされている。 ソースコードは112,000のプログラムで利用でき、各プログラムで検出された脆弱性を含む別のファイルが付属する。
  論文  参考訳（メタデータ） (2023-07-05T10:39:58Z)
• PEOPL: Characterizing Privately Encoded Open Datasets with Public Labels [59.66777287810985]
  プライバシとユーティリティのための情報理論スコアを導入し、不誠実なユーザの平均パフォーマンスを定量化する。 次に、ランダムなディープニューラルネットワークの使用を動機付ける符号化スキームのファミリーを構築する際のプリミティブを理論的に特徴づける。
  論文  参考訳（メタデータ） (2023-03-31T18:03:53Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。 これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。 この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
  論文  参考訳（メタデータ） (2023-02-08T11:54:07Z)
• CodeRL: Mastering Code Generation through Pretrained Models and Deep Reinforcement Learning [92.36705236706678]
  CodeRLは、事前訓練されたLMと深層強化学習によるプログラム合成タスクのための新しいフレームワークである。 推論中、我々は重要なサンプリング戦略を持つ新しい生成手順を導入する。 モデルバックボーンについては,CodeT5のエンコーダデコーダアーキテクチャを拡張し,学習目標を拡張した。
  論文  参考訳（メタデータ） (2022-07-05T02:42:15Z)
• Integrate Lattice-Free MMI into End-to-End Speech Recognition [87.01137882072322]
  音声認識(ASR)研究において、識別基準はDNN-HMMシステムにおいて優れた性能を達成している。 このモチベーションにより、差別的基準の採用は、エンドツーエンド(E2E)のASRシステムの性能を高めることを約束している。 これまでの研究は、最小ベイズリスク(MBR、差別基準の一つ)をE2E ASRシステムに導入してきた。 本研究では,他の広く使われている識別基準であるLF-MMIをE2Eに統合する新しいアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-03-29T14:32:46Z)
• Multi-context Attention Fusion Neural Network for Software Vulnerability Identification [4.05739885420409]
  ソースコードのセキュリティ脆弱性の共通カテゴリのいくつかを効率的に検出することを学ぶディープラーニングモデルを提案する。 モデルは、学習可能なパラメータの少ないコードセマンティクスの正確な理解を構築します。 提案したAIは、ベンチマークされたNIST SARDデータセットから特定のCWEに対して98.40%のF1スコアを達成する。
  論文  参考訳（メタデータ） (2021-04-19T11:50:36Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。