論文の概要: 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)の新たな脆弱性を特定し、最先端ツールを大幅に上回っている。
関連論文リスト
- An Extensive Comparison of Static Application Security Testing Tools [1.3927943269211593]
静的アプリケーションセキュリティテストツール(SASTT)は、ソフトウェアアプリケーションのセキュリティと信頼性をサポートするソフトウェア脆弱性を特定する。
いくつかの研究は、偽アラームを発生させる傾向があるため、代替ソリューションがSASTTよりも効果的である可能性を示唆している。
SASTTの評価は、制御されているが合成されたJavaに基づいています。
論文 参考訳(メタデータ) (2024-03-14T09:37:54Z) - Patch2QL: Discover Cognate Defects in Open Source Software Supply Chain
With Auto-generated Static Analysis Rules [1.9591497166224197]
本稿では,SASTルールの自動生成によるOSSのコグネート欠陥の検出手法を提案する。
具体的には、プリパッチバージョンとポストパッチバージョンから重要な構文と意味情報を抽出する。
我々はPatch2QLというプロトタイプツールを実装し、それをC/C++の基本OSSに適用した。
論文 参考訳(メタデータ) (2024-01-23T02:23:11Z) - Utilization of machine learning for the detection of self-admitted
vulnerabilities [0.0]
技術的負債(Technical debt)とは、短期的なニーズのために導入された、不公平なコードを記述するメタファーである。
開発者はそれを意識し、ソースコードのコメントで認めている。
論文 参考訳(メタデータ) (2023-09-27T12:38:12Z) - The Adversarial Implications of Variable-Time Inference [47.44631666803983]
本稿では,攻撃対象のMLモデルの予測を後処理するアルゴリズムの実行時間を簡単に計測する,新たなサイドチャネルを利用するアプローチを提案する。
我々は,物体検出装置の動作において重要な役割を果たす非最大抑圧(NMS)アルゴリズムからの漏れを調査する。
我々は、YOLOv3検出器に対する攻撃を実演し、タイミングリークを利用して、逆例を用いてオブジェクト検出を回避し、データセット推論を行う。
論文 参考訳(メタデータ) (2023-09-05T11:53:17Z) - 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) - SecureFalcon: The Next Cyber Reasoning System for Cyber Security [1.0700114817489723]
本稿では,FalconLLM上に構築された革新的なモデルアーキテクチャであるSecureFalconを紹介する。
SecureFalconは、脆弱性のあるCコードのサンプルと非脆弱性なCコードのサンプルを区別するように訓練されている。
我々は、その性能を評価するために、生成人工知能(AI)によって構築された新しいトレーニングデータセット、FormAIを構築した。
論文 参考訳(メタデータ) (2023-07-13T08:34:09Z) - 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) - Software Vulnerability Detection via Deep Learning over Disaggregated
Code Graph Representation [57.92972327649165]
この研究は、コードコーパスから安全でないパターンを自動的に学習するためのディープラーニングアプローチを探求する。
コードには解析を伴うグラフ構造が自然に認められるため,プログラムの意味的文脈と構造的規則性の両方を利用する新しいグラフニューラルネットワーク(GNN)を開発する。
論文 参考訳(メタデータ) (2021-09-07T21:24:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。