טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentPergament Evgenya
SubjectAlgebraic RAM
DepartmentDepartment of Computer Science
Supervisor Professor Eliyahu Ben Sasson
Full Thesis textFull thesis text - English Version


Abstract

With the increase of delegation of computation to powerful computational servers, questions of computational integrity and efficient verification start to arise. For instance, we may want to know if the execution was executed correctly or if the server had an incentive to misreport the result. How can the client who delegates a computation verify that the answer he received is the result of the computation? Probabilistically Checkable Proofs (PCP) can be used in order to verify the correctness of a computation that is executed by an untrusted server, such that the verification time is significantly less than the time needed to run the computation itself. They are, however, considered to be efficient only in theory. People believe that the constants that appear in the asymptotic measurements make PCPs impractical.


In this thesis we focus on arithmetization, i.e., encoding the transition function of a computation as an algebraic problem. Arithmetization is used in many theoretical and practical results, and is valuable in making PCPs practical. In order to encode the transition function, we define polynomials over a field F such that these polynomials are set to zero iff the computation corresponding to that function is executed correctly. The main contribution of our work is that we have significantly reduced the number of variables over which these polynomials are defined. This reduction improves both prover and verifier practical efficiency as well as the proof length. Also, ours is one of the first works, that uses arithmetization over a field of small characteristic. Our encoding uses a number of variables that is only linear in size of a register, even in fields of small characteristic.


Another main contribution of our work is a modular construction of polynomials for transition functions. We start by defining a set of polynomials for opcodes, such as bitwise-XOR, ADD, etc. These polynomials are set to zero iff an opcode is executed correctly. Then, we expand this set of polynomials to capture instructions. An instruction consists of an opcode and operands upon which the opcode operates. For example, ADD R1,R2,R3, which denotes that register R1, should be assigned with the addition result of registers R2,R3, namely, R1 = R2 R3. For each instruction, we define a set of polynomials that is set to zero iff an instruction is executed correctly. Finally, we expand these sets of polynomials to capture the transition's function correctness. Using this encoding technique, one can arithmetize numerous programs, in particular any sequential code written in assembly language.


We implemented the arithmetization in C for assembly language based on TinyRAM assembly language. TinyRAM is a Random Access Machine (RAM) whose assembly language is concise yet, at the same time, is expressive and contains widely-used opcodes that produce efficient assembly codes for high-level languages. We present concrete measurements of the arithmetization for programs written in this assembly.