The motivation for this paper is that x86 devices don't automatically get virtualization because of sensitive instructions like popf, and should satisfy the author to compose a formal definition for the x86 computer to support virtualization
Equivalence, i.e., the VMM needs to simulate an environment for the virtual machine on the host that is essentially the same as the physical machine. The virtual machine runs on this environment in the same way as it does on the physical machine, except that it may perform slightly differently in the virtual environment due to resource competition or VMM intervention, e.g., the I/O, network, etc. of the virtual machine may be slower than when it is exclusively on the physical machine due to the host's speed limit or multiple virtual machines sharing resources.
Efficient, i.e., the performance of virtual machine instruction execution is not significantly degraded compared to running on a physical machine. The standard requires that the vast majority of instructions in the virtual machine run directly on the physical CPU without VMM intervention, such as the ARM system we run on the x86 architecture through Qemu is not virtualized, but emulated.
Resource control, that is, VMM can completely control system resources. The VMM controls the coordination of host resources to individual virtual machines, and cannot be controlled by the virtual machine having the resources of the host.
The solution for that is Trap and Emulate model. Privileged instructions can only be run in system mode and will trigger a processor exception if run in user mode. The operating system allows the kernel to run in system mode because the kernel needs to manage system resources and needs to run privileged instructions, while normal user programs run in user mode. In the fall-in and simulation models, the user programs of the virtual machine still run in user mode, but the kernel of the virtual machine will also run in user mode, in a way called privileged compression. In this approach, the unprivileged instructions in the virtual machine run directly on the processor, satisfying the virtualization standard's requirement for efficiency, i.e., most instructions run directly on the processor without VMM intervention. However, when a VM executes a privileged instruction because it is running in user mode, it will trigger a processor exception, which will fall into the VMM, which will act as a proxy for the VM to complete access to system resources, the so-called emulate. In this way, the requirements of the virtualization standard for VMM-controlled system resources are again met, and the virtual machine will not modify the host's resources because it can run privileged instructions directly, thus destroying the host's environment.
They prove using the definition of the machine S = (E, M, P, R) and using A virtual machine map (VM map) f: Cr -> Co is a one-one homomorphism with respect to all the operators $e_i$ in the instruction sequence set L to bound the instruction change or trap does not leak message or information by two states. If this proof is correct, I think it's great.
Critique
I generally agree with the author using the state machine to formally prove how sensitive instruction affects message leakage. But now if we want to prove something, we may have a better framework like Framework K.
The novelty comes in that it classifies the sensitive instruction that
Instructions that attempt to access or modify the virtual machine mode or machine state.
Instructions that attempt to access or modify sensitive registers or storage units, such as clock registers, interrupt registers, etc.
Instructions that attempt to access the memory protection system or memory or address allocation system.
All I/O instructions.
The essence of the "fall-in-simulation" is to ensure that instructions that may affect the correct operation of the VMM are simulated by the VMM and that most of the non-sensitive instructions run as usual. The CPU needs to support a protection mechanism, such as MMU, to isolate the physical system and other VMs from the currently active VMs. 4. Since the execution of control-sensitive instructions may change the state of the system (processor and device), in order to ensure the absolute control of resources by the VMM and maintain the normal operation of the VM, the execution of such instructions needs to fall into the VMM and transfer the control to the VMM, which will handle the simulation. The execution result of behavior-sensitive instructions depends on the highest privilege level of the CPU, and the Guest OS runs at a non-highest privilege level, so to ensure the correct result, it also needs to fall into the VMM and be emulated by it.
It's obviously the start of the whole virtualization industry or cloud industry. The Full virtualization party, represented by VMware, is paranoid about the idea of running without modifications. Xen's excellent performance with appropriate modifications to the Guest OS and Xen's excellent performance with appropriate modifications to the Guest OS made Para virtualization a big hit. Later, Intel and AMD entered the fray and expanded the hardware to address the difficulties of traditional x86 virtualization and to improve performance. In the end, hardware extensions were adopted by both the Full and Para schools. Since then, the performance advantage of the Para school has been less obvious, and the friendliness of the Full school, which runs directly without modification, has gradually gained the upper hand The user-friendliness of running without modification is gaining ground.
Although various solutions have been used from the software level to solve the problems encountered when virtualizing the x86 architecture, these solutions have introduced additional overhead in addition to significant complexity to the VMM implementation. Intel did not modify the unprivileged sensitive instructions to privileged ones, because not all privileged instructions need to be intercepted. As a typical example, whenever the OS kernel switches processes, it switches the cr3 register so that it points to the page table of the currently running process. However, when using the shadow page table for GVA to HPA mapping, the VMM module needs to capture every operation of Guest to set the cr3 register to point to the shadow page table. When hardware-level EPT support is enabled, the cr3 register no longer needs to point to the shadow page table; it still points to the page table of Guest's process. Intel developed VT technology to support virtualization by adding Virtual-Machine Extensions, or VMX, to CPUs. VMM runs in VMX Root Mode, which is not fundamentally different from normal mode except that it supports VMX.
