טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentRiabzev Michael
SubjectComputation Verification for Noobs
DepartmentDepartment of Computer Science
Supervisor Professor Yuval Ishai
Full Thesis textFull thesis text - English Version


Abstract

Computational-integrity (also known as checking-computation [BFLS91], verifiable-computation [PGHR13,CFHKKNPZ15], and computation-delegation [GKR08]) protocols eliminate the need to trust reporters of computation results, by allowing the latter to provide a cryptographic proof attesting to the validity of the results. The proof verification time is polylogarithmic with the length of the computation (succinct), introducing significant improvement over the naive solution for general computations, which is merely re-execution. Computational-integrity protocols were introduced around three decades ago [BFLS91]. This original work offered theoretical solutions to practical problems. An immediate practical motivation for taking such an approach comes from a different field of mathematical-proofs done by computer such as the celebrated example of [AH79] showing that any planar graph is four-colourable. The method used in [AH79] included a computer exhaustively verifying correctness of a finite set of graphs, requiring work beyond what is humanly achievable, and took over a thousand hours to complete using the computer. Obviously, anyone who did not want to repeat this heavy verification process had to put their trust in the researcher who claimed to execute it. This kind of a proof to a mathematical claim was novel,
 and the fact the proof cannot be easily verified by peer reviews disappointed many. Computational-integrity is a natural solution to such problems, as it can be used by researchers to generate a succinct proof for the integrity of any computation, verifiable by anyone. Unfortunately, the work of [AH79] predated the initial ideas of verifiable computation,
 introduced in [BFLS91], by roughly a decade. Even though roughly three decades have passed since the introduction of [BFLS91], it is still probably infeasible to use modern computational-integrity for problems of such complexity. Although there are implementations of succinct verifiers that can succinctly verify the correctness of a small proof, the computation overhead on the prover, compared to the naive computation, is still too high. The line of research work we present shows what we have done in order to advance the field of computational-integrity from theory to practice. Our results show how theory can be improved to provide concrete efficiency. A common technique we have used is adding interactivity to both improve the soundness of protocols, and reduce the proving computational load. In addition to theoretical improvements, we provide three POC implementations of systems used to measure the constructions' concrete efficiency. Moreover, the implementations can be used as a reference for production grade system, as they introduce efficient data-structures and algorithms designed and tuned for implementation of algebraic proof systems.