Mar 17, 2024
1 min read
Rust,

Rust 社区发起标准库验证竞赛,验证内存安全性

Rust 社区发起了一项标准库验证竞赛,其核心宗旨在于充分借助广大社区的磅礴力量,深度验证 Rust 标准库的安全性。

Rust 社区发起标准库验证竞赛,验证内存安全性

Rust 社区发起了一项标准库验证竞赛,其核心宗旨在于充分借助广大社区的磅礴力量,深度验证 Rust 标准库的安全性。

在 Rust 编程语言的世界里,标准库的可靠性与安全性至关重要。今天,我们就一同走进验证 Rust 标准库的奇妙领域,看看其中有哪些值得关注的亮点与挑战。

这项工作的目录主要是验证 Rust 标准库工作旨在为 Rust 标准库提供自动验证,确保其实现安全。目标是验证给定的 Rust 标准库实现是否安全。

基本介绍

但是想要验证Rust 标准库是一件很困难的工作,主要挑战在于:

  1.  缺乏规范

  2. Rust生态系统中缺乏现有的验证机制

  3. 验证问题规模较大

  4. 可扩展验证的未知数

考虑到这项工作的规模和范围,基金会认为这应该是社区主导的工作。为此,他们发起了一场竞赛,其中包括一系列挑战,重点是验证内存安全和 Rust 标准库中未定义行为的子集。

主要努力主要分为以下几个方面:

  1. 为验证 Rust 标准库的核心机制做出贡献

  2. 创建新技术来执行可扩展的验证

  3. 应用技术来验证标准库中以前未验证的部分。

每项挑战均根据其规格提供相应的财务奖励,并在成功完成后颁发。

挑战规则

验证目标

官方主要分叉了一个分支[verfi-rust](GitHub - model-checking/verify-rust-std: Verifying the Rust standard library)作为挑战目标,其library/文件夹中保留了 Rust 标准库的副本。

挑战内容

每个单独的验证工作都会有一个跟踪问题,贡献者可以在其中添加评论并提出澄清问题。挑战者可以在此处找到开放挑战的列表。

解决方案

问题的解决方案应作为单个拉取请求 (PR) 提交到此存储库。该解决方案应作为 CI 的一部分运行。查看有关每个解决方案最低要求的更多详细信息。

事实上,这项工作并不正式附属于 Rust 项目或 Rust 基金会,也没有得到其认可。

他们还发布了更详细的工作流程、方案要求等,感兴趣的可以[点击这里](Introduction - Verify Rust Std Lib) 看看。