On Thu, Feb 06, 2025 at 10:02:43AM -0500, Stefan Hajnoczi wrote: > 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 though that those three proofs were the more interesting. I think we can cover all the proofs in queue.rs during the internship. Matias
