2
$\begingroup$

I have a simple program F (think of a cellular automaton) that, when executed in some input X, takes a while to complete and returns a short result (a hash function, for example). How do I produce a short string that proves the result F(X) = Y without requiring the verifier to run the entire computation?

I'm aware of zk-snarks, but I couldn't a simple, practical "get started" guide to them. Moreover, they might be overkill for this since I don't need any privacy.

$\endgroup$
  • $\begingroup$ To bte honest, if security (privacy, etc.) is of no interest to you, then this is the wrong site for that question. I suggest looking for the keyword verifiable computation, but possibly you only get cryptographic results, here's one paper I just remembered: Parno, Gentry, Howell, Raykova Pinocchio: Nearly Practical Verifiable Computation (2013). $\endgroup$ – tylo Dec 8 '17 at 11:51
  • $\begingroup$ @tylo ah, you're correct, I didn't think that. Which S.E. sub-site would you suggest? $\endgroup$ – MaiaVictor Dec 8 '17 at 14:17
  • 3
    $\begingroup$ @tylo By no means is the goal of cryptographic solutions always privacy. Integrity is another important protection goal addressed in cryptography, so asking this question seems totally reasonable. Verifiable computing is indeed the right place to start looking for solutions. $\endgroup$ – mti Dec 8 '17 at 14:35
  • 1
    $\begingroup$ This is clearly in the scope of crypto. You do not need the full power of snargs (which need not be zk, btw), because you only want to prove efficient computation (polytime). There exists other proof systems tailored to that. But do you need a theoretical solution (if so I can point to papers) or a practical, implemented one? (If so, snargs being more popular because of their wider range of applications which goes well further delegation, you are more likely to find smth if you look for implementations of snargs, even though they're overkill in a sense) $\endgroup$ – Geoffroy Couteau Dec 9 '17 at 7:10
  • $\begingroup$ @GeoffroyCouteau I'm looking for something which is realistically implementable by me... if that does not exist, something that has been implemented at least once would be great. $\endgroup$ – MaiaVictor Dec 9 '17 at 11:45
4
$\begingroup$

There are several option - none of which is trivial to implement.

A bit of background first. Essentially, verifiable delegation of computation boils down to being able to prove relations between inputs and outputs, so that the verification time is way smaller than the computation time, for relations that can be computed in polynomial time. In contrast, the famous SNARGs are way more powerful, as they also allow to prove any NP statement, even those that are not known to be computable in polynomial time. So in a sense, delegating computation is "easier" than constructing SNARGs. However, two remarks are in order:

  • A very large effort has been devoted to the analysis and construction of SNARGs, even leading to some implementations (e.g. zcash). Therefore, it might be that the current best way of verifying delegated computation in practice goes through SNARGs
  • A sense in which SNARGs are harder than verifiable computation is with respect to the underlying assumptions: while we have strong indications that SNARGs require non-standard assumptions, we know how to base verifiable computation on standard assumptions. But if you are looking for a practical solution, you might well not care about the theoretical issues of the underlying assumptions.

For those reasons, even in SNARG is an overkill from a theoretical point of view, it is not necessarily the case if what you care about is practice, and you can easily find some implementations (there are more recent ones, such as the famous Pinocchio, or the even more recent Geppetto).

That being said, there are several natural approaches for delegation of computation. The first that comes to mind is this approach, which is the seminal paper on the topic of delegation, and that works for restricted classes of computation. This approach was refined several time, culminating with this beautiful paper that gives a very satisfying solution for delegating evaluation of boolean circuit, with reasonable efficiency. I believe they have implementations, I do not know how easy it is to find and reuse these implementations.

The second, that I only mention for the sake of completeness, is to use techniques for batch verification: the prover evaluate the same program $P$ on many inputs $x_1, \cdots, x_n$, in time $O(sn)$ ($s$ being the time needed to evaluate $P$ on a single input) and the verifier can check the correctness of all computations in time $O(s + n)$, instead of $O(sn)$.

Another natural approach (see also this paper, this paper, and papers that reference them on Google scholar) for delegation of computation essentially requires to ask the server to perform the computation in the encrypted domain, via fully homomorphic encryption. It is based on homomorphic MACs, which can be constructed from FHE. From my understanding, they are conceptually quite simple - you essentially have to execute the computation several time in the encrypted domain, and there is an easy check for the verifier. The main issue is the cost of using FHE - but if your circuit is small enough, using this recent FHE scheme (see also the follow up) which performs bootstrapping in less than 20ms, this might be quite feasible. For more restricted computations, one can also avoid using FHE.

I've not read it yet, but if you have access to the ACM digital library, there was a recent survey on the subject of verifiable computation, by one of the leading researchers in the area (Rosario Gennaro), called "Verifiable Outsourced Computation: A Survey".

$\endgroup$
  • $\begingroup$ I'm not sure if it is reasonable to ask this kind of question here, but would you be willing to give me 1 or 2 hours of consulting? This is costing way to much time because I'm essentially walking through a huge field without knowing exactly where the answer lies for my particular issues. Consulting with an expert would be invaluable and speed up this process a lot, I believe. $\endgroup$ – MaiaVictor Dec 9 '17 at 22:44
  • $\begingroup$ Well, I suppose that's something we'd better discuss by mail (geoffroy dot couteau (at) ens dot fr). But the bottom line is, if a 1h consulting time could suffice to help you (or something very reasonable of this kind), I might also consider doing it for free. $\endgroup$ – Geoffroy Couteau Dec 10 '17 at 15:17
0
$\begingroup$

I think there is only one possibility: that is that F(X) is in fact solving a "hard inverse problem", but that depends on the nature of F(X). After all, if there's a simple way to test whether, given X and Y, Y = F(X) you have or 1) a way to calculate F(X) quickly (but then you could implement that in the automaton), or 2) have a way to calculate G(X,Y) = 0, which is exactly the problem of which Y = F(X) is an "inversion". But that depends on the exact nature of F() of course, so there's no solution in all generality.

For instance, think of the problem of solving an equation G(x,y) = 0 for a given x. Solving this equation can be difficult. The procedure to solve such an equation is symbolized by F(): F(x) gives you the y such that G(x,y) = 0. The verification, on the other hand, is easy: put in your solution y in the original equation and see whether it comes out: G(x,y) = 0. Example: discrete exponentiation and discrete log. Suppose that $G(x,y) = a^y - x$ mod p, and F(x) is that y, such that G(x,y) = 0. F(x) is nothing else but the discrete log problem in a field p with generator a. It is hard. However, verifying this is easy.

In all generality, I don't see how there could potentially be a "quick solution" to your question, but for specific cases, yes, but it depends on those cases.

$\endgroup$
  • $\begingroup$ Maybe some generalization - proof of work $\endgroup$ – gusto2 Dec 8 '17 at 14:38
  • $\begingroup$ Proof of work is usually indeed implemented as solving a hard reverse problem: find a number y = f(x) such that hash(y) has x leading zeros. Easy to verify if given x and y: calculate hash(y) and see if it has x leading zeros. Very hard to find a correct y if given x. $\endgroup$ – entrop-x Dec 8 '17 at 14:57
  • 1
    $\begingroup$ There may be another way if we introduce a precomputation step: We may be able to encode F and X into F' and X' and prepare a verification algorithm V and a decoding algorithm D such that for any Y' returned by the worker: if V(Y')=1 then either F(X)=D(Y') or (X,Y') is the solution to a hard computational problem. $\endgroup$ – mti Dec 8 '17 at 15:01
  • 1
    $\begingroup$ I still don't see how this can be general. Suppose that X is "the state of the solar system at t = 0", and I want Y "the state of the solar system 5 billion years from now". The computation of the evolution of the solar system is the long complex calculation. How do I verify the result quickly without doing it over ? (change it into weather forecasting or just any heavy physics simulation) $\endgroup$ – entrop-x Dec 8 '17 at 15:04
  • 1
    $\begingroup$ @entrop-x intuitively perhaps, but can we actually prove that is not possible? Think about it: it'd still require someone to do all the computation. It is just that, as he went, he could be doing "something else" which enabled the next person to perform the same computation to take a lot of shortcuts. $\endgroup$ – MaiaVictor Dec 8 '17 at 16:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.