On Tue, Jan 28, 2025 at 11:16:43AM -0500, Stefan Hajnoczi wrote: > Dear QEMU and KVM communities, > QEMU will apply for the Google Summer of Code internship > program again this year. Regular contributors can submit project > ideas that they'd like to mentor by replying to this email by > February 7th. > > About Google Summer of Code > ----------------------------------------- > GSoC (https://summerofcode.withgoogle.com/) offers paid open > source remote work internships to eligible people wishing to participate > in open source development. QEMU has been doing internship for > many years. Our mentors have enjoyed helping talented interns make > their first open source contributions and some former interns continue > to participate today. > > Who can mentor > ---------------------- > Regular contributors to QEMU and KVM can participate as mentors. > Mentorship involves about 5 hours of time commitment per week to > communicate with the intern, review their patches, etc. Time is also > required during the intern selection phase to communicate with > applicants. Being a mentor is an opportunity to help someone get > started in open source development, will give you experience with > managing a project in a low-stakes environment, and a chance to > explore interesting technical ideas that you may not have time to > develop yourself. > > How to propose your idea > ------------------------------ > Reply to this email with the following project idea template filled in: > > === TITLE === > > '''Summary:''' Short description of the project > > Detailed description of the project that explains the general idea, > including a list of high-level tasks that will be completed by the > project, and provides enough background for someone unfamiliar with > the code base to research the idea. Typically 2 or 3 paragraphs. > > '''Links:''' > * Links to mailing lists threads, git repos, or web sites > > '''Details:''' > * Skill level: beginner or intermediate or advanced > * Language: C/Python/Rust/etc > > More information > ---------------------- > You can find out about the process we follow here: > Video: https://www.youtube.com/watch?v=xNVCX7YMUL8 > Slides (PDF): https://vmsplice.net/~stefan/stefanha-kvm-forum-2016.pdf > > The QEMU wiki page for GSoC 2024 is now available: > https://wiki.qemu.org/Google_Summer_of_Code_2025 > > What about Outreachy? > ------------------------------- > We have struggled to find sponsors for the Outreachy internship > program (https://www.outreachy.org/) in recent years. If you or your > organization would like to sponsor an Outreachy internship, please get > in touch. > > Thanks, > Stefan === 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]) '''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
