論文の概要: Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata

• arxiv url: http://arxiv.org/abs/2310.20392v1
• Date: Tue, 31 Oct 2023 12:10:35 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-01 15:19:26.202703
• Title: Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
• Title（参考訳）: 時間型オートマトンにおける実行時間不透明性を確保するためのタイミングパラメータの設定
• Authors: \'Etienne Andr\'e (Universit\'e Sorbonne Paris Nord, LIPN, CNRS, Villetaneuse, France), Engel Lefaucheux (Universit\'e de Lorraine, CNRS, Inria, LORIA, Nancy, France), Didier Lime (Nantes Universit\'e, \'Ecole Centrale Nantes, CNRS, LS2N, Nantes, France), Dylan Marinho (Universit\'e de Lorraine, CNRS, Inria, LORIA, Nancy, France), Jun Sun (School of Computing and Information Systems, Singapore Management University, Singapore)
• Abstract要約: タイムオートマトン(Timed Automatica)は、有限状態オートマトンの拡張であり、一連のクロックが線形に進化する。 我々は、タイムドオートマトンを入力形式として使用し、攻撃者がシステム実行時間のみにアクセス可能であると仮定する。
• 参考スコア（独自算出の注目度）: 2.2003515924552044
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with a set of clocks evolving linearly and that can be tested or reset, making this formalism able to reason on systems involving concurrency and timing constraints. In this paper, we summarize a recent line of works using timed automata as the input formalism, in which we assume that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed system modeled by a timed automaton, given a secret location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the secret location was visited. This means that for any such execution time, the system is opaque: either the final location is not reachable, or it is reachable with that execution time for both a run visiting and a run not visiting the secret location. We also address the full execution-time opacity problem, asking whether the system is opaque for all execution times; we also study a weak counterpart. Second, we add timing parameters, which are a way to configure a system: we identify a subclass of parametric timed automata with some decidability results. In addition, we devise a semi-algorithm for synthesizing timing parameter valuations guaranteeing that the resulting system is opaque. Third, we report on problems when the secret has itself an expiration date, thus defining expiring execution-time opacity problems. We finally show that our method can also apply to program analysis with configurable internal timings.
• Abstract（参考訳）: タイミング情報漏洩は、攻撃者がタイムスタンプのあるイベントなどのタイムスタンプ情報を観察して機密内部情報を引き出すと発生する。 タイムドオートマトン(Timed Automatica)は、有限状態オートマトンの拡張であり、一連のクロックが線形に進化し、テストやリセットが可能である。 本稿では,timed automataを入力形式として使用し,攻撃者がシステム実行時間に対して(のみ)アクセス可能と仮定した最近の成果を要約する。 まず、タイムドオートマトンでモデル化されたタイムドシステムは、秘密の場所と最終位置を与えられた場合、その実行時間を初期位置から最終位置まで合成し、秘密の場所が訪れたかどうかを推定できない。 つまり、最終的な位置が到達できないか、あるいは、実行時と、秘密の場所を訪問していないランの両方で到達可能である、というような実行時間に対して、システムは不透明である。 また,全実行時間不透明性問題にも対処し,すべての実行時間に対してシステムが不透明であるかどうかを問う。 第2に、システムを構成するためのタイミングパラメータを追加し、決定可能性のあるパラメトリックタイムドオートマタのサブクラスを特定します。 さらに,結果が不透明であることを保証したタイミングパラメータ評価を合成するための半アルゴリズムを考案した。 第3に,シークレットが有効期限を持つ場合の問題点を報告し,実行時の不透明性問題を定義する。 提案手法は,構成可能な内部タイミングでプログラム解析にも適用可能であることを示す。

関連論文リスト

• Execution-time opacity control for timed automata [0.0]
  タイムドオートマトンにおけるタイミングリークは、攻撃者がタイムドビヘイビアを観察して秘密を推論できるときに起こりうる。 実行時の不透明さにおいて、攻撃者は実行時間だけを観察して、プライベートな場所が訪れたかどうかを推定することを目的としている。 TAが実行時に制御可能かどうかを判断して不透明性を確保することができることを示す。
  論文  参考訳（メタデータ） (2024-09-16T14:46:52Z)
