überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor