論文の概要: VUPER: Verified ASN.1 UPER Parser

• arxiv url: http://arxiv.org/abs/2608.09094v1
• Date: Mon, 10 Aug 2026 03:47:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-11 19:16:37.072437
• Title: VUPER: Verified ASN.1 UPER Parser
• Title（参考訳）: VUPER: ASN.1 UPERパーサの検証
• Abstract要約: 本稿では,認証された ASN.1 UPER を生成するためのフレームワーク VUPER を提案する。 VUPERは、一般的なコンパイラの20種類の不整合を明らかにし、SN.1 UPER標準への厳格な準拠を示す。 これらの脆弱性を利用した具体的な攻撃を実演する。
• 参考スコア（独自算出の注目度）: 19.74234190254681
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: ASN.1 is a widely used interface description language, and UPER (Unaligned Packed Encoding Rules) is one of its key encoding rules, particularly popular in security-critical domains such as cellular networks and vehicle-to-everything (V2X) communication. To ensure the correctness and security of this foundational infrastructure, we present VUPER, a framework for generating verified ASN.1 UPER parsers. We first formalize the notion of a bit-precise parser and identify properties that prove round-trip consistency for parsers and serializers, while accounting for ASN.1 features such as backward/forward compatibility. We then implement and verify parser and serializer combinators for ASN.1 basic types and structures, while adhering to the UPER specification. We also develop a compiler that translates ASN.1 definitions into verified parsers. Finally, we develop a dynamic testing framework using the VUPER parser as a test oracle. To empirically evaluate our approach, we test 7 open-source and 4 commercial ASN.1 parsers using 5G and V2X communication protocols. VUPER uncovers 20 types of inconsistencies in popular parsers and demonstrates stricter compliance with ASN.1 UPER standards. Additionally, we demonstrate concrete attacks by exploiting these parser vulnerabilities.
• Abstract（参考訳）: ASN.1は広く使われているインタフェース記述言語であり、UPER(Unaligned Packed Encoding Rules)は重要な符号化ルールの1つであり、特にセルラーネットワークやV2X通信のようなセキュリティクリティカルなドメインで人気がある。 この基盤インフラの正しさと安全性を確保するため、検証された ASN.1 を生成するためのフレームワーク VUPER を提案する。 UPERパーサー。 まず、ビット精度パーサの概念を定式化し、解析器とシリアライザのラウンドトリップ一貫性を証明する特性を定式化し、後方互換性や前方互換性などの ASN.1 の機能を考慮する。 次に、UPER仕様に準拠しつつ、ASN.1の基本型と構造のためのパーサとシリアライザのコンビネータを実装し、検証する。 また、ASN.1定義を検証されたパーサに変換するコンパイラも開発しています。 最後に,VUPERパーサをテストオラクルとして使用した動的テストフレームワークを開発した。 提案手法を実証的に評価するために,5GおよびV2X通信プロトコルを用いて7つのオープンソースと4つの商用ASN.1パーサを試験した。 VUPERは、人気のあるパーサーの20種類の不整合を明らかにし、ASN.1への厳格なコンプライアンスを実証する UPER標準。 さらに、これらのパーサ脆弱性を利用した具体的な攻撃を実演する。

関連論文リスト

• Weave of Formal Thought [51.56484100374058]
  WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。 本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。 Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
  論文  参考訳（メタデータ） (2026-06-24T15:58:11Z)
• Protocol Testing with I/O Grammars [45.68497486907946]
  本稿では,単一フレームワークにおける入力生成と出力チェックを組み合わせた新しいプロトコルテスト手法を提案する。 我々は、I/O文法が、テスト中のプログラムの出力検証を可能にするとともに、高度なプロトコルの特徴を正しく、完全に指定できることを実証する。
  論文  参考訳（メタデータ） (2025-09-24T16:41:04Z)
• XML Prompting as Grammar-Constrained Interaction: Fixed-Point Semantics, Convergence Guarantees, and Human-AI Protocols [0.2864713389096699]
  我々は、(i)文法制約付きデコード、(ii)階層的プロンプトの格子上の固定点意味論、(iii)収束型人間とAIの相互作用ループを統一するXMLプロンプトの論理第一処理を開発する。 数学的に完全な証明を提供し、我々のフレームワークを文法に整合した復号化、検証の連鎖、プログラム的プロンプトの最近の進歩に結びつける。
  論文  参考訳（メタデータ） (2025-09-09T23:03:53Z)
• Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE [1.2419340000421064]
  検証およびシリアライザのライブラリであるPulseParseを紹介します。 我々は、バイナリデータフォーマット標準であるCBORの最初の形式化を提供することで、大規模にPulseParseを使用します。 一定のスタックスペースしか持たないフォーマットを解析する方法を示す。
  論文  参考訳（メタデータ） (2025-05-22T23:12:03Z)
• Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
  プロトコル標準は一般的に自然言語で書かれるが、実装はソースコードで書かれている。 大規模言語モデル(LLM)に基づくフレームワークであるPARVALを提案する。 プロトコル標準とそれらの実装の両方を、フォーマット仕様と呼ばれる統一された中間表現に変換する。 実装とRFC標準の矛盾をうまく識別し、偽陽性率は5.6%と低い。
  論文  参考訳（メタデータ） (2025-04-18T07:09:56Z)
• Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study [0.0]
  ASN.1は地上および宇宙通信で広く使われているデータ構造を記述するための言語である。 ACN は ASN.1 に沿って、複雑なバイナリフォーマットとレガシプロトコルを記述するために使用できる。 ASN.1/ACNコードジェネレータをScalaコードに移植する方法を示す。 次に、生成元を拡張して、実行可能コードだけでなく、十分な事前条件、後条件、帰納的証明のための補題を出力します。
  論文  参考訳（メタデータ） (2024-12-10T06:54:42Z)
• Cross-domain Chinese Sentence Pattern Parsing [67.1381983012038]
  文パターン構造解析(SPS)は、主に言語教育に使用される構文解析法である。 既存のSPSは教科書のコーパスに大きく依存しており、クロスドメイン機能に欠ける。 本稿では,大規模言語モデル(LLM)を自己学習フレームワーク内で活用する革新的な手法を提案する。
  論文  参考訳（メタデータ） (2024-02-26T05:30:48Z)
• Compositional Program Generation for Few-Shot Systematic Generalization [59.57656559816271]
  コンポジションプログラムジェネレータ(CPG)と呼ばれるニューロシンボリックアーキテクチャに関する研究 CPGには3つの重要な特徴がある: 文法規則の形で、テキストモジュラリティ、テキストコンポジション、テキストタストラクションである。 SCAN と COGS のベンチマークでは,SCAN の14例と COGS の22例を使用して,完全な一般化を実現している。
  論文  参考訳（メタデータ） (2023-09-28T14:33:20Z)
• 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)

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

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