M.Sc Student | Pergament Evgenya |
---|---|

Subject | Algebraic RAM |

Department | Department of Computer Science |

Supervisor | Professor Eliyahu Ben Sasson |

Full Thesis text |

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 R_{1},R_{2},R_{3}, which denotes that register R_{1},
should be assigned with the addition result of registers R_{2},R_{3},
namely, R_{1} = R_{2} R_{3}. 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.