"Verifying Memory Safety for the Rust Standard Library"
summary
AWS organizes a crowdsourced contest that defines small verification goals for the Rust standard library, posts challenges with success criteria, and awards cash bounties up to $40,000 for new tools. There are four verification tools already able to handle the library, seven challenges solved, and 37% of the library covered by formal contracts and proofs. The program reports 121 contributors in the last month, multiple bug fixes merged into core, and reusable models emerging from Verifast, Flux, ESBMC and others.
AI-written summary · about
chapters (7)
- 0:00Introduction to the project
- 0:42Goal of verifying Rust core
- 2:33The crowdsourcing contest
- 4:43Challenge creation process
- 5:35Notable results and metrics
- 7:40Acknowledging contributors
- 9:10Call to action and closing
related talks
01h 01mMemory Safety: Rust vs. C
45mBuilding Safe and Secure Systems in Rust
45mRust
01h 09mThe Rust Programming Language: Origin, History and Why it's so important for Arm today
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
30mIntegrating Rust into Tor: Successes and Challenges
44mUnsafe Rust
30mEnsuring Rust Safety: Strategies for Managing Unsafe Rust