不安全块Rust程序的模块化形式化验证
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
