Skip to main content

Verifiable Properties of Computations Outsourced to the Cloud

Researchers: Virgil Gligor, Anupam Datta, Amit Vasudevan

Cross Cutting Thrusts: Cryptography


Large-scale data analytics, machine learning, and large-scale enterprise computing are likely to require both storage- and computation-intensive resources. Such scalable architectures are captured in various application settings by the notion of cloud computing. For example, in a typical setting, a relatively weak computing client would often outsource computations to powerful worker programs operating in a cloud. In general, the client expects to be able to efficiently verify the correctness of the results returned by the worker programs since in most environments cloud computations cannot be trusted; e.g., they may be subject to adversary attacks, both from outside of the cloud and from privileged insiders. Efficient result verification leads to the notion of verifiable computations

The notion of verifiable computation – introduced by CMU research -- requires advanced cryptographic constructs, including fully homomorphic encryption. A key advantage of cryptography-based verifiable computation is that a client would not need to trust worker programs and their cloud computing platform at all; e.g., the worker's operating system and/or hardware may be malicious or malfunctioning. Furthermore, the state of the worker's platform on which the outsourced computation is performed may be arbitrary; e.g., the platform many be contaminated by malware or corrupted by privileged insiders. In this admittedly narrow setting, formal verification of most worker and platform security properties would become unnecessary. To date, this notion of verifiable computation has addressed only limited properties of outsourced computations; e.g., attestation of a simple program un-tampered execution on a single remote server. Future research will need to address the following basic questions: Could one always avoid the complexity of formal analysis based on system structuring, secure software development, and trustworthy operational assurance, and yet obtain desired security and other outsourced program guarantees by relying exclusively on cryptography-based verifiable-computation techniques? If so, what types of properties and what application architectures (e.g., outsourced applications, third-party applications) could be supported? If no, what types of system architecture would simplify the formal verification effort necessary to obtain verified security properties? And what type of architecture would enable the composition of verified properties and their scaling to large application components? 

The goals of this research leverage extensive past CMU experience and extend into new and uncharted areas. For example, making a clear and unambiguous case that, in general, verifiable computation requires trustworthy computing platforms and devices and cannot rely exclusively on cryptographic primitives will help drive the attention onto the design of practical architectures for trustworthy computing -- not just on fast crypto implementations. Specific research projects include the verification of resource use in the cloud, flexible client-directed resource provisioning, verifiable confinement of cloud computations, and client-controlled access policy enforcement in a multi-tenant cloud.