Fugu-MT 論文翻訳(概要): Formal Verification of the Safegcd Implementation

論文の概要: Formal Verification of the Safegcd Implementation

arxiv url: http://arxiv.org/abs/2507.17956v1
Date: Wed, 23 Jul 2025 21:57:30 GMT
ステータス: 翻訳完了
システム内更新日: 2025-07-25 15:10:42.631769
Title: Formal Verification of the Safegcd Implementation
Title（参考訳）: Safegcd実装の形式的検証
Authors: Russell O'Connor, Andrew Poelstra,
Abstract要約: 拡張ユークリッドアルゴリズムに対する新しいアプローチが、Bitcoinで使用されているlibsecp256k1暗号ライブラリに開発され、組み込まれている。我々は,Coq証明アシスタントを用いた(一方の)libsecp256k1のモジュラー逆実装の正しさのコンピュータ検証を完了した。
参考スコア（独自算出の注目度）: 0.10742675209112622
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The modular inverse is an essential piece of computation required for elliptic curve operations used for digital signatures in Bitcoin and other applications. A novel approach to the extended Euclidean algorithm has been developed by Bernstein and Yang within the last few years and incorporated into the libsecp256k1 cryptographic library used by Bitcoin. However, novel algorithms introduce new risks of errors. To address this we have completed a computer verified proof of the correctness of (one of) libsecp256k1's modular inverse implementations with the Coq proof assistant using the Verifiable C's implementation of separation logic.
Abstract（参考訳）: モジュラー逆は、Bitcoinや他のアプリケーションにおけるデジタルシグネチャに使用される楕円曲線演算に必要な計算の不可欠な部分である。拡張ユークリッドアルゴリズムに対する新しいアプローチは、ここ数年でベルンシュタインとヤンによって開発され、Bitcoinで使用されているlibsecp256k1暗号ライブラリに組み込まれている。しかし、新しいアルゴリズムはエラーの新たなリスクをもたらす。この問題に対処するために,検証可能なCの分離論理の実装を用いたCoq証明アシスタントを用いて,(1つの)libsecp256k1のモジュラー逆実装の正当性を証明するコンピュータ証明を完了した。

関連論文リスト

A Non-leveled and Reliable Approximate FHE Framework through Binarized Polynomial Rings [1.1701842638497677]
ホモモルフィック暗号化(HE)は、暗号化されたデータに対するセキュアな計算を可能にし、クラウドコンピューティング、ヘルスケア、ファイナンスなどのドメインにおけるユーザのプライバシを保護する。 CKKSは、機械学習と数値計算の重要な要件である複素数に対する近似演算をサポートすることで有名である。本稿では,2値係数のリング上で完全に動作し,軽量なブートストラップ機構で再スケーリングを置き換えたCKKSの2値変種を提案する。
論文参考訳（メタデータ） (2025-08-04T22:53:36Z)
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)
Post-Quantum Cryptography: An Analysis of Code-Based and Lattice-Based Cryptosystems [55.49917140500002]
量子コンピュータはShorのアルゴリズムを使って最新の暗号システムを破ることができる。我々はまず、量子攻撃に対して安全とされるコードベースのスキームであるMcEliece暗号システムについて検討する。次に,最短ベクトル問題を解くことの難しさを基礎とした格子型システムNTRUについて検討する。
論文参考訳（メタデータ） (2025-05-06T03:42:38Z)
Cryptanalysis via Machine Learning Based Information Theoretic Metrics [58.96805474751668]
本稿では,機械学習アルゴリズムの新たな2つの応用法を提案する。これらのアルゴリズムは、監査設定で容易に適用でき、暗号システムの堅牢性を評価することができる。本稿では,DES,RSA,AES ECBなど,IND-CPAの安全でない暗号化スキームを高精度に識別する。
論文参考訳（メタデータ） (2025-01-25T04:53:36Z)
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)
Estimating the Decoding Failure Rate of Binary Regular Codes Using Iterative Decoding [84.0257274213152]
並列ビットフリップデコーダのDFRを高精度に推定する手法を提案する。本研究は,本症候群のモデル化およびシミュレーションによる重み比較,第1イテレーション終了時の誤りビット分布の誤検出,復号化復号化率(DFR)について検証した。
論文参考訳（メタデータ） (2024-01-30T11:40:24Z)
CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
この文書はセキュリティプロトコル検証器CryptoVerifを示す。これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
論文参考訳（メタデータ） (2023-10-23T07:53:38Z)
ArctyrEX : Accelerated Encrypted Execution of General-Purpose Applications [6.19586646316608]
FHE(Fully Homomorphic Encryption)は、計算中のユーザデータのプライバシとセキュリティを保証する暗号化手法である。我々は、暗号化実行を高速化する新しい技術を開発し、我々のアプローチの顕著な性能上の利点を実証する。
論文参考訳（メタデータ） (2023-06-19T15:15:41Z)
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
論文参考訳（メタデータ） (2023-05-20T11:26:51Z)
A quantum algorithm for finding collision-inducing disturbance vectors in SHA-1 [2.963904090194172]
現代の暗号プロトコルは、ユーザ認証やその他のセキュリティ検証のシグネチャとして機能する準ユニクティックな数値を生成するために、洗練されたハッシュ関数に依存している。セキュリティは、同一の番号にマッチするハッシュテキストを見つけ、いわゆる衝突攻撃を発生させることによって妥協される可能性がある。本稿では,絡み合った量子状態を利用して,候補外乱ベクトルの同時シード化を行うアルゴリズムを提案する。
論文参考訳（メタデータ） (2022-10-23T16:01:17Z)
A modular software framework for the design and implementation of ptychography algorithms [55.41644538483948]
我々は,Pychographyデータセットをシミュレートし,最先端の再構築アルゴリズムをテストすることを目的とした,新しいptychographyソフトウェアフレームワークであるSciComを紹介する。その単純さにもかかわらず、ソフトウェアはPyTorchインターフェースによる高速化処理を利用する。結果は合成データと実データの両方で示される。
論文参考訳（メタデータ） (2022-05-06T16:32:37Z)

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