論文の概要: 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
- arxiv url: http://arxiv.org/abs/2404.10362v1
- Date: Tue, 16 Apr 2024 07:53:28 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-17 17:33:19.976477
- Title: 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
- Title(参考訳): 3DGen:AIによる、おそらく正しいバイナリフォーマットパーザの生成
- Authors: Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy,
- Abstract要約: 3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。
3DGenはテストスイートに準拠した3D仕様を生成する。
- 参考スコア(独自算出の注目度): 5.102523342662388
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use. In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D. To support humans in understanding and trusting the generated specifications, 3DGen uses symbolic methods to also synthesize test inputs that can be validated against an external oracle. Symbolic test generation also helps in distinguishing multiple plausible solutions. Through a process of repeated refinement, 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C. We have evaluated 3DGen on 20 Internet standard formats, demonstrating the potential for AI-agents to produce formally verified C code at a non-trivial scale. A key enabler is the use of a domain-specific language to limit AI outputs to a class for which automated, symbolic analysis is tractable.
- Abstract(参考訳): 特にプログラマがRFCの非公式な形式記述を低レベルのメモリアンセーフな言語で効率的に解析するロジックに書き起こす場合である。
何人かの研究者が、効率的なコードを抽出できるデータフォーマットの正式な仕様言語を提案している。
しかし、非公式な要件を形式的な仕様に抽出することは困難であり、その利点にもかかわらず、新しい形式言語は人々が学び、使うのが難しい。
本稿では,AIエージェントを用いて自然言語文書(RFC)やサンプル入力を3Dと呼ばれる言語でフォーマット仕様に変換する3DGenを提案する。
生成された仕様を理解し信頼するために、3DGenはシンボリックメソッドを使用して、外部のオラクルに対して検証可能なテストインプットを合成する。
シンボリックテスト生成は、複数の可算解の区別にも役立つ。
我々は、20のインターネット標準フォーマットで3DGenを評価し、AIエージェントが公式に認証されたCコードを非自明なスケールで生成する可能性を実証した。
重要なイネーブルは、AI出力を、自動化されたシンボリック分析が抽出可能なクラスに制限するために、ドメイン固有の言語を使用することである。
関連論文リスト
- CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [59.32609948217718]
我々は,Large Language Models(LLM)ベースのコード生成のための新しい透かし技術であるCodeIPを提案する。
CodeIPは、生成されたコードのセマンティクスを保持しながら、マルチビット情報の挿入を可能にする。
論文 参考訳(メタデータ) (2024-04-24T04:25:04Z) - FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。
FoC-BinLLMは、ROUGE-LスコアでChatGPTを14.61%上回った。
FoC-Simは52%高いRecall@1で過去のベストメソッドを上回っている。
論文 参考訳(メタデータ) (2024-03-27T09:45:33Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z) - Trusta: Reasoning about Assurance Cases with Formal Methods and Large
Language Models [4.005483185111992]
Trustworthiness Derivation Tree Analyzer (Trusta)は、TDTを自動構築し検証するデスクトップアプリケーションである。
バックエンドにはPrologインタプリタが内蔵されており、制約解決器Z3とMONAによってサポートされている。
Trustaは自然言語のテキストから形式的な制約を抽出し、解釈と検証を容易にする。
論文 参考訳(メタデータ) (2023-09-22T15:42:43Z) - From Ambiguity to Explicitness: NLP-Assisted 5G Specification
Abstraction for Formal Analysis [5.526122280732959]
我々はNLPツールを用いてデータを構築し、構築されたデータを用いて識別子と形式的特性を抽出する2段階パイプラインを提案する。
最適モデルの結果は,抽出精度が39%,形式的特性の同定精度が42%に達している。
論文 参考訳(メタデータ) (2023-08-07T03:37:31Z) - Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning [27.59524153097858]
文法制約付き復号法(GCD)は、大言語モデル(LM)の生成を制御するために用いられる。
GCDは一般に構造化NLPタスクの統一フレームワークとして機能する。
文法制約付きLMは、制約なしLMよりも大幅に優れるか、タスク固有の微調整モデルよりも優れていることを示す。
論文 参考訳(メタデータ) (2023-05-23T11:54:37Z) - Physics of Language Models: Part 1, Context-Free Grammar [61.05762942335984]
我々は、GPTのようなHOW生成言語モデルを研究するための制御実験を設計し、文脈自由文法(CFG)を学ぶ。
難しい(長くあいまいな)CFGであっても、事前学習したトランスフォーマーは、ほぼ完璧な精度と印象的な多様性で文を生成することができる。
論文 参考訳(メタデータ) (2023-05-23T04:28:16Z) - Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
本研究は,統計的,ニューラルベース,トランスフォーマーベースの機械学習手法に基づく形式性検出手法の体系的研究を初めて行う。
単言語,多言語,言語横断の3種類の実験を行った。
本研究は,モノリンガルおよび多言語形式分類タスクのためのトランスフォーマーベースモデルに対するChar BiLSTMモデルの克服を示す。
論文 参考訳(メタデータ) (2022-04-19T16:23:07Z) - Synchromesh: Reliable code generation from pre-trained language models [38.15391794443022]
コード生成のための事前学習モデルの信頼性を大幅に向上するフレームワークであるSynchromeshを提案する。
まず、TST(Target similarity Tuning)を使用して、トレーニングバンクから、セマンティックなサンプル選択の新しい方法を使用して、数ショットのサンプルを検索する。
次に、Synchromeshはサンプルをトレーニング済みの言語モデルに供給し、対象言語の有効なプログラムセットに出力を制約する一般的なフレームワークであるConstrained Semantic Decoding (CSD)を使用してプログラムをサンプリングする。
論文 参考訳(メタデータ) (2022-01-26T22:57:44Z) - CGEMs: A Metric Model for Automatic Code Generation using GPT-3 [0.0]
本研究は,理論的証明を用いて,あるいはモンテカルロシミュレーション法を用いてAI生成コンテンツを検証することを目的とする。
この場合、後者の手法を用いて統計的にかなりの数のサンプルを検査・検証する。
コンパイル、ロジック変換へのNL記述、必要な編集数、一般的に使用されている静的コードメトリクスとNLPメトリクス。
論文 参考訳(メタデータ) (2021-08-23T13:28:57Z) - Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。
英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。
このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
論文 参考訳(メタデータ) (2021-04-15T16:08:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。