PhD Proposal: Verifiable Computation in Practice: Tools and Protocols

Talk
Ahmed Kosba
Time: 
05.05.2017 09:00 to 10:30
Location: 

AVW 3450

Cloud computing enables many scenarios where users can use mobile and computationally-limited devices flexibly, while outsourcing expensive computations to remote servers. This raises a security requirement for integrity-sensitive applications, when a remote server is untrusted, and when it has to provide secret inputs to the computation. Efficient cryptographic techniques are needed to verify the integrity of the computation, and authenticate any secret inputs. Recently, new systems have been proposed to provide solutions for the problem of Verifiable Computation (VC), in which efficient constructions for Zero-Knowledge Succinct Non-interactive ARguments of Knowledge (zk-SNARKs) were provided. Such techniques enable the untrusted server to prove the correctness of the computation in zero-knowledge using a succinct constant-size proof that can be verified very efficiently by the verifier.

My thesis will aim at addressing some challenges in the current VC systems, and develop practical protocols for different applications. The challenges mainly include the computation overhead at the prover side, and the level of expertise expected from the programmers to write secure and efficient programs for VC. More specifically, current VC protocols require the computation task to be carefully expressed as an arithmetic circuit. A programmer could rely on two approaches, either by low-level development tools; or by expressing the computation in a high-level program and rely on compilers to perform the program-to-circuit transformation. The former approach is difficult to use but on the other hand allows an expert programmer to perform custom optimizations. In comparison, the latter approach is more friendly to non-specialist users, but existing compilers often emit suboptimal circuits, and still require some experience from the programmers.

I propose a framework that aims to reduce the proof computation overhead, and offer more programmability to non-specialist developers, while automating the task of circuit size minimization through a combination of techniques. The framework includes new circuit-friendly algorithms for frequent operations that achieve constant to asymptotic savings over existing algorithms; optimizations for short- and long- integer arithmetic; as well as circuit minimization techniques. In addition, I explore and optimize cryptographic primitives that can be considered SNARK-friendly to be implemented as arithmetic circuits.

Furthermore, I explore different settings where VC can be useful. For example, I present the design of Hawk, a system for privacy-preserving smart contracts. Hawk enables custom decentralized applications in the smart contract setting to run verifiably on top of the blockchain, while keeping the participants' inputs private. My future work will extend verifiable computation to other settings where integrity and privacy are needed as in biological applications.

Examining Committee:

Co-Chairs: Dr. Charalampos Papamanthou

Dr. Elaine Shi

Dept rep: Dr. Hector Corrada Bravo

Members: Dr. Michael Hicks

Dr. Jonathan Katz