論文の概要: Towards Efficient Verification of Constant-Time Cryptographic Implementations

• arxiv url: http://arxiv.org/abs/2402.13506v1
• Date: Wed, 21 Feb 2024 03:39:14 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-22 17:07:34.219421
• Title: Towards Efficient Verification of Constant-Time Cryptographic Implementations
• Title（参考訳）: 一定時間暗号実装の有効検証に向けて
• Authors: Luwei Cai and Fu Song and Taolue Chen
• Abstract要約: 一定時間プログラミングの規律は、タイミングサイドチャネル攻撃に対する効果的なソフトウェアベースの対策である。 本研究では, テナント解析の新たな相乗効果と自己構成プログラムの安全性検証に基づく実用的検証手法を提案する。 当社のアプローチはクロスプラットフォームで完全に自動化されたCT-Proverとして実装されている。
• 参考スコア（独自算出の注目度）: 5.433710892250037
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software security. Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks, but developing constant-time implementations turns out to be challenging and error-prone. Current verification approaches/tools suffer from scalability and precision issues when applied to production software in practice. In this paper, we put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Specifically, we first use an IFDS-based lightweight taint analysis to prove that a large number of potential (timing) side-channel sources do not actually leak secrets. We then resort to a precise taint analysis and a safety verification approach to determine whether the remaining potential side-channel sources can actually leak secrets. These include novel constructions of taint-directed semi-cross-product of the original program and its Boolean abstraction, and a taint-directed self-composition of the program. Our approach is implemented as a cross-platform and fully automated tool CT-Prover. The experiments confirm its efficiency and effectiveness in verifying real-world benchmarks from modern cryptographic and SSL/TLS libraries. In particular, CT-Prover identify new, confirmed vulnerabilities of open-source SSL libraries (e.g., Mbed SSL, BearSSL) and significantly outperforms the state-of-the-art tools.
• Abstract（参考訳）: タイミングサイドチャネル攻撃は、暗号実装の秘密を完全にまたは部分的に回復するために秘密に依存した実行時間を利用する。 コンスタントタイムプログラミングの分野は、タイミングのサイドチャネル攻撃に対する効果的なソフトウェアベースの対策であるが、コンスタントタイム実装の開発は困難でエラーやすいことが判明した。 現在の検証アプローチ/ツールは、実運用ソフトウェアに適用する場合、スケーラビリティと精度の問題に苦しむ。 本稿では,taint分析の新たなシナジーと自己合成プログラムの安全性検証に基づく実践的検証手法を提案する。 具体的には、まず、ifdsベースの軽量なtaint分析を使用して、多数の潜在(timing)サイドチャネルソースが実際には秘密を漏らしていないことを証明します。 次に、正確なtaint分析と安全性検証アプローチを用いて、残りの潜在的サイドチャネルソースが実際に秘密を漏らすことができるかどうかを判断する。 これには、オリジナルのプログラムのtaint-directed semi-cross-productとそのbooleanの抽象化、taint-directed self-compositionの新規な構成が含まれる。 当社のアプローチはクロスプラットフォームで完全に自動化されたCT-Proverとして実装されている。 実験は、現代の暗号およびSSL/TLSライブラリから実世界のベンチマークを検証するための効率と有効性を確認した。 特にct-proverは、オープンソースのsslライブラリ(例えば、mbed ssl、beassl)の新たな脆弱性を特定し、最先端ツールを大幅に上回っている。

関連論文リスト

• Secret Breach Prevention in Software Issue Reports [2.8747015994080285]
  本稿では,ソフトウェア問題報告における秘密漏洩検出のための新しい手法を提案する。 ログファイル、URL、コミットID、スタックトレース、ダミーパスワードなど、ノイズによって引き起こされる課題を強調します。 本稿では,最先端技術の強みと言語モデルの文脈的理解を組み合わせたアプローチを提案する。
  論文  参考訳（メタデータ） (2024-10-31T06:14:17Z)
• Divide and Conquer based Symbolic Vulnerability Detection [0.16385815610837165]
  本稿では,シンボル実行と制御フローグラフ解析に基づく脆弱性検出手法を提案する。 提案手法では,無関係なプログラム情報を除去するために,分割・分散アルゴリズムを用いる。
  論文  参考訳（メタデータ） (2024-09-20T13:09:07Z)
