论文标题
模块化对具有不安全块的生锈程序的形式验证
Modular Formal Verification of Rust Programs with Unsafe Blocks
论文作者
论文摘要
Rust是一种现代系统编程语言，其类型系统可确保内存安全性。为了表达和性能，它允许程序员使用不安全的代码块暂时放松键入规则。但是，在不安全的块中，确保代码最终不会具有未定义的行为的负担在程序员身上。即使是大多数专家程序员，在不安全的块中犯错误和记忆安全错误也会使所有类型系统保证无效。为了解决这个问题，我们正在尝试验证使用模块化符号执行算法的Rust不安全代码的声音。本文概述了我们的方法以及到目前为止取得的进步。
Rust is a modern systems programming language whose type system guarantees memory safety. For the sake of expressivity and performance it allows programmers to relax typing rules temporarily, using unsafe code blocks. However, in unsafe blocks, the burden of making sure that the code does not end up having undefined behaviour is on the programmer. Even most expert programmers make mistakes and a memory safety bug in an unsafe block renders all the type system guarantees void. To address this problem we are trying to verify soundness of Rust unsafe code applying our Modular Symbolic Execution algorithm. This text outlines our approach and the progress that has been made so far.
