AI 中文总结
Velosiraptor是一款自动生成正确内存翻译相关操作系统代码的系统，可实现操作系统的硬件移植与新型翻译机制研究，提升开发效率并保障安全性。
AI 中文摘要
安全性是操作系统（OS）开发者最关注的问题之一。安全的运行环境依赖于操作系统正确配置其运行所依托的内存硬件，这是一项关键任务，因为它提供了与安全相关的核心特性和抽象，确保相互并行运行的不可信应用程序的完整性和隔离性。配置平台的内存硬件并非一次性工作，因为设计人员会不断开发具有不同特性和配置方式的新型翻译与保护机制。使操作系统代码适配新硬件不仅是一项手动、重复且耗时的任务，还可能引入细微但对安全至关重要的漏洞，破坏安全和隔离保障。我们提出了Velosiraptor，这是一个能自动生成正确低级操作系统代码以对机器内存硬件进行编程的系统。Velosiraptor利用软件合成技术，并挖掘该问题的领域特性，使合成过程高效。借助Velosiraptor，开发者仅需编写内存硬件映射行为和操作系统环境的高级描述；Velosiraptor工具链会将此规范转换为可与操作系统其余部分直接链接的已验证实现。将操作系统环境纳入此流程，可在无需编写内存硬件配置代码的情况下，将操作系统移植到新硬件平台。我们还可使用同一规范生成硬件组件，这为新型翻译机制的研究提供了支持，使操作系统开发者无需手动编写操作系统代码。
英文摘要
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.
CommentsASPLOS '25, Rotterdam, Netherland
Journal refProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (ASPLOS '25), March 30-April 3, 2025, Rotterdam, Netherlands
