Practical Symbolic Execution for 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.