Rust 社区发起标准库验证竞赛,验证内存安全性
Rust 社区发起了一项标准库验证竞赛,其核心宗旨在于充分借助广大社区的磅礴力量,深度验证 Rust 标准库的安全性。
在 Rust 编程语言的世界里,标准库的可靠性与安全性至关重要。今天,我们就一同走进验证 Rust 标准库的奇妙领域,看看其中有哪些值得关注的亮点与挑战。
这项工作的目录主要是验证 Rust 标准库工作旨在为 Rust 标准库提供自动验证,确保其实现安全。目标是验证给定的 Rust 标准库实现是否安全。
基本介绍
但是想要验证Rust 标准库是一件很困难的工作,主要挑战在于:
-
缺乏规范
-
Rust生态系统中缺乏现有的验证机制
-
验证问题规模较大
-
可扩展验证的未知数
考虑到这项工作的规模和范围,基金会认为这应该是社区主导的工作。为此,他们发起了一场竞赛,其中包括一系列挑战,重点是验证内存安全和 Rust 标准库中未定义行为的子集。
主要努力主要分为以下几个方面:
-
为验证 Rust 标准库的核心机制做出贡献
-
创建新技术来执行可扩展的验证
-
应用技术来验证标准库中以前未验证的部分。
每项挑战均根据其规格提供相应的财务奖励,并在成功完成后颁发。
挑战规则
验证目标
官方主要分叉了一个分支[verfi-rust](GitHub - model-checking/verify-rust-std: Verifying the Rust standard library)作为挑战目标,其library/文件夹中保留了 Rust 标准库的副本。
挑战内容
每个单独的验证工作都会有一个跟踪问题,贡献者可以在其中添加评论并提出澄清问题。挑战者可以在此处找到开放挑战的列表。
解决方案
问题的解决方案应作为单个拉取请求 (PR) 提交到此存储库。该解决方案应作为 CI 的一部分运行。查看有关每个解决方案最低要求的更多详细信息。
事实上,这项工作并不正式附属于 Rust 项目或 Rust 基金会,也没有得到其认可。
他们还发布了更详细的工作流程、方案要求等,感兴趣的可以[点击这里](Introduction - Verify Rust Std Lib) 看看。