Re: [RFC] virtio-villain: Guest fault injection for VMM robustness

[Anatol Belski <anbelski@linux.microsoft.com>]

Hi Matias,

On Fri, 2026-07-10 at 14:52 +0200, Matias Ezequiel Vara Larsen wrote:
> 


> Thanks for sharing it. I am also interesting on finding violations of
> the virtio specification. I presented something two years ago in LPC
> (see https://lpc.events/event/18/contributions/1897/). As a result of
> that work, we worked adding kani proofs in rust-vmm devices. The
> validation of the spec is coded in RUST and by using kani we verify
> that
> the implemented devices follows the specification. For some
> requirements, we were able to prove that the device is conform. The
> proofs are written together with the implementation of the device
> like
> tests.  

Thanks for the pointer. The virtio-sound case is a good example of why
this matters. The driver was exposing buffers back into the avail ring
while still owned by the device, and nothing caught it until it was
traced by hand.

The work you describe verifies that the rust-vmm device implementations
follow the spec both through formal proofs and runtime observation.
virtio-villain comes at it from the other end by acting as a
deliberately broken guest driver against any VMM and checking whether
the device handles the violation gracefully. Different sides of the
same medal.

> 
> Feel free to file patches to the virtio specification in cases you
> think
> the spec is too permissive. 

That would be worth doing. Several of the divergences I see between
VMMs come down to the spec being silent on what the device should do,
so tightening the normative text would help everyone.

One example is that the spec defines the descriptor addr and len fields
in virtio 1.4 section 2.7.5 but never states what the device must do
when addr plus len falls outside guest physical memory. Every VMM needs
to handle this, and Cloud Hypervisor already fixed it after the harness
surfaced the issue. A normative statement there would save each
implementation from rediscovering the same gap on its own.

> 
> At some point, I wanted to add some checks in QEMU to inform user
> when
> guest violates the spec. That would help to catch some issues with
> less
> testing. For example, two years ago the virtio-sound driver was
> silently
> violating the spec by writing the content of the buffers that were
> already in the available ring. 

That lines up with the discussion in your talk about placing the
observer on the device side. virtio-villain already classifies each
case as pass, reject, or wedge, so the cases where QEMU silently
tolerates a violation instead of flagging it are straightforward to
spot.

Regards

Anatol
>