Confidential computing is an increasingly popular means to wider Cloud adoption. By offering confidential virtual machines and enclaves, Cloud service providers now host organizations, such as banks and hospitals, that abide by stringent legal requirement with regards to their client’s data confidentiality. These technologies foster sufficient trust to enable such clients to transition to the Cloud, while protecting themselves against a potentially compromised or malicious host. Unfortunately, confidential computing solutions depend on bleeding-edge emerging hardware that (1) takes long to roll out at the Cloud scale and (2) as a recent technology, lacks a clear consensus on both the underlying hardware mechanisms and the exposed programming model and is thus bound to frequent changes and potential security vulnerabilities. This proposal strives to explore the possibilities of building confidential systems without special hardware support. Instead, we will leverage existing commodity hardware that is already deployed in Cloud datacenters combined with new programming language and formal method techniques and identify how to provide similar or even more elaborate confidentiality and integrity guarantees than the existing confidential hardware. Achieving such a software/hardware co-design will enable Cloud providers to deploy new Cloud products for confidential computing without waiting for neither the standardization nor the wide installation of confidential hardware. The key goal of this project is the design and implementation of a trusted, attested, and formally verified monitor acting as a trusted intermediary between resource managers, such as a Cloud hypervisor or an OS, and their clients, e.g., confidential virtual machines and applications. We plan to explore how commodity hardware features, such as hardware support for virtualization, can be leveraged in the implementation of such a solution with as little modification as possible to existing hypervisor implementations.