Survey tools suitability for Std safety verification

rust-lang / rust-project-goals

Rust Project Goals tracker

https://rust-lang.github.io/rust-project-goals/

MIT License

51 stars 49 forks source link

Survey tools suitability for Std safety verification #126

Open nikomatsakis opened 4 months ago

nikomatsakis commented 4 months ago

Metadata
Owner(s)	@celinval
Team(s)	libs
Goal document	2024h2/std-verification

Summary

Instrument a fork of the standard library (the [verify-rust-std] repository) with safety contracts, and employ existing verification tools to verify the standard library.

Tasks and status

[x] Discussion and moral support (libs )
[ ] Standard review (libs )
[x] Problem proposals ()
[x] Fork maintenance (@celinval, @jaisnan)
[ ] Fork PR Reviews ()
[ ] Instrumentation and verification ()

nikomatsakis commented 4 months ago

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

celinval commented 3 months ago

Update: So far we have integrated Kani into our repository and we have successfully instrumented and verified 22 functions in the standard library. We have also published 11 challenges.

We are currently investigating the integration of other tools, such as Gillian Rust and Verus.

celinval commented 2 months ago

Key developments: We have welcome the help of students from the CMU Practicum Project. They have started writing functions contracts that include the safety conditions for some unsafe functions in the core library, as well as verifying that safe abstractions respect those pre-conditions and are indeed safe. Help wanted: Contracts and verification harnesses are being added to our existing fork: https://github.com/model-checking/verify-rust-std. Help needed to write more contracts, to integrate new tools, to review pull requests or to participate in the repository discussions.

celinval commented 1 week ago

Key developments: A new partnership between the Rust Foundation and AWS will help fund this effort [ref]. The verification challenges in the verify-rust-std fork now have financial rewards for those completing them. Help wanted: Help needed to write more contracts, to integrate new tools, to review pull requests or to participate in the repository discussions.