Velosiraptor: Code Synthesis for Memory Translation

• URL: http://arxiv.org/abs/2608.07966v1
• Date: Sat, 08 Aug 2026 07:01:59 GMT
• Title: Velosiraptor: Code Synthesis for Memory Translation
• Abstract summary: Velosiraptor is a system that automatically generates correct, low-level OS code that programs the memory hardware of a machine.<n>We present Velosiraptor, a system that automatically generates correct, low-level OS code that programs the memory hardware of a machine.
• Score: 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.

Related papers

• PREPING: Building Agent Memory without Tasks [65.75870568959644]
  Preping is a proposer-guided memory construction framework.<n>At its core is proposer memory, a structured control state that shapes future practice.<n>Trials show Preping substantially improves over a no-memory baseline.
  arXiv  Detail & Related papers  (2026-05-11T04:34:43Z)
• Trust Nothing: RTOS Security without Run-Time Software TCB (Extended Version) [3.6676516275835165]
  We present a token capability approach suitable for building an untrusted operating system with protection against malicious devices.<n>We present a soft real-time operating system based on Zephyr that has no run-time software TCB.<n>Our work offers a foundation for more rigorous security-by-design in tomorrow's security-critical embedded devices.
  arXiv  Detail & Related papers  (2026-03-09T13:59:27Z)
• Sockeye: a language for analyzing hardware documentation [0.2142042364864257]
  We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties.<n>We then create machine-specified specifications for a diverse set of eight System-on-Chips from their reference manuals.
  arXiv  Detail & Related papers  (2025-10-31T14:04:01Z)
• TECS/Rust: Memory-safe Component Framework for Embedded Systems [0.0]
  This paper proposes TECS/Rust, a Rust-based framework specifically designed for embedded systems.<n>It leverages Rust's compile-time memory-safe features, such as lifetime and borrowing, to mitigate memory vulnerabilities common with C.<n>The proposed framework not only ensures memory safety but also maintains the flexibility of CBD, automates Rust code generation for CBD components, and supports efficient integration with real-time operating systems.
  arXiv  Detail & Related papers  (2025-10-29T08:28:48Z)
• Dynamic Vulnerability Patching for Heterogeneous Embedded Systems Using Stack Frame Reconstruction [10.905694063940425]
  Existing dynamic vulnerability patching techniques are not well-suited for embedded devices.<n>We propose a hot patching framework called StackPatch that facilitates patch development based on stack frame reconstruction.<n>We tested StackPatch on embedded devices featuring three major microcontroller (MCU) architectures: ARM, RISC-V, and Xtensa.
  arXiv  Detail & Related papers  (2025-09-12T13:00:45Z)
• Securing Cryptographic Software via Typed Assembly Language (Extended Version) [3.394433117563263]
  This paper introduces SecSep, a framework that rewrites assembly programs so that they partition secret and public data on the stack.<n>By moving from the source-code level to assembly rewriting, SecSep is able to address limitations of prior work.<n>Key innovation of our methodology is a new variant of typed assembly language (TAL), Octal, which allows us to address this challenge.
  arXiv  Detail & Related papers  (2025-09-10T16:17:31Z)
• Detecting Hardware Trojans in Microprocessors via Hardware Error Correction Code-based Modules [49.1574468325115]
  Hardware Trojans (HTs) enable attackers to execute unauthorized software or gain illicit access to privileged operations.<n>This manuscript introduces a hardware-based methodology for detecting runtime HT activations using Error Correction Codes (ECCs) on a RISC-V microprocessor.
  arXiv  Detail & Related papers  (2025-06-18T12:37:14Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  We introduce ProtocolLLM, the first benchmark suite specifically targeting widely used SystemVerilog protocols.<n>We observe that most of the models fail to generate SystemVerilog code for communication protocols that follow timing constrains.
  arXiv  Detail & Related papers  (2025-06-09T17:10:47Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• Extending Lifetime of Embedded Systems by WebAssembly-based Functional Extensions Including Drivers [46.538276603099916]
  We present Wasm-IO, a framework designed to facilitate peripheral I/O operations within WebAssembly (Wasm) containers.<n>We detail synchronous I/O and methods for embedding platform-independent peripheral configurations within Wasm binaries.
  arXiv  Detail & Related papers  (2025-03-10T17:22:00Z)
• L2MAC: Large Language Model Automatic Computer for Extensive Code Generation [52.81694565226513]
  Transformer-based large language models (LLMs) are constrained by the fixed context window of the underlying transformer architecture.<n>This paper presents L2MAC, the first practical LLM-based general-purpose stored-program automatic computer (von Neumann architecture) framework, for long and consistent output generation.
  arXiv  Detail & Related papers  (2023-10-02T16:55:19Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory [8.414722884952525]
  We introduce a new security property we call relaxed microarchitectural isolation (RMI)<n>RMI allows sensitive programs that are not-constant-time to share memory with an attacker while restricting the information leakage to that of non-speculative execution.<n>Our end-to-end prototype, Citadel, consists of an FPGA-based multicore processor that boots Linux and runs secure applications.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.