<p>It is possible in standard cryptographic assumptions (like, existence of cryptographic hash functions), and proofs can be made non-interactive in a random oracle model.</p>
<p>Modern zero knowledge proofs are also asymptotically shorter than the computation itself, so you could publish a short argument (relative to the computation time) that the execution of the program gave the result O.</p>
<p>Techniques to read about are ZK-Starks (weakest cryptographic assumptions) and various ZK-Snarks, which typically leverage at least hardness of discrete logarithm (Bulletproofs, Halo) or stronger assumptions about elliptic curves with pairings (Pinoccio).</p>
<hr />
<p>I will very briefly explain the basic idea behind ZK-Starks. First of all, we could use a Merkle tree to make prover commit on a trace of computation, and then probabilistically check in ~N queries that, say, 1-const/N of gates were executed correctly. However, flipping even one bit in a computation might make it go completely wrong, so we are in a very strange model of error-resistant computation: normally, error-resistance is against random errors, but here errors are malicious, prover can force specific gates to misbehave.</p>
<p>So, the trace of computation is transformed into some polynomial, and the predicate of being correct on each gate is transformed into some property on these polynomials.</p>
<p>(I'd like to warn you that in practice there are a lot of technical details, for instance because nobody likes working with Turing machines, but you can imagine that you have some polynomial P(x), and its values in points <span class="math-container">$x \in \{1...m; m+1, ... 2m; ..., (n-1)m+1 ... nm\}$</span> encode the state of the tape of length m in time n.</p>
<p>Then, encoding states of the cells of the tape by values of the polynomial, you can devise polynomial condition <span class="math-container">$Q$</span></p>
<p><span class="math-container">$Q(P(x+n), P(x), P(x+1), P(x+2), x) = 0$</span> in every point of the set <span class="math-container">$\{1...mn\}$</span>, which holds iff the state of your Turing machine at the moment t+1 is a correct evolution of its state in the moment t). The variable x is added explicitly to control overflow.</p>
<p>Then, you can reformulate it as a condition on polynomials which holds everywhere. Indeed, you can just demand that <span class="math-container">$Q(P(x+n), P(x), P(x+1), P(x+2), x) = IH$</span>, where I is an indicator polynomial <span class="math-container">$(x-1)...(x-mn)$</span>, and <span class="math-container">$H$</span> is some polynomial. It is equivalent to the previous condition.</p>
<p>Now, good thing about polynomials is that if you check the condition in a random point, and size of your field is big (think ~2^256) relative to the degree of a polynomial, then with overwhelming probability condition holding in a random point holds everywhere.</p>
<p>The rest is error-correcting codes: you need to somehow check that the commited function is a polynomial of bounded degree, or at least <span class="math-container">$\varepsilon$</span>-close to it (in Hamming distance). For this, you repeatedly engage in Fourier-transform-like activity, breaking the polynomial into odd and even part and proving it for its random linear combination.</p>
<hr />
<p>Good classical results to read and understand where these techniques come from:</p>
<p>Matiyasevich's classical theorem on non-solvability of diophantine equations is, I believe, one of the first examples of arithmetization. It is over <span class="math-container">$\mathbb{Z}$</span> and encoding is not by polynomials, but by numbers, but it is the predecessor of the whole story.</p>
<p>IP=PSPACE is a celebrated result that any PSPACE problem can be verified by an interactive probabilistic protocol of polynomial time. In this result prover is computationally unbounded, but ideas of encoding your boolean formula as an arithmetic circuit over bigger finite field <span class="math-container">$\mathbb{F}_q$</span> and then using random linear combinations to convince polynomially bounded verifier are all there.</p>

