On Thu, Feb 6, 2025 at 4:34 AM Matias Ezequiel Vara Larsen <mvaralar@xxxxxxxxxx> wrote: > === 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: > - Get familiar with Kani proofs written for Firecraker > - Finish current PR that adds a proof for the notification suppression > mechanism (see [2]) > - Port add_used() proof (see [5]) > - Port verify_prepare_kick() proof (see [6]) add_used(), verify_prepare_kick(), and notification suppression are explicitly named. Firecracker's queue.rs has proofs for a number of other proofs as well. Would it be possible to work on them if there is time remaining, or is there a reason why only the proofs you mentioned can be ported? I'm asking because a 12-week internship is likely to leave enough time to tackle more than 3 proofs. Stefan > > '''Links:''' > * [1] Kani source code - https://github.com/model-checking/kani/ > * [2] Notification suppression mechanism PR - > https://github.com/rust-vmm/vm-virtio/pull/324 > * [3] LPC Talk about how we may check conformance in the VirtIO > specification - https://www.youtube.com/watch?v=w7BAR228344 > * [4] FOSDEM'25 talk current effort to use Kani - > https://fosdem.org/2025/schedule/event/fosdem-2025-5930-hunting-virtio-specification-violations/ > * [5] https://github.com/firecracker-microvm/firecracker/blob/4bbbec06ee0d529add07807f75d923cc3d3cd210/src/vmm/src/devices/virtio/queue.rs#L1006 > * [6] https://github.com/firecracker-microvm/firecracker/blob/4bbbec06ee0d529add07807f75d923cc3d3cd210/src/vmm/src/devices/virtio/queue.rs#L966 > > '''Details:''' > * Skill level: intermediate > * Language: Rust >
