MultiNyx: A Multi-Level Abstraction Framework for Systematic Analysis of Hypervisors

MULTINYX is a new framework designed to systematically analyze modern virtual machine monitors (VMMs), which rely on complex processor extensions to enhance their efficiency. To achieve better scalability, MULTINYX introduces selective, multi-level symbolic execution: it analyzes most instructions at a high semantic level, and leverages an executable specification (e.g., the Bochs CPU emulator) to analyze complex instructions at a low semantic level. MULTINYX seamlessly transitions between these different semantic levels of analysis by converting their state. Our experiments demonstrate that MULTINYX is practical and effective at analyzing VMMs. By applying MULTINYX to KVM, we automatically generated 206,628 test cases. We found that many of these test cases revealed inconsistent results that could have security implications. In particular, 98 test cases revealed different results across KVM configurations running on the Intel architecture, and 641 produced different results across architectures (Intel and AMD). We reported some of these inconsistencies to the KVM developers, one of which already has been patched.