# On Program Verification Through zk-SNARKs

Can you provide an example use case of program verification using zk-SNARKs that explains:

• What it actually means to verify the execution;
• What are the implication of this new technology;
• How does it work, because at moment I still haven't understood the difference between zk-SNARKs and proofs that can be generated with asymmetric cryptosystems, since they also are zero-knowledge. Are zk-SNARKs just more general? If so can you provide an example use case that highlights what can be done with zk-SNARKs that instead can't be done with asymmetric cryptosystems?
• IACR preprint 879/2013 is 35 pages. Any specific question? – Vadym Fedyukovych May 21 '18 at 10:56

I think the simplest and the best example for a system which uses zk-SNARKs to verify execution of a computation (program) is the Pinocchio system, developed by Microsoft and IBM research groups. You can get access to their source paper, which has some examples, in this URL.

With regard to your questions; the meaning of verifying an execution is that you check that the computation of your target program or circuit has been done correctly. E.g. assume you have a program $$P(.)$$ and you need to run this program with some inputs, e.g. $$x$$. Due to some reasons (e.g. low power device, save money) you outsource the computation and ask some cloud computing services (e.g. Amazon service, Google, Microsoft) to execute this program with this input for you and return the result. The cloud executes the program with your input $$x$$ and returns $$y=P(x)$$ to you. But if you do not trust the server, you are not convinced that $$y$$ is the correct answer for $$P(x)$$. To deal with this issue, the cloud (service provider) needs to give a formal proof that the execution of $$P(x)$$ is done correctly.

Note that outsourcing computation makes sense only if checking the proof generated by service provider is easier (lighter) than recomputing $$P(x)$$ by verifier himself.

zk-SNARKs such as Pinocchio uses pairing-based cryptography which makes the proof size very short (less than 1KB) and proof verification very efficient for verifier (client), verification time is around 0.1 second on current smartphones or laptops.

To get a clear view about how zk-SNARKs are used to prove that an execution of a circuit is done correctly, I strongly recommend to look at Pinocchio system. For a quick overview check the following Slides. At a very high level, the following figure shows what steps Pinocchio system (that uses zk-SNARKs) takes to give a proof for a computation.