Rustv: Semi-automatic Verification of Unsafe Rust Programs

Explore a 21-minute conference talk on semi-automatic verification of unsafe Rust programs presented by Yulu Pan and Yuichi Nishiwaki. Delve into the architecture of seL4 verification and learn how theorem provers are utilized in the process. Discover the speakers' approach to adapting seL4's methodology for Rust, including translation into Isabelle/Simpl, global heap representation, and function state space representation. Examine an example of verification, covering program translation, formalizing safety conditions, and proof of safety. Gain insights into the verification effort, interesting examples, and key observations. Conclude with a discussion on future work and a summary of the presented concepts.

Intro
This work
Outline • Overview
Background
What we want to do
The architecture of sel4 verification Verification using theorem prover
Our approach (in the future) Adapt sel 4's approach to Rust
Translation into Isabelle/Simpl
Global heap representation
Function state space representation
Example of Verification
Program translation
Formalizing safety conditions
Proof of safety
Verification Effort
Interesting example
Why?
Some observations
Future work
Summary