Internships/ProjectIdeas/KaniProofsInRustVMM

Adding Kani proofs for Virtqueues in Rust-vmm

Summary: Verify conformance of the virtqueue implementation in rust-vmm to the VirtIO specification.

In the rust-vmm project, devices rely on the virtqueue implementation provided by the `vm-virtio` crate. This implementation is based on the VirtIO specification, which defines the behavior and requirements for virtqueues. To ensure that the implementation meets these specifications, we have been relying on unit tests that check the output of the code given specific inputs.

However, writing unit tests can be incomplete, as it's challenging to cover all possible scenarios and edge cases. During this internship, we propose a more comprehensive approach: using Kani proofs to verify that the virtqueue implementation conforms to the VirtIO specification.

Kani allows us to write exhaustive checks for all possible values, going beyond what unit tests can achieve. By writing Kani proofs, we can confirm that our implementation meets the requirements of the VirtIO specification. If a proof passes, it provides strong evidence that the virtqueue implementation is correct and conformant.

During the internship, we propose the following tasks:

• Finish current PR that adds a proof for the notification suppression mechanism
• Port add_used() proof
• Port verify_prepare_kick() proof
• Port other proofs from queue.rs

Links:

• LPC Talk about how we may check conformance in the VirtIO specification (video)
• FOSDEM'25 talk current effort to use Kani

Details:

• Project size: 350 hours
• Skill level: intermediate
• Language: Rust
• Mentor: Matias Ezequiel Vara Larsen (mvaralar@redhat.com)