論文の概要: Velosiraptor: Code Synthesis for Memory Translation
- arxiv url: http://arxiv.org/abs/2608.07966v1
- Date: Sat, 08 Aug 2026 07:01:59 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-11 19:16:36.589088
- Title: Velosiraptor: Code Synthesis for Memory Translation
- Title（参考訳）: Velosiraptor: メモリ変換のためのコード合成
- Abstract要約: Velosiraptorは、マシンのメモリハードウェアをプログラムする正しい低レベルOSコードを自動的に生成するシステムである。
本稿では,マシンのメモリハードウェアをプログラムする,正しい低レベルOSコードを自動的に生成するシステムであるVelosiraptorを提案する。
- 参考スコア（独自算出の注目度）: 1.1144160500749258
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Security is among the top concerns of operating system (OS) developers. A secure runtime environment relies on the OS to correctly configure the memory hardware on which it runs. This is mission-critical as it provides essential security-relevant features and abstractions that ensure the integrity and isolation of untrusted applications running alongside each other. Configuring a platform's memory hardware is not a one-off effort as designers constantly develop new mechanisms for translation and protection with different features and means of configuration. Adapting the OS code to the new hardware is not only a manual, repetitive and time consuming task, it may also introduce subtle, but security critical bugs that break security and isolation guarantees. We present Velosiraptor, a system that automatically generates correct, low-level OS code that programs the memory hardware of a machine. Velosiraptor leverages software synthesis techniques and exploits the domain specificity of the problem to make the synthesis process efficient. With Velosiraptor, developers write only a high-level description of the memory hardware's mapping behavior and OS environment. The Velosiraptor toolchain transforms this specification into a verified implementation that can be linked directly with the rest of the operating system. Incorporating the OS environment into this process allows porting an OS to new hardware platforms without worrying about writing code to configure the memory hardware. We can also use the same specification to generate hardware components. This enables research in new translation mechanisms, freeing up OS developers from manually writing OS code.
- Abstract（参考訳）: セキュリティはオペレーティングシステム(OS)開発者の最大の関心事のひとつだ。
セキュアなランタイム環境は、OSが実行するメモリハードウェアを正しく構成するためにOSに依存している。
これは重要なセキュリティ関連機能と抽象化を提供し、信頼できないアプリケーションが相互に動作することを保証するため、ミッションクリティカルなことです。
プラットフォームのメモリハードウェアの設定は、デザイナが常に異なる機能と構成手段を備えた翻訳と保護のための新しいメカニズムを開発するため、ワンオフの作業ではない。
OSコードを新しいハードウェアに適応させることは、手動、繰り返し、そして時間のかかるタスクであるだけでなく、セキュリティとアイソレーションの保証を破る、微妙な、しかしセキュリティクリティカルなバグも導入するかもしれない。
本稿では,マシンのメモリハードウェアをプログラムする,正しい低レベルOSコードを自動的に生成するシステムであるVelosiraptorを提案する。
ヴェロシラプターはソフトウェア合成技術を活用し、問題の領域特異性を利用して合成プロセスを効率化する。
Velosiraptorを使えば、開発者はメモリハードウェアのマッピング動作とOS環境の高レベルな記述のみを書くことができる。
Velosiraptorツールチェーンは、この仕様を、オペレーティングシステムの他の部分と直接リンクできる検証済みの実装に変換する。
このプロセスにOS環境を組み込むことで、新しいハードウェアプラットフォームにOSを移植することができる。
同じ仕様を使ってハードウェアコンポーネントを生成することもできます。
これにより、新しい翻訳メカニズムの研究が可能になり、OS開発者が手動でOSコードを書けなくなる。
関連論文リスト
- PREPING: Building Agent Memory without Tasks [65.75870568959644]
Prepingはプロポーザル誘導型メモリ構築フレームワークである。
コアとなるのは、将来の実践を形作る構造化制御状態であるプロジェクタメモリである。
トライアルでは、Prepingはメモリなしのベースラインよりも大幅に改善されている。
論文 参考訳（メタデータ） (2026-05-11T04:34:43Z) - Trust Nothing: RTOS Security without Run-Time Software TCB (Extended Version) [3.6676516275835165]
本稿では、悪意のあるデバイスに対して保護された信頼できないオペレーティングシステムを構築するのに適したトークン機能アプローチを提案する。
本稿では,実行時ソフトウェアTCBを持たないZephyrをベースとしたソフトリアルタイムオペレーティングシステムを提案する。
私たちの仕事は、明日のセキュリティクリティカルな組み込みデバイスにおいて、より厳格なセキュリティバイデザインのための基盤を提供します。
論文 参考訳（メタデータ） (2026-03-09T13:59:27Z) - Sockeye: a language for analyzing hardware documentation [0.2142042364864257]
ハードウェアのセマンティクス、ソフトウェア動作に関する仮定、および所望のセキュリティ特性を記述するためのドメイン固有言語を導入する。
次に、参照マニュアルから8つのSystem-on-Chipsの多様なセットのマシン仕様を作成します。
論文 参考訳（メタデータ） (2025-10-31T14:04:01Z) - TECS/Rust: Memory-safe Component Framework for Embedded Systems [0.0]
本稿では,組み込みシステム用に設計されたRustベースのフレームワークであるTECS/Rustを提案する。
Rustのコンパイル時メモリセーフな機能である、ライフタイムや借用といった機能を活用して、Cと共通するメモリ脆弱性を軽減する。
提案されたフレームワークはメモリ安全性を保証するだけでなく、CBDの柔軟性も維持し、CBDコンポーネント用のRustコード生成を自動化するとともに、リアルタイムオペレーティングシステムとの効率的な統合をサポートする。
論文 参考訳（メタデータ） (2025-10-29T08:28:48Z) - Dynamic Vulnerability Patching for Heterogeneous Embedded Systems Using Stack Frame Reconstruction [10.905694063940425]
既存の動的脆弱性パッチ技術は組み込みデバイスには適していない。
スタックフレーム再構築に基づくパッチ開発を容易にするStackPatchというホットパッチフレームワークを提案する。
ARM、RISC-V、Xtensaの3つの主要なマイクロコントローラ(MCU)アーキテクチャを備えた組み込みデバイス上でStackPatchをテストしました。
論文 参考訳（メタデータ） (2025-09-12T13:00:45Z) - Securing Cryptographic Software via Typed Assembly Language (Extended Version) [3.394433117563263]
本稿では,アセンブリプログラムを書き換えて,シークレットと公開データをスタック上に分割するフレームワークSecSepを紹介する。
ソースコードのレベルからアセンブリの書き換えに移行することで、SecSepは以前の作業の制限に対処することができる。
私たちの方法論のキーとなる革新は、型付けアセンブリ言語(TAL)の新たな変種Octalです。
論文 参考訳（メタデータ） (2025-09-10T16:17:31Z) - Detecting Hardware Trojans in Microprocessors via Hardware Error Correction Code-based Modules [49.1574468325115]
ハードウェアトロイの木馬(HT)は、攻撃者が無許可のソフトウェアを実行したり、特権操作に不正にアクセスしたりすることができる。
RISC-Vマイクロプロセッサ上のエラー訂正符号(ECC)を用いて,ランタイムHTアクティベーションを検出するハードウェアベースの手法を紹介する。
論文 参考訳（メタデータ） (2025-06-18T12:37:14Z) - ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。
我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
論文 参考訳（メタデータ） (2025-06-09T17:10:47Z) - CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。
我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。
最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
論文 参考訳（メタデータ） (2025-04-21T17:33:33Z) - Extending Lifetime of Embedded Systems by WebAssembly-based Functional Extensions Including Drivers [46.538276603099916]
WebAssembly(Wasm)コンテナ内の周辺I/O操作を容易にするために設計されたフレームワークであるWasm-IOを紹介する。
プラットフォームに依存しない周辺構成をWasmバイナリ内に埋め込むための同期I/Oと手法について詳述する。
論文 参考訳（メタデータ） (2025-03-10T17:22:00Z) - L2MAC: Large Language Model Automatic Computer for Extensive Code Generation [52.81694565226513]
トランスフォーマーベースの大規模言語モデル(LLM)は、基盤となるトランスフォーマーアーキテクチャの固定コンテキストウィンドウによって制約される。
本稿では,L2MACを提案する。L2MACは,LLMをベースとした汎用型自動計算機(von Neumann Architecture)フレームワークで,長期的かつ一貫した出力生成を実現する。
論文 参考訳（メタデータ） (2023-10-02T16:55:19Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory [8.414722884952525]
緩和マイクロアーキテクチャ分離(RMI)と呼ばれる新しいセキュリティ機能を導入する。
RMIは、攻撃者とメモリを共有できない機密プログラムを許可し、情報漏洩を非投機的実行に制限する。
エンドツーエンドのプロトタイプであるCitadelは、Linuxをブートしてセキュアなアプリケーションを実行するFPGAベースのマルチコアプロセッサで構成されています。
論文 参考訳（メタデータ） (2023-06-26T17:51:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。