< 返回版块

关于安全性的证明

Nalleyer 发表于 2020-05-01 21:09

楼主是多年的rust萌新了，写了很多也看了很多。最近计划整理一个ppt，分享一下rust给身边的人。

现在我突然有个疑问。我看过的不论是文档，还是书籍，都只说了（或者是我只记得我看到了）rust达到了怎样的安全等级，以及它是怎么实现的，但是缺乏了听众最关心的“如何证明它的安全”。

对于例如rustc的实现有没有经过形式证明啊，理论上又有哪些结论啊，什么论文里面能查到这些知识，这一类问题，各位有什么资料可以分享一下吗？

先行谢过各位。

评论区

写评论
作者 Nalleyer 2020-05-02 10:05

万分感谢楼上大神！ 对以下内容的回复：

Mike Tang 2020-05-02 09:50

哇哦，我学习了。感谢楼上。

7sDream 2020-05-02 05:24

帮楼上（下？）补一个 《Why Rust》 的链接。

另外有两篇个人认为比较重要的论文：

  1. 证明不使用 unsafe 的 Rust 程序是内存安全的：《Patina: A Formalization of the Rust Programming Language》
  2. 讨论单个使用 unsafe 的 library 的内存安全：《https://homes.cs.washington.edu/~emina/doc/crust.ase15.pdf》
  3. 讨论多个使用 unsafe 的 library 的内存安全：《RustBelt: Securing the Foundations of the Rust Programming Language》

其实这个 RustBelt 项目是个围绕 Rust 安全性的大项目，有很多可以看的论文。

另外再推荐一篇 RustBelt 成员 Ralf Jung 的博文《Formalizing Rust》

Mike Tang 2020-05-01 22:59

这个parity的一篇博文里面提到过，我明天去翻翻。你也可以搜一下：Why Rust

1 共 4 条评论, 1 页