論文の概要: An AI Approach to Verified Production Cryptographic Libraries
- arxiv url: http://arxiv.org/abs/2608.00965v1
- Date: Sun, 02 Aug 2026 03:32:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-04 15:07:25.037846
- Title: An AI Approach to Verified Production Cryptographic Libraries
- Title（参考訳）: 検証された生成暗号ライブラリに対するAIアプローチ
- Authors: Chuyue Sun, Su Fong, Zhiyi Kuang, Yizheng Jiao, Nina Narodytska, Haoze Wu, David L. Dill, Clark Barrett,
- Abstract要約: 我々は、高レベルのAPI契約から内部仕様とVerusチェックされた証明を合成するAIベースのシステムであるCryptoProverを提案する。
実行可能なコードを変更することなく、CryptoProverはCrypto25519-dalekの新しい独立した証明を構築している。
- 参考スコア（独自算出の注目度）: 5.564288012051712
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isolated obligations with specifications and premises already given, leaving production-library verification unresolved. We present CryptoProver, an AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts. Without changing executable code, CryptoProver constructs a new independent proof of curve25519-dalek and verifies RustCrypto's previously unverified chacha20 implementation against an RFC 8439 specification. These cryptographic lineages underpin deployed systems including Signal and Shadowsocks; Signal has an estimated 218M global downloads. The independent, human-led curve25519-dalek verification was developed publicly over eight months by five main contributors. Given the API contracts and a fixed trusted library of field specifications, arithmetic facts, axioms, and vstd, CryptoProver synthesizes the internal specifications and proofs in 11.4 hours with USD 466.99 in recorded API cost. CryptoProver follows a trust-first design principle: mechanical gates reject specification weakening, invented axioms, and cross-module breakage, while isolation blocks reference proof retrieval, including from git history.
- Abstract（参考訳）: 暗号コードは正確でなければならない重要なインフラストラクチャですが、運用ライブラリを公式に検証することは難しいままです。
既存の言語モデル証明システムは、すでに与えられた仕様と前提で分離された義務を解決し、プロダクション・ライブラリーの検証は未解決のままである。
我々は、高レベルのAPI契約から内部仕様とVerusチェックされた証明を合成するAIベースのシステムであるCryptoProverを提案する。
実行可能なコードを変更することなく、CryptoProverはvell25519-dalekの新しい独立した証明を構築し、RFC 8439仕様に対してRustCryptoの未検証のchacha20実装を検証する。
SignalとShadowsocksは2億8800万ダウンロードと推定されている。
独立した、人間主導の Curve25519-dalek 検証は、主要な5人のコントリビュータによって8ヶ月にわたって公に開発された。
APIコントラクトと、フィールド仕様、算術的事実、公理、および vstd の固定された信頼できるライブラリを考えると、CryptoProverは内部仕様と証明を11.4時間で合成し、USD 466.99は記録されたAPIコストで記録される。
CryptoProverは信頼第一の設計原則に従う: 機械ゲートは仕様の弱体化を拒絶し、公理を発明し、モジュール間の切断を回避し、アイソレーションはgit履歴を含む参照証明の検索をブロックする。
関連論文リスト
- ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
ShannonProverは暗号証明を自動化するエージェントフレームワークである。
暗号化者がセキュリティモデルを提供し、ターゲット定理をProvレベルの証明義務に分解する設定をターゲットにしている。
本稿では,ShannonProverがケーススタディの暗号証明工学のかなりの部分を自動化可能であることを示す。
論文 参考訳（メタデータ） (2026-07-03T00:50:51Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
マルチチェーンエコシステムの重要な基盤であるクロスチェーンブリッジは、攻撃者にとって主要なターゲットとなっている。
バイトコードレベルの静的解析のような既存の防御は、チェーン間の相互作用のセマンティックな複雑さを扱うには不十分である。
パターンマッチングから体系的な第一原理検証へ自動的なクロスチェーンスマートコントラクト監査を移行するフレームワークであるGoAT-Xを提案する。
論文 参考訳（メタデータ） (2026-04-27T11:34:21Z) - CryptoScope: Utilizing Large Language Models for Automated Cryptographic Logic Vulnerability Detection [10.620899430085576]
我々は,Large Language Models(LLMs)を利用した暗号脆弱性の自動検出のための新しいフレームワークであるCryptoScopeを紹介する。
CryptoScopeがChain-of-Thought(CoT)とRetrieval-Augmented Generation(RAG)を併用
我々は,LLM-CLVAのCryptoScopeの評価を行った。
論文 参考訳（メタデータ） (2025-08-15T17:07:54Z) - Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。
この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。
バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
論文 参考訳（メタデータ） (2025-06-24T13:42:59Z) - VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
LLM生成コードの正確性を保証することは依然として困難である。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
論文 参考訳（メタデータ） (2025-05-29T06:12:52Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - Demystifying and Detecting Cryptographic Defects in Ethereum Smart Contracts [14.203991954526789]
スマートコントラクトにおける暗号欠陥の解読と検出を目的とした,最初の研究を行った。
我々は,スマートコントラクトにおける暗号欠陥検出を自動化するファジィベースのツールであるCrySolを提案した。
25,745の暗号関連スマートコントラクトを含む大規模データセットを収集し,CrySolの有効性を評価した。
論文 参考訳（メタデータ） (2024-08-09T08:40:08Z) - The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。
Aptosのメインネットからの測定によると、楽観的なアプローチは遅延オーバーヘッドを71%削減する。
論文 参考訳（メタデータ） (2024-07-16T20:53:04Z) - CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。
主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。
理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
論文 参考訳（メタデータ） (2023-05-20T11:26:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。