Transparent pointer safety: Rust to Lua to OS Components

透明指针安全：Rust 到 Lua 到 OS 组件

基本信息

批准号：
EP/X021173/1
负责人：
Mark Batty
金额：
$ 63.04万
依托单位：
University of Kent
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2022
资助国家：
英国
起止时间：
2022 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FX021173%2F1
关键词：
Transparent pointer safety Rust Lua

项目摘要

The Digital Security by Design (DSbD) challenge builds a software ecosystem atop Morello, an ARM processor extended with capabilities. Capabilities combine a pointer to memory with permissions and bounds information that Morello processors use to enforce memory safety at run time, halting programs in error when safety is violated. This project develops a vertical stack in the DSbD ecosystem in three parts: a Rust compiler, an implementation of Lua in Rust, and integration of this Lua interpreter into FreeBSD, replacing a core component of the FreeBSD bootloader with software built in DSbD tech.Rust maximises the guarantees provided by capabilities with a memory-saftey-first design, and Lua is a high-level language used for joining systems components together, with the details of memory management safely automated. We will support this vertical with a theoretical development. In our Lua interpreter, we anticipate allocation and reclamation requiring unsafe Rust code, and we will verify that these components cannot produce capability errors. We will raise this to memory safety of the whole interpreter by proving that safe Rust code should never exhibit capability errors.Rust is a systems language from academia with substantial industrial use. Rust is proposed as the second language of the Linux kernel after C, with support from the creator of Linux. Rust excludes the vast majority of pointer misuse - ensuring memory safety - with a static (compile time) check, and a fall-back run-time check for complex cases. Our Rust compiler port will, as a consequence, port all safe Rust code to Morello, and typical Rust programmers may target Morello with no change to their working practices.Sometimes a Rust programmer must subvert the type system, e.g. to interface with hardware or C OS components. These regions of code must be declared as unsafe, enabling a limited set of additional operations that the compiler cannot check, forgoing the automatic guarantees afforded to safe code. This segregation of unsafe code offers a model for programming capability hardware: Rust ensures safe code cannot exhibit capability errors, and unsafe code highlights regions where verification tools can be targeted.Lua is a safe managed language that is used to set up the FreeBSD bootloader. We will port the Lua interpreter to Rust, integrate it into FreeBSD and establish that the garbage collector cannot capability fault.We offer Rust, memory-safe Lua and OS components, together with a theoretical case study that demonstrates scalable security reasoning enabled by the new capability features.

数字设计安全 (DSbD) 挑战赛在 Morello（一款功能扩展的 ARM 处理器）之上构建了一个软件生态系统。这些功能将指向内存的指针与权限和边界信息相结合，Morello 处理器使用这些信息在运行时强制执行内存安全，从而在违反安全性时停止错误的程序。该项目在 DSbD 生态系统中开发了一个垂直堆栈，分为三个部分：Rust 编译器、Rust 中 Lua 的实现以及将此 Lua 解释器集成到 FreeBSD 中，用 DSbD 技术中内置的软件替换 FreeBSD 引导加载程序的核心组件。Rust通过内存安全优先的设计最大限度地保证了功能所提供的保证，Lua 是一种高级语言，用于将系统组件连接在一起，并安全地自动化内存管理的细节。我们将通过理论发展来支持这一垂直领域。在我们的 Lua 解释器中，我们预计分配和回收需要不安全的 Rust 代码，并且我们将验证这些组件不会产生功能错误。我们将通过证明安全的 Rust 代码永远不会出现功能错误，将其提升到整个解释器的内存安全性。Rust 是一种来自学术界的系统语言，具有大量的工业用途。在 Linux 创建者的支持下，Rust 被提议作为继 C 之后的 Linux 内核的第二语言。 Rust 通过静态（编译时）检查和针对复杂情况的回退运行时检查来排除绝大多数指针误用，从而确保内存安全。因此，我们的 Rust 编译器端口将把所有安全的 Rust 代码移植到 Morello，典型的 Rust 程序员可能会以 Morello 为目标，而不改变他们的工作实践。有时，Rust 程序员必须颠覆类型系统，例如与硬件或 C OS 组件连接。这些代码区域必须声明为不安全，从而启用编译器无法检查的一组有限的附加操作，从而放弃为安全代码提供的自动保证。这种不安全代码的隔离为编程能力硬件提供了一个模型：Rust 确保安全代码不会出现能力错误，而不安全代码则突出显示验证工具可以瞄准的区域。Lua 是一种安全托管语言，用于设置 FreeBSD 引导加载程序。我们将把 Lua 解释器移植到 Rust，将其集成到 FreeBSD 中，并确保垃圾收集器无法处理故障。我们提供 Rust、内存安全的 Lua 和操作系统组件，以及理论案例研究，展示新的可扩展安全推理功能。能力特征。