virtio: fuzz the parsers and the data-plane invariants
Two property kinds. Crash-safety on adversarial bytes: the virtio-PCI capability
walk (a device-controlled cap_next chain) and Virtio_net.handle_control (any
request bytes/offset/length) must never raise, loop, or read out of bounds, and
the control handler's ack stays in {OK,ERR} with the active pair count inside the
advertised [1,max]. High-level data-plane invariants: the mergeable placement
contract (chunks sum to the frame, each fits its buffer, num_buffers counts
them), the loopback round-trip both directions (a transmitted frame is drained
intact or dropped, never corrupted; an injected frame is received up to the
buffer capacity), and a forged receive used index only ever latches failed --
never a crash or OOB. 7 properties, all pass; afl profile drives afl-fuzz.
virtio: fuzz the parsers and the data-plane invariants
Two property kinds. Crash-safety on adversarial bytes: the virtio-PCI capability
walk (a device-controlled cap_next chain) and Virtio_net.handle_control (any
request bytes/offset/length) must never raise, loop, or read out of bounds, and
the control handler's ack stays in {OK,ERR} with the active pair count inside the
advertised [1,max]. High-level data-plane invariants: the mergeable placement
contract (chunks sum to the frame, each fits its buffer, num_buffers counts
them), the loopback round-trip both directions (a transmitted frame is drained
intact or dropped, never corrupted; an injected frame is received up to the
buffer capacity), and a forged receive used index only ever latches failed --
never a crash or OOB. 7 properties, all pass; afl profile drives afl-fuzz.