Verifiable computing


Verifiable computing enables a computer to offload the computation of some function, to other perhaps untrusted clients, while maintaining verifiable results. The other clients evaluate the function and return the result with a proof that the computation of the function was carried out correctly. The introduction of this notion came as a result of the increasingly common phenomenon of "outsourcing" computation to untrusted users in projects such as SETI@home and also to the growing desire of weak clients to outsource computational tasks to a more powerful computation service like in cloud computing. The concept dates back to work by Babai et al., and has been studied under various terms, including "checking computations", "delegating computations", "certified computation", and verifiable computing. The term verifiable computing itself was formalized by Rosario Gennaro, Craig Gentry, and Bryan Parno, and echoes Micali's "certified computation".

Motivation and overview

The growing desire to outsource computational tasks from a relatively weak computational device to a more powerful computation services, and the problem of dishonest workers who modify their client's software to return plausible results without performing the actual work motivated the formalization of the notion of Verifiable Computation.
Verifiable computing is not only concerned with getting the result of the outsourced function on the client's input and the proof of its correctness, but also with the client being able to verify the proof with significantly less computational effort than computing the function from scratch.
Considerable attention has been devoted in verifying the computation of functions performed by untrusted workers including the use of secure coprocessors, Trusted Platform Modules, interactive proofs, probabilistically checkable proofs, efficient arguments, and Micali's CS proofs. These verifications are either interactive which require the client to interact with the worker to verify the correctness proof, or are non-interactive protocols which can be proven in the random oracle model.

Verification by replication

The largest verified computation uses verification by replication.
The SETI@home verification process involves one client machine and many worker machines.
The client machine sends identical workunits to multiple computers.
When not enough results are returned in a reasonable amount of time—due to machines accidentally turned off, communication breakdowns, etc.—or the results do not agree—due to computation errors, cheating by submitting false data without actually doing the work, etc.—then the client machine sends more identical workunits to other worker machines.
Once a minimum quorum of the results agree, then the client assumes those results are correct.
The client grants credit to all machines that returned the correct results.

Verifiable computation

Gennaro et al. defined the notion of verifiable computation scheme as a protocol between two polynomial time parties to collaborate on the computation of a function F: n → m. This scheme consists of three main phases:
  1. Preprocessing. This stage is performed once by the client in order to calculate some auxiliary information associated with F. Part of this information is public to be shared with the worker while the rest is private and kept with the client.
  2. Input preparation. In this stage, the client calculates some auxiliary information about the input of the function. Part of this information is public while the rest is private and kept with the client. The public information is sent to the worker to compute F on the input data.
  3. Output computation and verification. In this stage, the worker uses the public information associated with the function F and the input, which are calculated in the previous two phases, to compute an encoded output of the function F on the provided input. This result is then returned to the client to verify its correctness by computing the actual value of the output by decoding the result returned by the worker using the private information calculated in the previous phases.
The defined notion of verifiable computation scheme minimizes the interaction between the client and the worker into exactly two messages, where a single message sent from each party to the other party during the different phases of the protocol.

An example scheme based on fully homomorphic encryption

Gennaro et al. defined a verifiable computation scheme for any function F using Yao's garbled circuit combined with a fully homomorphic encryption system.
This verifiable computation scheme VC is defined as follows:
VC = consists of four algorithms as follows:
  1. KeyGen → : The randomized key generation algorithm generates two keys, public and private, based on the security parameter λ. The public key encodes the target function F and is sent to the worker to compute F. On the other hand, the secret key is kept private by the client.
  2. ProbGenSK → : The problem generation algorithm encodes the function input x into two values, public and private, using the secret key SK. The public value σx is given to the worker to compute F with, while the secret value τx is kept private by the client.
  3. Compute → σy: The worker computes an encoded value σy of the function's output y = F using the client's public key PK and the encoded input σx.
  4. VerifySK → y ∪ ⊥: The verification algorithm converts the worker's encoded output σy into the actual output of the function F using both the secret key SK and the secret “decoding” τx. It outputs y = F if the σy represents a valid output of F on x, or outputs ⊥ otherwise.
The protocol of the verifiable computations scheme defined by Gennaro et al. works as follows:
The function F should be represented as a Boolean circuit on which the key generation algorithm would be applied. The key generation algorithm runs Yao's garbling procedure over this Boolean circuit to compute the public and secret keys. The public key is composed of all the ciphertexts that represent the garbled circuit, and the secret key is composed of all the random wire labels. The generated secret key is then used in the problem generation algorithm. This algorithm first generates a new pair of public and secret keys for the homomorphic encryption scheme, and then uses these keys with the homomorphic scheme to encrypt the correct input wires, represented as the secret key of the garbled circuit. The produced ciphertexts represent the public encoding of the input that is given to the worker, while the secret key is kept private by the client. After that, the worker applies the computation steps of the Yao's protocol over the ciphertexts generated by the problem generation algorithm. This is done by recursively decrypting the gate ciphertexts until arriving to the final output wire values. The homomorphic properties of the encryption scheme enable the worker to obtain an encryption of the correct output wire. Finally, the worker returns the ciphertexts of the output to the client who decrypts them to compute the actual output y = F or ⊥.
The definition of the verifiable computation scheme states that the scheme should be both correct and secure. Scheme Correctness is achieved if the problem generation algorithm produces values that enable an honest worker to compute encoded output values that will verify successfully and correspond to the evaluation of F on those inputs. On the other hand, a verifiable computation scheme is secure if a malicious worker cannot convince the verification algorithm to accept an incorrect output for a given function F and input x.

Practical verifiable computing

Although it was shown that verifiable computing is possible in theory, most of the known constructions are very expensive in practice. Recently, some researchers have looked at making verifiable computation practical. One such effort is the work of UT Austin researchers. The authors start with an argument system based on probabilistically checkable proofs and reduce its costs by a factor of 1020. They also implemented their techniques in the system. The authors note that "Our conclusion so far is that, as a tool for building secure systems, PCPs and argument systems are not a lost cause."
The overall area, which now includes a number of implementations by different groups, has been surveyed.