Towards practical verifiable computation: Verification outsourcing, linear arguments without linearity tests, and repeated structures

Cloud Computing represents a new trend in modern computing. Since computation can be purchased as a service, companies and individual users can cut down their computing assets and outsource any burdensome computational workload. In addition to savings in computing infrastructure, the Cloud may also provide expert technical consulting. But while outsourcing computation provides appealing benefits, one must fully consider a critical security issue: there is no guarantee on the correctness of the results. That is, the Cloud servers should be considered error-prone and may or may not be fully trustworthy. Thus an immediate need for result assurance naturally arises. This need motivates a growing body of research on verification of outsourced computation. Researchers strive for verifying the result of general computation, not limited to a specific computational task. Extending classical proof systems, interactive proof (IP) systems and probabilistically checkable proof (PCP) systems provide basic theoretical models and meaningful tools for applications. Unfortunately, PCPs and hence arguments are wildly impractical: traditional PCPs are too expensive to instantiate at the prover or query from the verifier. While state-of-the-art PCP schemes are asymptotically efficient, the constants on their running times are large, and they seem too intricate to be implemented easily.;This dissertation focuses on the verifiable computation, taking steps towards bringing it closer to practicality. We argue that since the verification may be tedious and expensive, users are likely to outsource (again) the verification workload to a third party. Other scenarios such as auditing and arbitrating may also require the use of third-party verification. Outsourcing verification will introduce new security challenges. One such challenge is to protect the computational task and the results from the untrusted third party verifier. In this work, we address this problem by proposing an efficient verification outsourcing scheme. To our knowledge, this is the first solution to the verification outsourcing problem. We show that, without using expensive fully-homomorphic encryption, an honest-but-curious third party can help to verify the result of an outsourced computational task without having to learn either the computational task or the result thereof. We have implemented our design by combining a novel commitment protocol and an additive-homomorphic encryption in the argument system model. The total cost of the verification in our design is less than the verifiers cost in the state-of-the-art argument systems that rely only on standard cryptographic assumptions.;Besides the introduction of the verification outsourcing paradigm, we also bring improvements to the state-of-the-art verification protocol designs. We firstly investigate the linearity tests, which overwhelmingly occupy the bandwidth of the interaction part of the state-of-the-art designs based on linear PCP. Our results show that under certain assumptions, if this Single- Commit-Multi-Decommit protocol further combines with the linear PCP, the linearity tests in the combined linear PCP become redundant. Our theoretical result immediately results in RIVER, a new linear-PCP-based argument system which achieves lower cost. Then, we focus on the computations with repeated sub-structures and design a novel verification protocol, that takes advantage of these particular features. We notice the state of the art involve a considerable cost, including the verifiers amortized cost, (i.e., the cost that needs to be amortized over a large number of work instances), and the provers cost of proof generation. The most efficient argument systems still incur an amortized cost that is linear in the size of the circuit. We address reducing this cost for those outsourced computations which contain repeated substructures (e.g. loops). Since loops play a pivotal role in the real world of computing (not only compute-intensive computations but also data-intensive computations such as big data applications), we take loops as a typical example, propose the first verification protocol that is specific for computations with repeated structures and show that the circuit generated from computation with loops can indeed lead to a lower amortized cost and a lower cost of proof generation. Using the theory of arithmetic circuit complexity we prove that for most programs our design results in very significant savings.