virtio-queue: verification: prevent loop in load and store methods

[MatiasVara]

Kani needs to iterate through VolatileSlices in the load and store methods mentioned in [1]. To handle this, we would need to unroll a loop. However, Kani doesn’t support unrolling a specific loop, it only allows setting a global unroll count [2]. Setting all loops to unroll once leads to problems, e.g., the execution gets stuck in infinite unrolling. For now, we’ve disabled the verify_add_used() proof (see #371), but this should ideally be addressed with a proper fix later.

[1] rust-vmm/vm-memory@66b9427
[2] https://model-checking.github.io/kani/tutorial-loop-unwinding.html

[priyasiddharth]

Apart from this breakage, imo it would be better to move the StubRegion to vm_memory crate and enable kani there. This way breaking changes will be caught when changes are made in vm_memory rather than downstream in client projects.

[MatiasVara]

Apart from this breakage, imo it would be better to move the StubRegion to vm_memory crate and enable kani there. This way breaking changes will be caught when changes are made in vm_memory rather than downstream in client projects.

I see but the implementation of queue is in vm-virtio, which is what we are testing ....

[stefano-garzarella]

@priyasiddharth FYI we are going to move all the rust-vmm crates in a single repo (monorepo) by the end of the year, so in that way we can catch this kind of issues early. So my suggestion for now is to keep the StubRegion here.

[priyasiddharth]

Thanks @stefano-garzarella.

@MatiasVara, i am only talking about StubRegion, not the proofs. For testing queue, we interface with other components like vm_memory. If we maintain all stub components in queue but have no control over the interface then over time we will necessarily diverge.