Practical Symbolic Execution for Rust

Rust 的实用符号执行

• 批准号: 580524-2022
• 负责人: Ko, StevenSY
• 金额: $ 1.82万
• 依托单位: Simon Fraser University
• 依托单位国家: 加拿大
• 项目类别: Alliance Grants
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750537
• 关键词: Practical; Symbolic; Execution; Rust

The goal of our collaboration is to design and implement a practical symbolic execution engine for programs written in the Rust programming language. This goal stems from two factors---the emerging significance of Rust and the lack of symbolic execution support for it. First, Rust is emerging as a critical language to support and use, since it can provide memory safety without compromising on performance. Major software companies, such as Amazon, Microsoft, Google, and Meta (Facebook), all invest in Rust, and the Linux kernel community is now supporting Rust as the second language for developing kernel components. What this shows is that Rust is emerging as a critical language, which is one of the factors of our goal. The second factor of our goal is symbolic execution, which is a fundamental technique used in automated discovery of vulnerabilities and bugs. For example, all three winning teams for 2016 DARPA Cyber Grand Challenge used a variation of symbolic execution to automatically discover bugs and vulnerabilities. However, we have noticed that Rust's infrastructure for symbolic execution is in its infancy---though there has been rapid progress with projects such as Project Oak and MIRAI , there is still much work that needs to be done to use them in large code bases. Thus, our collaboration aims to design and implement a practical symbolic execution engine for Rust.

我们合作的目标是为用Rust编程语言编写的程序设计和实现一个实用的符号执行引擎。这个目标源于两个因素——Rust的重要性和缺乏对它的符号执行支持。首先，Rust正在成为一种需要支持和使用的关键语言，因为它可以在不牺牲性能的情况下提供内存安全。主要的软件公司，如亚马逊、微软、b谷歌和Meta (Facebook)，都在投资Rust， Linux内核社区现在也支持Rust作为开发内核组件的第二种语言。这表明Rust正在成为一门关键语言，这也是我们的目标之一。我们目标的第二个因素是符号执行，这是用于自动发现漏洞和错误的基本技术。例如，2016年DARPA网络大挑战赛的所有三个获胜团队都使用了符号执行的变体来自动发现漏洞和漏洞。然而，我们已经注意到Rust用于符号执行的基础设施还处于起步阶段——尽管像Project Oak和MIRAI这样的项目已经取得了快速进展，但要在大型代码库中使用它们，还有很多工作要做。因此，我们的合作旨在为Rust设计和实现一个实用的符号执行引擎。