論文の概要: Securing Cryptographic Software via Typed Assembly Language (Extended Version)

• arxiv url: http://arxiv.org/abs/2509.08727v1
• Date: Wed, 10 Sep 2025 16:17:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-11 15:16:52.499302
• Title: Securing Cryptographic Software via Typed Assembly Language (Extended Version)
• Title（参考訳）: 型付けアセンブリ言語による暗号化ソフトウェアのセキュア化(拡張バージョン)
• Authors: Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan,
• Abstract要約: 本稿では,アセンブリプログラムを書き換えて,シークレットと公開データをスタック上に分割するフレームワークSecSepを紹介する。 ソースコードのレベルからアセンブリの書き換えに移行することで、SecSepは以前の作業の制限に対処することができる。 私たちの方法論のキーとなる革新は、型付けアセンブリ言語(TAL)の新たな変種Octalです。
• 参考スコア（独自算出の注目度）: 3.394433117563263
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Authors of cryptographic software are well aware that their code should not leak secrets through its timing behavior, and, until 2018, they believed that following industry-standard constant-time coding guidelines was sufficient. However, the revelation of the Spectre family of speculative execution attacks injected new complexities. To block speculative attacks, prior work has proposed annotating the program's source code to mark secret data, with hardware using this information to decide when to speculate (i.e., when only public values are involved) or not (when secrets are in play). While these solutions are able to track secret information stored on the heap, they suffer from limitations that prevent them from correctly tracking secrets on the stack, at a cost in performance. This paper introduces SecSep, a transformation framework that rewrites assembly programs so that they partition secret and public data on the stack. By moving from the source-code level to assembly rewriting, SecSep is able to address limitations of prior work. The key challenge in performing this assembly rewriting stems from the loss of semantic information through the lengthy compilation process. The key innovation of our methodology is a new variant of typed assembly language (TAL), Octal, which allows us to address this challenge. Assembly rewriting is driven by compile-time inference within Octal. We apply our technique to cryptographic programs and demonstrate that it enables secure speculation efficiently, incurring a low average overhead of $1.2\%$.
• Abstract（参考訳）: 暗号ソフトウェアの著者たちは、自分たちのコードがタイミング行動を通じて秘密を漏らすべきではないことをよく認識しており、2018年までは、業界標準の定時コーディングガイドラインに従うだけで十分だと信じていた。 しかし、スペクター・ファミリーの投機的実行攻撃が暴露され、新たな複雑さがもたらされた。 投機的攻撃を阻止するために、事前の作業では、プログラムのソースコードに秘密データをマークするよう注釈付けすることを提案した。 これらのソリューションは、ヒープに格納された秘密情報を追跡できますが、パフォーマンス上のコストで、スタック上の秘密を正しく追跡できないような制限に悩まされます。 本稿では,アセンブリプログラムを書き換えて,シークレットと公開データをスタック上に分割する変換フレームワークSecSepを紹介する。 ソースコードのレベルからアセンブリの書き換えに移行することで、SecSepは以前の作業の制限に対処することができる。 このアセンブリ書き換えを行う上で重要な課題は、長いコンパイルプロセスを通じて意味情報が失われることにある。 私たちの方法論の重要な革新は、型付けアセンブリ言語(TAL)の新たな変種Octalです。 アセンブリの書き換えは、Octal内のコンパイル時の推論によって実行される。 この手法を暗号プログラムに適用し、セキュアな投機を可能にすることを実証し、平均的オーバーヘッドが1.2\%$であることを示す。

関連論文リスト

• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。 この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。 バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
  論文  参考訳（メタデータ） (2025-06-24T13:42:59Z)
• TFHE-Coder: Evaluating LLM-agentic Fully Homomorphic Encryption Code Generation [10.597643264309415]
  TFHE (Homomorphic Encryption over the Torus) は、復号化せずにデータを暗号化する。 マシンラーニングのプライバシ保護、セキュアなマルチパーティ計算、プライベートブロックチェーントランザクション、セキュアな医療診断といった可能性にもかかわらず、暗号化の複雑さとユーザビリティの問題により、その採用は制限されている。 この研究は、TFHEコード生成の最初のベンチマークを確立し、ドメイン固有のフィードバックで拡張されたLLMが、FHEコード生成の専門的ギャップを埋める方法を示している。
  論文  参考訳（メタデータ） (2025-03-15T17:57:44Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。 このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
  論文  参考訳（メタデータ） (2025-02-17T12:38:57Z)
• CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [56.019447113206006]
  大規模言語モデル(LLM)はコード生成において顕著な進歩を遂げた。 CodeIPは、新しいマルチビット透かし技術で、出所の詳細を保持するために追加情報を挿入する。 5つのプログラミング言語にまたがる実世界のデータセットで実施された実験は、CodeIPの有効性を実証している。
  論文  参考訳（メタデータ） (2024-04-24T04:25:04Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Securing Optimized Code Against Power Side Channels [1.589424114251205]
  セキュリティエンジニアは、コンパイラの最適化をオフにしたり、ローカルでコンパイル後の変換を実行することで、コードの効率を犠牲にすることが多い。 本稿では,最適化されたセキュアなコードを生成する制約ベースのコンパイラであるSecConCGを提案する。
  論文  参考訳（メタデータ） (2022-07-06T12:06:28Z)

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

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