Hunting Virtio Specification Violations
- Track: Virtualization and Cloud Infrastructure
- Room: UB4.132
- Day: Sunday
- Start: 10:00
- End: 10:30
- Video only: ub4132
- Chat: Join the conversation!
In the rust-vmm project, we implement VirtIO devices in Rust by following the VirtIO specification that defines how devices and driver interact. For example, the specification outlines the steps that drivers must follow to initialize a device. If a driver makes any incorrect sequence, the device returns an error. While the driver or device may not always conform to the spec, deviations can lead to unexpected behaviors or bugs. In this presentation, we introduce two tools to check whether a VirtIO device conforms to the specification. Firstly, we present Kani - a tool developed by Amazon that is used to verify conformance in devices implemented in Firecracker. Secondly, we discuss an experimental tool that validates conformance during the execution of the device. This is a Rust tracer that developers can add to an existing device to ensure its implementation conforms to the specification. Traces are compared with the specification at runtime to detect any violations that may have occurred.
Speakers
Matias Vara Larsen |