The BedRock Ultravisor provides client operating systems (guest OSes) with a virtualization layer on a shared physical machine. To show that the Ultravisor enables strong isolation properties, we need to prove a refinement between the virtualization stack (the implementation), running on the physical machine, and the "bare-metal" virtual machine (the specification). This is particularly challenging because both the bare-metal machine and the virtualization stack are composed of multiple (hardware/software) interacting components. Furthermore, the software components are implemented across multiple levels of abstractions (e.g., in both assembly and C++). In this talk, we present an approach to establish an end-to-end refinement theorem that avoids constructing new operational semantics for intermediate abstractions, and instead incrementally constructs those abstractions within separation logics. First, we reflect both the bare-metal virtual machine and the physical machine, both expressed operationally using process calculi, into separation logics. The bare-metal machine is encoded as pure ghost state, and the physical machine is tied into weakest preconditions. Second, we break down the physical machine model into smaller, separate, communicating systems. We then selectively recombine slices of these individual systems to build up increasingly abstract reasoning principles. For example, we demonstrate how to combine low-level resources of a CPU core and some DRAM memory segments, to establish higher-level resources to reason about an "assembly language program" stored in said memory segments. We can also encode convenient protocols for driving I/O devices from code running on the CPU. Third, we orthogonally decompose the specification (the bare-metal virtual machine) into smaller, separate specification models, and modularly show that the components of the implementation refine those models in separation logics, using the reasoning principles from the previous step. We show how our approach supports both horizontal decomposition (roughly characterized by [WP p1 ** WP p2 |-- WP (p1 || p2)]), and vertical decomposition (roughly characterized by [WP src |-- WP target]). Working within separation logic allows us to work with an "open-ended" foundation, where we can use small footprint abstractions and we can under-specify complex behaviors.