• A Framework for Differential Privacy Against Timing Attacks [0.0]
  我々は、タイミング側チャネルの存在下での差分プライバシーを確保するための一般的な枠組みを確立する。 タイミングプライバシという新たな概念を定義し、敵に異なるプライベートなプログラムをキャプチャする。 私たちは、OpenDP Programming Frameworkの自然な拡張を通じて、私たちのフレームワークをコードでどのように実現できるかを示します。
  論文  参考訳（メタデータ） (2024-09-09T13:56:04Z)
• Expiring opacity problems in parametric timed automata [0.0]
  タイムドオートマトンにおける期限付き不透明度問題について検討した。 我々は,システムが不透明な時間境界の集合を考察し,時間付きオートマトンに対して有効に計算できることを示す。
  論文  参考訳（メタデータ） (2024-03-12T13:30:53Z)
• Tooling Offline Runtime Verification against Interaction Models : recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
  オフライン実行時の検証には、仕様に対するシステムの実行の静的解析が含まれる。 分散システムでは、グローバルクロックが存在しないため、グローバルトレースの形での実行を特徴付けることは一般的に不可能である。 本稿では,インタラクションと呼ばれる形式仕様に対して,そのようなトレースの適合性を検証するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-03-05T16:09:55Z)
• RelayAttention for Efficient Large Language Model Serving with Long System Prompts [59.50256661158862]
  本稿では,長いシステムプロンプトを含むLCMサービスの効率を向上させることを目的とする。 これらのシステムプロンプトの処理には、既存の因果注意アルゴリズムにおいて、大量のメモリアクセスが必要である。 本稿では,DRAMから入力トークンのバッチに対して,DRAMから隠れた状態を正確に1回読み取ることのできるアテンションアルゴリズムであるRelayAttentionを提案する。
  論文  参考訳（メタデータ） (2024-02-22T18:58:28Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。 これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。 関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
  論文  参考訳（メタデータ） (2023-12-20T13:26:31Z)
• Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond [2.803675461772196]
  本稿ではJITスタイルのWasmtimeをベースとした新しいコンパイラ検証スイートを提案する。 また、ct-wasmをターゲットに、既存の定時対応DSLである FaCT のポートも提示する。
  論文  参考訳（メタデータ） (2023-11-24T01:38:19Z)
• Better than the Best: Gradient-based Improper Reinforcement Learning for Network Scheduling [60.48359567964899]
  パケット遅延を最小限に抑えるため,制約付き待ち行列ネットワークにおけるスケジューリングの問題を考える。 我々は、利用可能な原子ポリシーよりも優れたスケジューラを生成するポリシー勾配に基づく強化学習アルゴリズムを使用する。
  論文  参考訳（メタデータ） (2021-05-01T10:18:34Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。 ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。 サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
  論文  参考訳（メタデータ） (2020-09-08T16:42:55Z)
• Towards Streaming Perception [70.68520310095155]
  本稿では、リアルタイムオンライン知覚のための単一のメトリクスにレイテンシと精度を協調的に統合するアプローチを提案する。 この指標の背後にある重要な洞察は、瞬間ごとに認識スタック全体の出力を共同で評価することである。 本稿では,都市ビデオストリームにおけるオブジェクト検出とインスタンスセグメンテーションの具体的タスクに注目し,高品質で時間依存的なアノテーションを備えた新しいデータセットを寄贈する。
  論文  参考訳（メタデータ） (2020-05-21T01:51:35Z)
• Time-varying Gaussian Process Bandit Optimization with Non-constant Evaluation Time [93.6788993843846]
  非定常評価時間を効果的に処理できる新しい時間変化ベイズ最適化アルゴリズムを提案する。 我々の限界は、評価時間列のパターンが問題の難易度に大きな影響を与えることを決定づける。
  論文  参考訳（メタデータ） (2020-03-10T13:28:33Z)

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

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