权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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