論文の概要: DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification

• arxiv url: http://arxiv.org/abs/2604.16832v1
• Date: Sat, 18 Apr 2026 04:47:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 13:55:23.73032
• Title: DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification
• Title（参考訳）: DALC-CT:一定時間検証のための低レベルコードトレースの動的解析
• Authors: Nges Brian Njungle, Edwin P. Kayang, Mishel J. Paul, Michel A. Kinsy,
• Abstract要約: 低レベルの実行トレースの動的解析に基づく定数時間プログラムの検証手法を提案する。 我々は,DALC-CTというオープンソースのツールを開発し,この手法を用いてプログラムの一定時間検証を行った。
• 参考スコア（独自算出の注目度）: 0.08749675983608168
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Timing side-channel attacks exploit variations in program execution time to recover sensitive information. Cryptographic implementations are especially vulnerable to these attacks, since even small timing differences in operations such as modular exponentiation or key comparisons can be exploited to extract highly sensitive information, such as secret keys. To mitigate this threat, implementations of programs that handle sensitive information are often expected to adhere to constant-time principles, ensuring that execution behavior does not depend on secret inputs. However, validating the constant-time property of programs remains a major challenge in cryptography development. Formal method approaches to verify constant-time implementations rely on abstractions that often fail to capture real execution behavior, while timing-based measurement techniques are highly sensitive to noise from other programs and even hardware environments. In this work, we propose a novel approach for verifying constant-time programs based on dynamic analysis of low-level execution traces. Our method measures instruction sequences across multiple input values for any given binary and targeted function. Any variations in the instruction mix distribution for any given pair of traces indicate a deviation from the constant-time principle and behavior. We developed an open-source tool called DALC-CT, for the constant-time verification of programs using this approach. We evaluated it on a set of well-known constant-time and non-constant-time examples, achieving a perfect detection of issues. Our results demonstrate that analyzing the logical execution of programs via instruction trace comparisons provides a lightweight and reliable way to verify the constant-time property of programs.
• Abstract（参考訳）: タイミングサイドチャネル攻撃は、プログラムの実行時間の変化を利用して機密情報を回復する。 暗号の実装は特にこれらの攻撃に対して脆弱であり、モジュラー指数やキー比較のような操作のタイミングの違いさえも、秘密鍵のような非常に機密性の高い情報を抽出するために利用することができる。 この脅威を軽減するため、センシティブな情報を扱うプログラムの実装は、しばしば一定時間の原則に従うことが期待され、実行動作が秘密の入力に依存しないことを保証する。 しかし、プログラムの一定時間特性を検証することは、暗号開発において大きな課題である。 定時実装を検証するための形式的手法は、実際の実行動作を捉えるのにしばしば失敗する抽象化に依存するが、タイミングに基づく計測技術は他のプログラムやハードウェア環境からのノイズに非常に敏感である。 本研究では,低レベルの実行トレースの動的解析に基づく定数時間プログラムの検証手法を提案する。 提案手法は,任意のバイナリおよびターゲット関数に対して,複数の入力値にまたがる命令列を測定する。 任意の一対のトレースに対する命令混合分布の任意のバリエーションは、定数時間原理と振る舞いから逸脱していることを示す。 我々は,DALC-CTというオープンソースのツールを開発し,この手法を用いてプログラムの一定時間検証を行った。 我々は、よく知られた定時および非定時例のセットで評価し、問題の完全な検出を実現した。 提案手法は,命令トレース比較によるプログラムの論理的実行を解析することにより,プログラムの一定時間特性を検証する軽量で信頼性の高い方法であることを示す。

関連論文リスト

• QUACK! Making the (Rubber) Ducky Talk: A Systematic Study of Keystroke Dynamics for HID Injection Detection [60.105690843777666]
  我々は、タイミング機能のみで動作する軽量モデルを使用して、堅牢でプライバシー保護の検知が達成可能であることを示す。 分析の結果,攻撃者の高度化は単調に回避を改善できないことが明らかとなった。
  論文  参考訳（メタデータ） (2026-04-17T08:53:24Z)
• AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
  我々はAgentProcessBenchを紹介した。AgentProcessBenchは、現実的なツール拡張トラジェクトリにおけるステップレベルの有効性を評価するための最初のベンチマークである。 ベンチマークは、1,000の多様な軌跡と8,509の人間ラベル付きステップアノテーションと89.1%のアノテーション間合意で構成されている。 探索をキャプチャする3つのラベリングスキームと、ラベルのあいまいさを減らすためのエラー伝搬ルールを備えている。
  論文  参考訳（メタデータ） (2026-03-15T16:13:58Z)
• Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
  ビデオにおけるリアルタイムのオンラインオブジェクト追跡は、コンピュータビジョンにおける中核的なタスクである。 本稿では,物体追跡を逐次的仮説テストとして解釈することを提案する。 本研究では,地中追跡情報と内部追跡情報の両方を活用することにより,教師なしと教師なしの両方の変種を提案する。
  論文  参考訳（メタデータ） (2026-02-13T14:57:15Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  言語モデルの生成能力をプロセス検証器と組み合わせたテストタイムアルゴリズムは、新しい推論能力を引き出すための有望なレバーを提供する。 提案手法は, 理論的に根拠付きバックトラックを用いて, 検証誤差に対して, 確実な堅牢性を実現するための新しいプロセス誘導型テスト時間サンプリングアルゴリズムであるVGBを導入する。
  論文  参考訳（メタデータ） (2025-10-03T16:21:14Z)
• Systematic Timing Leakage Analysis of NIST PQDSS Candidates: Tooling and Lessons Learned [2.4508658326953108]
  我々は、広く使われている定時分析ツールの構成、実行、結果分析を自動化するツールチェーンを開発した。 合計26の問題を各開発者に報告し、そのうち5つはすでに修正済みです。
  論文  参考訳（メタデータ） (2025-09-04T08:41:06Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• CodeFlow: Program Behavior Prediction with Dynamic Dependencies Learning [11.347234752942684]
  CodeFlowは、コードカバレッジを予測し、実行時のエラーを検出する、新しい機械学習ベースのアプローチである。 CodeFlowは、実行可能なすべての実行パスと、異なるステートメント間の統計関係を効果的に表現します。 私たちの経験的評価は、CodeFlowがコードカバレッジ予測の精度を大幅に改善し、実行時のエラーを効果的にローカライズできることを示しています。
  論文  参考訳（メタデータ） (2024-08-05T20:32:00Z)
• Cassandra: Efficient Enforcement of Sequential Execution for Cryptographic Programs (Extended Version) [3.34371579019566]
  定時プログラミングは、サイドチャネル攻撃に対する暗号プログラムを強化するための広くデプロイされたアプローチである。 現代のプロセッサは、プログラムの意図しないパスを過渡的に実行することで、標準の定時ポリシーの前提に反することが多い。 我々は,一定時間暗号コードのシーケンシャル実行を強制する新しいハードウェア/ソフトウェア機構であるCassandraを提案する。
  論文  参考訳（メタデータ） (2024-06-06T17:34:48Z)
• Towards Efficient Verification of Constant-Time Cryptographic Implementations [5.433710892250037]
  一定時間プログラミングの規律は、タイミングサイドチャネル攻撃に対する効果的なソフトウェアベースの対策である。 本研究では, テナント解析の新たな相乗効果と自己構成プログラムの安全性検証に基づく実用的検証手法を提案する。 当社のアプローチはクロスプラットフォームで完全に自動化されたCT-Proverとして実装されている。
  論文  参考訳（メタデータ） (2024-02-21T03:39:14Z)
• Execution Time Program Verification With Tight Bounds [6.36836017515443]
  本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。 3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。 証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
  論文  参考訳（メタデータ） (2022-10-20T09:02:13Z)
• Change Point Detection in Time Series Data using Autoencoders with a Time-Invariant Representation [69.34035527763916]
  変化点検出(CPD)は、時系列データにおける急激な特性変化を見つけることを目的としている。 近年のCDD法は、深層学習技術を用いる可能性を示したが、信号の自己相関統計学におけるより微妙な変化を識別する能力に欠けることが多い。 我々は、新しい損失関数を持つオートエンコーダに基づく手法を用い、使用済みオートエンコーダは、CDDに適した部分的な時間不変表現を学習する。
  論文  参考訳（メタデータ） (2020-08-21T15:03:21Z)

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

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