CC BY-SA 4.0
2021-11-23T01:49:39.513Z
2021-11-23T01:57:51.813Z
2021-11-23T01:57:51.813Z
Lev Soukhanov
<p>Let's suppose that we create a program P, that given input I, generates output O. We then want to run this program on an untrusted computer C that may either want to tamper with the program (run P' instead) or tamper with the output (return O' instead). Is it possible to augment the program such that the new output Q contains both O and some form of proof or probabilistic &quot;suggestion&quot; (hash) that O was generated by running P (and not P', and was not substituted for O')?</p>
<p>One naive solution would be to run the same program locally and check that the outputs are identical. Given that, it would make sense to limit solution space only to those where the verification is faster (by perhaps a constant) than the runtime of the program.</p>
<p>That rules out hashing the state of the program (perhaps at every state change) - verifying the hash requires re-running the program locally. I don't know how to make a subsampling (i.e. hashing every N steps) work.</p>
<p>In terms of homomorphic encryption <a href="https://cstheory.stackexchange.com/questions/2873/can-a-fully-homomorphic-encryption-be-used-for-oblivious-code-execution">this question is similar but distinct</a>. There, we see that we can't obfuscate code, but we are going only after verification.</p>
<p>On the surface, it doesn't look like this would violate anything. We are not gaining runtime (e.g. if P is a program that computes an exponential algorithm, going through every possible augmented output will not be faster); we don't get knowledge of whether the program always halts.</p>

CC BY-SA 4.0
2021-11-07T19:41:30.033Z
Probabilistically checkable proofs (PCPs) do something like this.  They are defined as interactive proofs, e.g. of a given formula being satisfiable, but maybe you could apply them to the standard encoding of a TM computation as a SAT formula (similar to the Cook-Levin theorem proof) to obtain a PCP that a given computation took place.  Although the standard PCPs still require the verifier to essentially do the computation (build the SAT formula), so this isn't quite what you're after.
Neal Young
CC BY-SA 4.0
2021-11-10T14:56:14.223Z
I took a closer look at FHE - turns out that there are additions that make the program (circuit, in their parlance) resistant against malicious attacks or changes (paper: Maliciously Circuit-Private FHE). This proves that it's possible to have a scheme like what I want, but that paper is a superset of what I care about.
DarthShader
<cr.crypto-security><turing-machines><homomorphic-encryption>
Q: Trusting program output from an untrusted machine
DarthShader
# Q: Trusting program output from an untrusted machine

(Asked by: username_0 on 2021-11-07)

Let's suppose that we create a program P, that given input I, generates output O. We then want to run this program on an untrusted computer C that may either want to tamper with the program (run P' instead) or tamper with the output (return O' instead). Is it possible to augment the program such that the new output Q contains both O and some form of proof or probabilistic "suggestion" (hash) that O was generated by running P (and not P', and was not substituted for O')?

One naive solution would be to run the same program locally and check that the outputs are identical. Given that, it would make sense to limit solution space only to those where the verification is faster (by perhaps a constant) than the runtime of the program.

That rules out hashing the state of the program (perhaps at every state change) - verifying the hash requires re-running the program locally. I don't know how to make a subsampling (i.e. hashing every N steps) work.

In terms of homomorphic encryption [this question is similar but distinct](https://cstheory.stackexchange.com/questions/2873/can-a-fully-homomorphic-encryption-be-used-for-oblivious-code-execution). There, we see that we can't obfuscate code, but we are going only after verification.

On the surface, it doesn't look like this would violate anything. We are not gaining runtime (e.g. if P is a program that computes an exponential algorithm, going through every possible augmented output will not be faster); we don't get knowledge of whether the program always halts.

**Tags:** cr.crypto-security, turing-machines, homomorphic-encryption
> **Comments:**
> **username_1**: Probabilistically checkable proofs (PCPs) do something like this.  They are defined as interactive proofs, e.g. of a given formula being satisfiable, but maybe you could apply them to the standard encoding of a TM computation as a SAT formula (similar to the Cook-Levin theorem proof) to obtain a PCP that a given computation took place.  Although the standard PCPs still require the verifier to essentially do the computation (build the SAT formula), so this isn't quite what you're after.  
> **username_0**: I took a closer look at FHE - turns out that there are additions that make the program (circuit, in their parlance) resistant against malicious attacks or changes (paper: Maliciously Circuit-Private FHE). This proves that it's possible to have a scheme like what I want, but that paper is a superset of what I care about.  

---

## 1 answers

### Answer by username_2 on 2021-11-23. Score: 5 | Accepted answer

It is possible in standard cryptographic assumptions (like, existence of cryptographic hash functions), and proofs can be made non-interactive in a random oracle model.

Modern zero knowledge proofs are also asymptotically shorter than the computation itself, so you could publish a short argument (relative to the computation time) that the execution of the program gave the result O.

Techniques to read about are ZK-Starks (weakest cryptographic assumptions) and various ZK-Snarks, which typically leverage at least hardness of discrete logarithm (Bulletproofs, Halo) or stronger assumptions about elliptic curves with pairings (Pinoccio).

---

I will very briefly explain the basic idea behind ZK-Starks. First of all, we could use a Merkle tree to make prover commit on a trace of computation, and then probabilistically check in ~N queries that, say, 1-const/N of gates were executed correctly. However, flipping even one bit in a computation might make it go completely wrong, so we are in a very strange model of error-resistant computation: normally, error-resistance is against random errors, but here errors are malicious, prover can force specific gates to misbehave.

So, the trace of computation is transformed into some polynomial, and the predicate of being correct on each gate is transformed into some property on these polynomials.

(I'd like to warn you that in practice there are a lot of technical details, for instance because nobody likes working with Turing machines, but you can imagine that you have some polynomial P(x), and its values in points $x \in \{1...m; m+1, ... 2m; ..., (n-1)m+1 ... nm\}$ encode the state of the tape of length m in time n.

Then, encoding states of the cells of the tape by values of the polynomial, you can devise polynomial condition $Q$

$Q(P(x+n), P(x), P(x+1), P(x+2), x) = 0$ in every point of the set $\{1...mn\}$, which holds iff the state of your Turing machine at the moment t+1 is a correct evolution of its state in the moment t). The variable x is added explicitly to control overflow.

Then, you can reformulate it as a condition on polynomials which holds everywhere. Indeed, you can just demand that $Q(P(x+n), P(x), P(x+1), P(x+2), x) = IH$, where I is an indicator polynomial $(x-1)...(x-mn)$, and $H$ is some polynomial. It is equivalent to the previous condition.

Now, good thing about polynomials is that if you check the condition in a random point, and size of your field is big (think ~2^256) relative to the degree of a polynomial, then with overwhelming probability condition holding in a random point holds everywhere.

The rest is error-correcting codes: you need to somehow check that the commited function is a polynomial of bounded degree, or at least $\varepsilon$-close to it (in Hamming distance). For this, you repeatedly engage in Fourier-transform-like activity, breaking the polynomial into odd and even part and proving it for its random linear combination.

---

Good classical results to read and understand where these techniques come from:

Matiyasevich's classical theorem on non-solvability of diophantine equations is, I believe, one of the first examples of arithmetization. It is over $\mathbb{Z}$ and encoding is not by polynomials, but by numbers, but it is the predecessor of the whole story.

IP=PSPACE is a celebrated result that any PSPACE problem can be verified by an interactive probabilistic protocol of polynomial time. In this result prover is computationally unbounded, but ideas of encoding your boolean formula as an arithmetic circuit over bigger finite field $\mathbb{F}\_q$ and then using random linear combinations to convince polynomially bounded verifier are all there.


---

