論文の概要: Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond
- arxiv url: http://arxiv.org/abs/2311.14246v1
- Date: Fri, 24 Nov 2023 01:38:19 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-25 13:16:38.659801
- Title: Constant-Time Wasmtime, for Real This Time: End-to-End Verified Zero-Overhead Constant-Time Programming for the Web and Beyond
- Title（参考訳）: リアルタイムの定時待ち時間: エンドツーエンドで検証されたWeb向けゼロオーバーヘッドの定時プログラミング
- Authors: Garrett Gu, Hovav Shacham,
- Abstract要約: 本稿ではJITスタイルのWasmtimeをベースとした新しいコンパイラ検証スイートを提案する。
また、ct-wasmをターゲットに、既存の定時対応DSLである FaCT のポートも提示する。
- 参考スコア（独自算出の注目度）: 2.803675461772196
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We claim that existing techniques and tools for generating and verifying constant-time code are incomplete, since they rely on assumptions that compiler optimization passes do not break constant-timeness or that certain operations execute in constant time on the hardware. We present the first end-to-end constant-time-aware compilation process that preserves constant-time semantics at every step from a high-level language down to microarchitectural guarantees, provided by the forthcoming ARM PSTATE.DIT feature. First, we present a new compiler-verifier suite based on the JIT-style runtime Wasmtime, modified to compile ct-wasm, a preexisting type-safe constant-time extension of WebAssembly, into ARM machine code while maintaining the constant-time property throughout all optimization passes. The resulting machine code is then fed into an automated verifier that requires no human intervention and uses static dataflow analysis in Ghidra to check the constant-timeness of the output. Our verifier leverages characteristics unique to ct-wasm-generated code in order to speed up verification while preserving both soundness and wide applicability. We also consider the resistance of our compilation and verification against speculative timing leakages such as Spectre. Finally, in order to expose ct-Wasmtime at a high level, we present a port of FaCT, a preexisting constant-time-aware DSL, to target ct-wasm.
- Abstract（参考訳）: コンパイラの最適化が一定時間を経過しても、一定の操作がハードウェア上で一定時間実行されないという仮定に依存しているため、定数時間コードの生成と検証のための既存の技術やツールが不完全である、と我々は主張する。
ARM PSTATE.DIT機能によって提供される,ハイレベル言語からマイクロアーキテクチャ保証まで,各ステップにおける定時セマンティクスを保存する最初のエンドツーエンドの定数時間対応コンパイルプロセスを提案する。
まず、JITスタイルのランタイムをベースとした新しいコンパイラ検証スイートであるWasmtimeを、WebAssemblyの型セーフな定数時間拡張であるct-wasmを、すべての最適化パスを通じて定数プロパティを維持しながらARMマシンコードにコンパイルするように修正した。
結果のマシンコードは、人間の介入を必要としない自動検証器に入力され、Ghidraの静的データフロー分析を使用して出力の一定時間をチェックする。
本検証では,音質と適用性の両方を保ちながら検証を高速化するために,ct-wasm生成符号に特有の特性を利用する。
また、Spectreのような投機的タイミングリークに対するコンパイルと検証の抵抗についても検討する。
最後に、ct-Wasmtimeを高いレベルで公開するために、既存の定時対応DSLである FaCT を ct-wasm に移植する。
関連論文リスト
- Towards Efficient Verification of Constant-Time Cryptographic
Implementations [5.433710892250037]
一定時間プログラミングの規律は、タイミングサイドチャネル攻撃に対する効果的なソフトウェアベースの対策である。
本研究では, テナント解析の新たな相乗効果と自己構成プログラムの安全性検証に基づく実用的検証手法を提案する。
当社のアプローチはクロスプラットフォームで完全に自動化されたCT-Proverとして実装されている。
論文 参考訳（メタデータ） (2024-02-21T03:39:14Z) - AutoTimes: Autoregressive Time Series Forecasters via Large Language
Models [72.77653698874678]
本稿では,大規模言語モデル(LLM)を自動回帰時系列予測器として活用するためにAutoTimesを提案する。
提案手法は, LLM, 追加テキスト, 時系列を命令として利用することにより, 顕著な手法の一般化を実現し, 性能の向上を実現している。
論文 参考訳（メタデータ） (2024-02-04T06:59:21Z) - Defining and executing temporal constraints for evaluating engineering
artifact compliance [56.08728135126139]
プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。
これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。
関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
論文 参考訳（メタデータ） (2023-12-20T13:26:31Z) - DECLASSIFLOW: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security Measures (Full Version) [9.816078445230305]
投機的実行攻撃は、定数時間プログラミングのセキュリティを損なう。
本稿では,提案するDECLASSIFLOWを用いて,投機的漏洩から一定時間コードを効率よく保護する。
論文 参考訳（メタデータ） (2023-12-14T21:00:20Z) - Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed
Automata [2.2003515924552044]
タイムオートマトン(Timed Automatica)は、有限状態オートマトンの拡張であり、一連のクロックが線形に進化する。
我々は、タイムドオートマトンを入力形式として使用し、攻撃者がシステム実行時間のみにアクセス可能であると仮定する。
論文 参考訳（メタデータ） (2023-10-31T12:10:35Z) - Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
重み付き時間遅延フィードバック機構を備えた新しいゲートリカレントユニット(GRU)を導入する。
我々は、$tau$-GRUが、最先端のリカレントユニットやゲート型リカレントアーキテクチャよりも早く収束し、より一般化できることを示します。
論文 参考訳（メタデータ） (2022-12-01T02:26:34Z) - Securing Optimized Code Against Power Side Channels [1.589424114251205]
セキュリティエンジニアは、コンパイラの最適化をオフにしたり、ローカルでコンパイル後の変換を実行することで、コードの効率を犠牲にすることが多い。
本稿では,最適化されたセキュアなコードを生成する制約ベースのコンパイラであるSecConCGを提案する。
論文 参考訳（メタデータ） (2022-07-06T12:06:28Z) - Distortion-Aware Network Pruning and Feature Reuse for Real-time Video
Segmentation [49.17930380106643]
本稿では,リアルタイム視覚タスクのスキップ接続によるアーキテクチャの高速化を目的とした新しいフレームワークを提案する。
具体的には、各フレームの到着時に、前のフレームから特徴を変換し、特定の空間的ビンで再利用する。
次に、現在のフレームの領域におけるバックボーンネットワークの部分計算を行い、現在のフレームと前のフレームの時間差をキャプチャする。
論文 参考訳（メタデータ） (2022-06-20T07:20:02Z) - MAPLE-Edge: A Runtime Latency Predictor for Edge Devices [80.01591186546793]
汎用ハードウェアの最先端遅延予測器であるMAPLEのエッジデバイス指向拡張であるMAPLE-Edgeを提案する。
MAPLEと比較して、MAPLE-Edgeはより小さなCPUパフォーマンスカウンタを使用して、ランタイムとターゲットデバイスプラットフォームを記述することができる。
また、共通ランタイムを共有するデバイスプール上でトレーニングを行うMAPLEとは異なり、MAPLE-Edgeは実行時に効果的に一般化できることを示す。
論文 参考訳（メタデータ） (2022-04-27T14:00:48Z) - Lightweight Jet Reconstruction and Identification as an Object Detection
Task [5.071565475111431]
我々は、CERN大型ハドロン衝突型加速器で遭遇したジェットのエンド・ツー・エンドの識別と再構築作業に畳み込み技術を適用した。
PFJet-SSDは、クラスタジェットへの同時ローカライゼーション、分類、回帰タスクを実行し、特徴を再構築する。
3次ネットワークは、その完全精度の等価な性能と密に一致し、最先端のルールベースアルゴリズムより優れていることを示す。
論文 参考訳（メタデータ） (2022-02-09T15:01:53Z) - Towards Streaming Perception [70.68520310095155]
本稿では、リアルタイムオンライン知覚のための単一のメトリクスにレイテンシと精度を協調的に統合するアプローチを提案する。
この指標の背後にある重要な洞察は、瞬間ごとに認識スタック全体の出力を共同で評価することである。
本稿では,都市ビデオストリームにおけるオブジェクト検出とインスタンスセグメンテーションの具体的タスクに注目し,高品質で時間依存的なアノテーションを備えた新しいデータセットを寄贈する。
論文 参考訳（メタデータ） (2020-05-21T01:51:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。