論文の概要: Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution
- arxiv url: http://arxiv.org/abs/2512.11431v1
- Date: Fri, 12 Dec 2025 10:12:06 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-15 15:48:11.725166
- Title: Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution
- Title（参考訳）: DNSSECの正当性を証明する - ドメイン名解決の形式的アプローチ
- Authors: Qifan Zhang, Zilin Shen, Imtiaz Karim, Elisa Bertino, Zhou Li,
- Abstract要約: 本稿では、DNSSECプロトコルスイートの総合的かつ自動化されたセキュリティ分析のための最初のフレームワークであるDNSSECVerifを紹介する。
DNSSECのコアセキュリティ保証のうち4つを正式に証明し、標準における重要な曖昧さを明らかにします。
私たちの作業は、DNSSEC仕様と実装を強化するための重要なエビデンスベースのレコメンデーションを提供します。
- 参考スコア（独自算出の注目度）: 12.033681333491685
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: The Domain Name System Security Extensions (DNSSEC) are critical for preventing DNS spoofing, yet its specifications contain ambiguities and vulnerabilities that elude traditional "break-and-fix" approaches. A holistic, foundational security analysis of the protocol has thus remained an open problem. This paper introduces DNSSECVerif, the first framework for comprehensive, automated formal security analysis of the DNSSEC protocol suite. Built on the SAPIC+ symbolic verifier, our high-fidelity model captures protocol-level interactions, including cryptographic operations and stateful caching with fine-grained concurrency control. Using DNSSECVerif, we formally prove four of DNSSEC's core security guarantees and uncover critical ambiguities in the standards--notably, the insecure coexistence of NSEC and NSEC3. Our model also automatically rediscovers three classes of known attacks, demonstrating fundamental weaknesses in the protocol design. To bridge the model-to-reality gap, we validate our findings through targeted testing of mainstream DNS software and a large-scale measurement study of over 2.2 million open resolvers, confirming the real-world impact of these flaws. Our work provides crucial, evidence-based recommendations for hardening DNSSEC specifications and implementations.
- Abstract（参考訳）: DNSSEC(Domain Name System Security Extensions)はDNSの偽造を防止するために重要であるが、その仕様には従来の"ブレーク・アンド・フィックス"アプローチを損なう曖昧さと脆弱性が含まれている。
そのため、プロトコルの全体的、基礎的なセキュリティ分析は未解決の問題のままである。
本稿では、DNSSECプロトコルスイートの総合的かつ自動化されたセキュリティ分析のための最初のフレームワークであるDNSSECVerifを紹介する。
SAPIC+のシンボリック検証に基づいて構築された当社の高忠実度モデルは,暗号化操作やステートフルキャッシングなど,プロトコルレベルのインタラクションを微細な並行処理制御でキャプチャする。
DNSSECVerifを使用して、DNSSECのコアセキュリティ保証の4つを正式に証明し、標準における重要な曖昧さを明らかにする。
我々のモデルは、既知の攻撃の3つのクラスを自動で再分析し、プロトコル設計の根本的な弱点を示す。
モデルと現実のギャップを埋めるため、メインストリームDNSソフトウェアのターゲットテストと、220万以上のオープンリゾルバの大規模測定により、これらの欠陥の現実的な影響を検証した。
私たちの作業は、DNSSEC仕様と実装を強化するための重要なエビデンスベースのレコメンデーションを提供します。
関連論文リスト
- ReliabilityRAG: Effective and Provably Robust Defense for RAG-based Web-Search [69.60882125603133]
本稿では,検索した文書の信頼性情報を明確に活用する,敵対的堅牢性のためのフレームワークであるReliabilityRAGを提案する。
我々の研究は、RAGの回収されたコーパスの腐敗に対するより効果的で確実に堅牢な防御に向けた重要な一歩である。
論文 参考訳（メタデータ） (2025-09-27T22:36:42Z) - A Survey and Evaluation Framework for Secure DNS Resolution [0.749377967268953]
我々はDNS解決プロセスの攻撃と脅威を調査し、包括的脅威モデルを開発し、その体系的分類のための分類を攻撃する。
この分析により、特定された脅威を軽減するために、14の望ましいセキュリティ、プライバシ、可用性プロパティが定式化される。
評価の結果,解決経路全体にわたる理想的な保護策は存在しないことが明らかとなった。
論文 参考訳（メタデータ） (2025-09-17T08:07:20Z) - Overcoming DNSSEC Islands of Security: A TLS and IP-Based Certificate Solution [0.03262230127283452]
本稿では,DNSSECの信頼関係のギャップに対処する分散型アプローチを提案する。
我々はTLSとIPベースの証明書を活用し、階層レベル間のエンドツーエンドの認証を可能にする。
論文 参考訳（メタデータ） (2025-09-10T08:02:07Z) - Collusion Resistant DNS With Private Information Retrieval [42.34183823376613]
プライバシー保証を強化するために,シングルサーバのプライベート情報検索を利用したDNS拡張であるPDNSを提案する。
PDNSは許容パフォーマンス(TorよりもDoHよりも2倍速い)と、今日の強力なプライバシ保証を実現している。
論文 参考訳（メタデータ） (2025-07-28T13:17:25Z) - Implementing and Evaluating Post-Quantum DNSSEC in CoreDNS [0.4374837991804085]
本稿では,量子後暗号(PQC)アルゴリズムをCoreDNSに統合する。
5つのPQCシグネチャアルゴリズムファミリをサポートするCoreDNSを拡張するプラグインを開発した。
本実装では,既存のDNS解決フローとの互換性を維持しつつ,量子抵抗シグネチャを用いたオンザフライ署名を実現している。
論文 参考訳（メタデータ） (2025-07-12T14:34:17Z) - Quantum-Resistant Domain Name System: A Comprehensive System-Level Study [0.9365037811026767]
本稿では,広範に展開されている3つのメカニズムにまたがる,量子後DNSセキュリティに関する総合的なシステムレベル研究について述べる。
我々は、レガシー、ポスト量子、ハイブリッド暗号構成下でDNSセキュリティをベンチマークするための統合フレームワークであるポスト量子暗号(PQC)-DNSを提案する。
論文 参考訳（メタデータ） (2025-06-24T18:35:24Z) - CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳（メタデータ） (2024-11-20T14:16:55Z) - ss2DNS: A Secure DNS Scheme in Stage 2 [1.8379423176822356]
我々は、リゾルバと権威的なネームサーバ間の解決プロセスにおけるセキュリティとプライバシの脆弱性を軽減するために設計された、新しいDNSスキームであるss2DNSを紹介する。
サーバ側処理のレイテンシ、解像度時間、CPU使用率において、ss2DNSは安全性の低いスキームに匹敵するが、DNS-over-TLSを著しく上回る。
論文 参考訳（メタデータ） (2024-08-02T01:25:14Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - An Efficient and Multi-private Key Secure Aggregation for Federated Learning [41.29971745967693]
フェデレート学習のための効率的かつ多目的な鍵セキュアアグリゲーション手法を提案する。
具体的には、変種ElGamal暗号を巧みに修正し、同型加算演算を実現する。
高次元深層モデルパラメータに対しては,多次元データを1次元に圧縮する超増進シーケンスを導入する。
論文 参考訳（メタデータ） (2023-06-15T09:05:36Z) - Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。
本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。
われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
論文 参考訳（メタデータ） (2020-02-17T09:53:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。