Hypervisor implementations such as XMHF, Nova, PROSPER, prplHypervisor, the various L4 descendants, as well as KVM and Xen offer mechanisms for dynamic startup and reconfiguration, including the allocation, delegation and destruction of objects and resources at runtime. Some use cases such as cloud computing depend on this dynamicity, yet its inclusion also renders the state space intractable to simulation-based verification tools. On the other hand, system architectures for embedded devices are often fixed in the number and properties of isolated tasks, therefore a much simpler, less dynamic hypervisor design would suffice. We close this design gap by presenting Phidias, a new hypervisor consisting of a minimal runtime codebase that is almost devoid of dynamicity, and a comprehensive compile-time configuration framework. We then leverage this lack of dynamic components to non-interactively verify the validity of certain invariants. Specifically, we verify hypervisor integrity by subjecting the compiled hypervisor binary to our own symbolic execution engine. Finally, we discuss our results, point out possible improvements, and hint at unexplored characteristics of a static hypervisor design.

Adversaries with physical access to a target platform can perform cold boot or DMA attacks to extract sensitive data from the RAM. To prevent such attacks, hardware vendors announced respective processor extensions. AMD's extension SME will provide means to encrypt the RAM to protect security-relevant assets that reside there. The encryption will protect the user's content against passive eavesdropping. However, the level of protection it provides in scenarios that involve an adversary who cannot only read from RAM but also change content in RAM is less clear. This paper addresses the open research question whether encryption alone is a dependable protection mechanism in practice when considering an active adversary. To this end, we first build a software based memory encryption solution on a desktop system which mimics AMD's SME. Subsequently, we demonstrate a proof-of-concept fault attack on this system, by which we are able to extract the private RSA key of a GnuPG user. Our work suggests that transparent memory encryption is not enough to prevent active attacks.