Transparent pointer safety: Rust to Lua to OS Components

数字安全设计(DSbD)挑战在Morello之上构建了一个软件生态系统，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组件接口。必须将这些代码区域声明为不安全的，从而启用编译器无法检查的有限的附加操作集，放弃为安全代码提供的自动保证。这种不安全代码的分离为编程能力硬件提供了一个模型：Ruust确保安全代码不会显示能力错误，而不安全代码突出显示可以针对验证工具的区域。Lua是一种安全的托管语言，用于设置FreeBSD引导加载器。我们将把Lua解释器移植到Rust，将其集成到FreeBSD中，并确定垃圾收集器不会出现能力故障。我们提供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.