Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor

Developing systems code that robustly provides its intended security guarantees remains very challenging: conventional practice does not suffice, and full functional verification, while now feasible in some contexts, has substantial barriers to entry and use.