Re: Call for GSoC internship project ideas

[Matias Ezequiel Vara Larsen <mvaralar@redhat.com>]

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@redhat.com> 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