Internships/ProjectIdeas/KaniProofsInRustVMM: Difference between revisions

Latest revision as of 11:15, 12 February 2025

Adding Kani proofs for Virtqueues in Rust-vmm

Expected outcome: 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.

Kani is an open-source tool and any issues like regarding performance can be reported on GitHub. For more information, the blog[1] contains several examples on how to use Kani in real codebases (including Firecracker). Also, there is a current effort for verifying the Rust Standard Library using Kani [2].

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:

Details:

Project size: 175 or 350 hours, depending on how many proofs you wish to tackle
Skill level: intermediate
Language: Rust
Mentor: Matias Ezequiel Vara Larsen (mvaralar@redhat.com)

@@ Line 1: / Line 1: @@
-=== Adding Kani proofs for Virtqueues in Rust-vmm ===
+== Adding Kani proofs for Virtqueues in Rust-vmm ==
-'''Summary:''' Verify conformance of the virtqueue implementation in
+'''Expected outcome:''' Verify conformance of the virtqueue implementation in rust-vmm to the VirtIO specification.
-rust-vmm to the VirtIO specification.
 In the rust-vmm project, devices rely on the virtqueue implementation
@@ Line 22: / Line 21: @@
 virtqueue implementation is correct and conformant.
-During the internship, we propose the following tasks:
+Kani is an open-source tool and any issues like regarding performance can be reported on GitHub. For more information, the blog[https://model-checking.github.io/kani-verifier-blog/] contains several examples on how to use Kani in real codebases (including Firecracker). Also, there is a current effort for verifying the Rust Standard Library using Kani [https://model-checking.github.io/verify-rust-std/].
+'''Tasks:'''
 * Finish [https://github.com/rust-vmm/vm-virtio/pull/324 current PR] that adds a proof for the notification suppression mechanism
 * Port [https://github.com/firecracker-microvm/firecracker/blob/4bbbec06ee0d529add07807f75d923cc3d3cd210/src/vmm/src/devices/virtio/queue.rs#L1006 add_used() proof]
 * Port [https://github.com/firecracker-microvm/firecracker/blob/4bbbec06ee0d529add07807f75d923cc3d3cd210/src/vmm/src/devices/virtio/queue.rs#L966 verify_prepare_kick() proof]
+* Port other proofs from queue.rs
 '''Links:'''
 * [https://www.youtube.com/watch?v=w7BAR228344 LPC Talk about how we may check conformance in the VirtIO specification (video)]
 * [https://fosdem.org/2025/schedule/event/fosdem-2025-5930-hunting-virtio-specification-violations/ FOSDEM'25 talk current effort to use Kani]
+* [https://model-checking.github.io/kani-verifier-blog/ Kani Blog]
 '''Details:'''
-* Project size: 350 hours
+* Project size: 175 or 350 hours, depending on how many proofs you wish to tackle
 * Skill level: intermediate
 * Language: Rust
 * Mentor: Matias Ezequiel Vara Larsen (mvaralar@redhat.com)