Description
With a large part of today’s internet being served from applications running on multitenant
servers, hypervisor security has become very important due to the damage
potential vulnerabilities inside them can cause. There has also been a growing demand
to support tenants being able to act as hypervisors themselves and spawn their own
respective guests, so, despite these high stakes, nested virtualization with hardware
support has been adopted as a new feature by most major hypervisors in the recent
past.
For this feature to be secure, the hypervisor has to, among other things, properly
translate the Virtual machine control structure (VMCS) it gets passed by the first-level
guest to a VMCS that can securely be passed on to hardware to start the nested guest
without allowing for privilege escalation.
In this thesis, we build a symbolic execution based approach to differentially analyze
the way the KVM and Virtualbox hypervisors implement this mechanism.
We find that our approach can reproduce the findings of prior fuzzing-based work by
Großmann [Gro25] and surface interesting differences and patterns in the reachability of
single-bit values in the resulting VMCS passed on to hardware. In addition to that, our
approach also enables further, deeper manual analysis of the translation mechanism.
|
