論文の概要: Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

• arxiv url: http://arxiv.org/abs/2505.17335v1
• Date: Thu, 22 May 2025 23:12:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-26 18:08:33.727574
• Title: Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
• Title（参考訳）: CBOR, CDDL, COSEに応用した分離論理によるセキュア解析とシリアライズ
• Authors: Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy,
• Abstract要約: 検証およびシリアライザのライブラリであるPulseParseを紹介します。 我々は、バイナリデータフォーマット標準であるCBORの最初の形式化を提供することで、大規模にPulseParseを使用します。 一定のスタックスペースしか持たないフォーマットを解析する方法を示す。
• 参考スコア（独自算出の注目度）: 1.2419340000421064
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Incorrect handling of security-critical data formats, particularly in low-level languages, are the root cause of many security vulnerabilities. Provably correct parsing and serialization tools that target languages like C can help. Towards this end, we present PulseParse, a library of verified parser and serializer combinators for non-malleable binary formats. Specifications and proofs in PulseParse are in separation logic, offering a more abstract and compositional interface, with full support for data validation, parsing, and serialization. PulseParse also supports a class of recursive formats -- with a focus on security and handling adversarial inputs, we show how to parse such formats with only a constant amount of stack space. We use PulseParse at scale by providing the first formalization of CBOR, a recursive, binary data format standard, with growing adoption in various industrial standards. We prove that the deterministic fragment of CBOR is non-malleable and provide EverCBOR, a verified library in both C and Rust to validate, parse, and serialize CBOR objects implemented using PulseParse. Next, we provide the first formalization of CDDL, a schema definition language for CBOR. We identify well-formedness conditions on CDDL definitions that ensure that they yield unambiguous, non-malleable formats, and implement EverCDDL, a tool that checks that a CDDL definition is well-formed, and then produces verified parsers and serializers for it. To evaluate our work, we use EverCDDL to generate verified parsers and serializers for various security-critical applications. Notably, we build a formally verified implementation of COSE signing, a standard for cryptographically signed objects. We also use our toolchain to generate verified code for other standards specified in CDDL, including DICE Protection Environment, a secure boot protocol standard.
• Abstract（参考訳）: セキュリティクリティカルなデータフォーマットの不正なハンドリングは、特に低レベルの言語では、多くのセキュリティ脆弱性の根本原因となっている。 おそらくCのような言語をターゲットにしたパースとシリアライズツールが役に立つだろう。 この目的のために、検証済みのパーサとシリアライザのコンビネータのライブラリであるPulseParseを紹介します。 PulseParseの仕様と証明は分離ロジックにあり、データ検証、解析、シリアライゼーションを完全にサポートする、より抽象的で構成的なインターフェースを提供する。 PulseParseはまた、再帰的なフォーマットのクラスもサポートしています -- セキュリティと敵入力の処理に重点を置いて、このようなフォーマットを一定量のスタックスペースで解析する方法を示します。 我々はPulseParseを、再帰的でバイナリなデータフォーマット標準であるCBORの最初の形式化を提供することで、大規模に使用しています。 我々は、CBORの決定論的フラグメントが非コンパイル可能であることを証明し、PulseParseを使って実装されたCBORオブジェクトを検証、解析、シリアライズするためのCとRustの両方で検証されたライブラリであるEverCBORを提供する。 次に、CBORのスキーマ定義言語であるCDDLの最初の形式化を提供する。 本報告では,CDDL定義の適合性条件を特定し,CDDL定義が良好であることを確認するツールであるEverCDDLを実装し,検証済みのパーサとシリアライザを生成する。 本研究では,EverCDDLを用いて,各種セキュリティクリティカルなアプリケーションに対して,検証済みのパーサとシリアライザを生成する。 特に、暗号署名されたオブジェクトの標準であるCOSE署名の正式な実装を構築します。 また、セキュアなブートプロトコル標準であるDICE保護環境など、CDDLで規定されている他の標準の検証コードを生成するために、ツールチェーンも使用しています。

関連論文リスト

• Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
  プロトコル標準は一般的に自然言語で書かれるが、実装はソースコードで書かれている。 大規模言語モデル(LLM)に基づくフレームワークであるPARVALを提案する。 プロトコル標準とそれらの実装の両方を、フォーマット仕様と呼ばれる統一された中間表現に変換する。 実装とRFC標準の矛盾をうまく識別し、偽陽性率は5.6%と低い。
  論文  参考訳（メタデータ） (2025-04-18T07:09:56Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
  BCSDは、悪意のあるコードスニペットの識別や、コードパターンの比較によるバイナリパッチ解析といったバイナリタスクに対処することができる。 バイナリは異なるコンパイル構成でコンパイルされるため、既存のアプローチはバイナリの類似性を比較する際にも注目すべき制限に直面している。 データ依存に基づいてバイナリコードをスライスし,スライスレベルの微調整を行うStrTuneを提案する。
  論文  参考訳（メタデータ） (2024-11-19T12:20:08Z)
• 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
  3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。 3DGenはテストスイートに準拠した3D仕様を生成する。
  論文  参考訳（メタデータ） (2024-04-16T07:53:28Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• Blind Evaluation Framework for Fully Homomorphic Encryption and Privacy-Preserving Machine Learning [0.0]
  Blind Evaluation Framework (BEF) は暗号的にセキュアなプログラミングフレームワークである。 インタラクティブ・ラウンド・オブ・デクリプション・アンド・アセスメント(IRDE)を使わずに、盲目で、正しい、プログラミングロジックの実行を可能にする。 これは、解読ラウンドなしでFHEで機械学習モデルのトレーニングと推論を可能にする最初のフレームワークである。
  論文  参考訳（メタデータ） (2023-10-19T20:33:02Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。 英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。 このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
  論文  参考訳（メタデータ） (2021-04-15T16:08:43Z)
• Towards Instance-Level Parser Selection for Cross-Lingual Transfer of Dependency Parsers [59.345145623931636]
  我々は、インスタンスレベルの選択(ILPS)という、新しい言語間移動パラダイムを論じる。 本稿では,デレキシライズドトランスファーの枠組みにおけるインスタンスレベルの選択に着目した概念実証研究を提案する。
  論文  参考訳（メタデータ） (2020-04-16T13:18:55Z)

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

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