A client using a cloud service today trusts the cloud provider to implement and run the service correctly. A service typically depends on millions of lines of code, a multitude of engineers developing the software, administrators managing the service infrastructure, and security mechanisms protecting the platform the service runs on. A single bug, misconfiguration, or a rogue insider can break the service guarantees and mishandle client data. The trust management relies on manual processes such as external audits and hard-to-quantify notions such as «best practices» and provider reputation.

In the Zeta project, we envision making a cloud service untrusted by removing the cloud provider from the trust boundary for some of the guarantees of the service. A client needs only trust standard cryptography, the hardware provided guarantees of Trusted Execution Environments (TEEs), and service-agnostic toolchain such as compilers and SAT-solvers. Our insight is that the execution of a complex, stateful service can be validated by a simple, nearly stateless, «monitor» process. The service is modified to interact with the monitor that runs within a TEE to «prove» its correct execution. The responses from the service are signed by the monitor and verified at the client. The implementation of the monitor and the end-to-end runtime guarantees of the service are formally verified to be correct using the F* proof-oriented programming language (opens in new tab).

We have implemented a verifiable key-value store called FastVer, by extending the FASTER (opens in new tab) system. (We are working on making the FastVer code open source.) We are also working on extending other similar systems and hope to publish details soon.