• The Impact of SBOM Generators on Vulnerability Assessment in Python: A Comparison and a Novel Approach [56.4040698609393]
  Software Bill of Materials (SBOM) は、ソフトウェア構成における透明性と妥当性を高めるツールとして推奨されている。 現在のSBOM生成ツールは、コンポーネントや依存関係を識別する際の不正確さに悩まされることが多い。 提案するPIP-sbomは,その欠点に対処する新しいピップインスパイアされたソリューションである。
  論文  参考訳（メタデータ） (2024-09-10T10:12:37Z)
• An Extensive Comparison of Static Application Security Testing Tools [1.3927943269211593]
  静的アプリケーションセキュリティテストツール(SASTT)は、ソフトウェアアプリケーションのセキュリティと信頼性をサポートするソフトウェア脆弱性を特定する。 いくつかの研究は、偽アラームを発生させる傾向があるため、代替ソリューションがSASTTよりも効果的である可能性を示唆している。 SASTTの評価は、制御されているが合成されたJavaに基づいています。
  論文  参考訳（メタデータ） (2024-03-14T09:37:54Z)
• QTFlow: Quantitative Timing-Sensitive Information Flow for Security-Aware Hardware Design on RTL [0.3679557794795275]
  設計段階でのハードウェア情報漏洩を定量化する,タイミングに敏感なフレームワークQTFlowを紹介する。 QTFlowは、タイミングチャネルを自律的に識別し、時間に依存しない分析から生じるすべての偽陽性を減少させる。
  論文  参考訳（メタデータ） (2024-01-31T13:22:57Z)
• SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
  本稿では,SOCIの性能を大幅に向上させるSOCI+を提案する。 SOCI+は、暗号プリミティブとして、高速な暗号化と復号化を備えた(2, 2)ホールドのPaillier暗号システムを採用している。 実験の結果,SOCI+は計算効率が最大5.4倍,通信オーバヘッドが40%少ないことがわかった。
  論文  参考訳（メタデータ） (2023-09-27T05:19:32Z)
• Empirical Analysis of Software Vulnerabilities Causing Timing Side Channels [2.0794749869068005]
  本研究では,非暗号ソフトウェアにおけるタイミング攻撃関連脆弱性について検討する。 既知のセキュアなコーディングプラクティスに従わなかったため、タイミングアタック関連の脆弱性の大部分が導入されたことが分かりました。 この研究の結果は、ソフトウェアセキュリティコミュニティがタイミング攻撃に関連する脆弱性の性質と原因に関する証拠に基づく情報を得るのに役立つことが期待されている。
  論文  参考訳（メタデータ） (2023-08-23T01:38:03Z)
• Using Machine Learning To Identify Software Weaknesses From Software Requirement Specifications [49.1574468325115]
  本研究は、要求仕様からソフトウェア弱点を特定するための効率的な機械学習アルゴリズムを見つけることに焦点を当てる。 ProMISE_exp. Naive Bayes、サポートベクターマシン(SVM)、決定木、ニューラルネットワーク、畳み込みニューラルネットワーク(CNN)アルゴリズムをテストした。
  論文  参考訳（メタデータ） (2023-08-10T13:19:10Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。 近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。 本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
  論文  参考訳（メタデータ） (2022-11-29T13:32:38Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  本稿では,学習時の安全性維持が不可欠である高次元非線形最適化問題に対する一般的なアプローチを提案する。 LBSGDと呼ばれるアプローチは、慎重に選択されたステップサイズで対数障壁近似を適用することに基づいている。 安全強化学習における政策課題の違反を最小限に抑えるためのアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-07-21T11:14:47Z)
• VELVET: a noVel Ensemble Learning approach to automatically locate VulnErable sTatements [62.93814803258067]
  本稿では,ソースコード中の脆弱な文を見つけるための新しいアンサンブル学習手法であるVELVETを提案する。 我々のモデルは、グラフベースとシーケンスベースニューラルネットワークを組み合わせて、プログラムグラフの局所的およびグローバル的コンテキストを捕捉する。 VELVETは、合成データと実世界のデータに対して、それぞれ99.6%と43.6%の精度を達成している。
  論文  参考訳（メタデータ） (2021-12-20T22:45:27Z)

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

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