Brief Announcement: Incrementally Verifiable Distributed Computation

An $\mathrm{𝖨𝖵𝖢}$ scheme consists of a prover and a verifier. The prover is intended to run alongside the computation whose correctness it proves, so it is important for the prover to have low overhead in terms of space, and for distributed computations, also in terms of communication and rounds. At each point in time, the prover holds a proof that the computation has executed correctly so far, and as the computation proceeds, the prover updates the proof. The interface to the prover consists of a proof update procedure that takes a proof ${\pi }_t$ reflecting some prefix of $t$ computation steps, alongside the current state of the computation ${\mathrm{𝗌𝗍}}_t$, and returns a new proof ${\pi }_{t+1}$ reflecting $t+1$ computation steps. The verifier is modeled as a sequential algorithm. Because the input to the system could be very large (e.g., in streaming or MPC algorithms), we do not assume that the verifier can store all of it, or even that the verifier can store a single global state of the system in its entirety. Instead, the verifier is presented with hashes $h_0,h_t$ of two states ${\mathrm{𝗌𝗍}}_0,{\mathrm{𝗌𝗍}}_t$ of the computation (respectively), a number of steps $t$, and a proof $\pi$, and it checks whether $\pi$ is a “convincing” proof that the computation indeed reaches ${\mathrm{𝗌𝗍}}_t$ after $t$ computation steps from ${\mathrm{𝗌𝗍}}_0$. We use the short-hand notation “${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$” for this statement. The notions of “states” and “computation steps” depends on the exact computation model (e.g., it can mean synchronous rounds, or a single step of a process).

The fact that the verifier is given hashes $h_0,h_t$ of the states ${\mathrm{𝗌𝗍}}_0,{\mathrm{𝗌𝗍}}_t$ instead of plaintext, presents some definitional subtleties, as one cannot reconstruct the original state from its hash value; technically, given $h_0,h_t$ and $t$, the verifier does not even know what statement “${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$” is being asserted. To resolve this we adopt definitions analogous to the one used for RAM delegation [11, 6], where the same issue arises. Informally, the distributed $\mathrm{𝖨𝖵𝖢}$ schemes that we design have the following essential properties:

• $\mathrm{■}$

  Succinctness: the proof is short enough to store on a single machine.

• $\mathrm{■}$

  Incremental completeness: for any system states ${\mathrm{𝗌𝗍}}_0,{\mathrm{𝗌𝗍}}_t$ and ${\mathrm{𝗌𝗍}}_{t+1}$ such that ${\mathrm{𝗌𝗍}}_t$ transitions to ${\mathrm{𝗌𝗍}}_{t+1}$ in one computation step, if the prover is given ${\mathrm{𝗌𝗍}}_0,{\mathrm{𝗌𝗍}}_t$ and a proof ${\pi }_t$ such that the verifier accepts ${\pi }_t$ as a proof for the statement ${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$, then the prover produces a proof ${\pi }_{t+1}$ for the statement “${\mathrm{𝗌𝗍}}_0\stackrel{t+1}{⟶}{\mathrm{𝗌𝗍}}_{t+1}$”, which is also accepted by the verifier.¹¹1Here, by “the verifier accepts ${\pi }_t$ for ${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$” we mean it accepts $(h_0,h_t,t,\pi )$ where $h_0,h_t$ are the respective hash values of ${\mathrm{𝗌𝗍}}_0,{\mathrm{𝗌𝗍}}_t$.

• $\mathrm{■}$

  Computational soundness: no poly-size algorithm²²2That is, an algorithm that can be represented as a circuit with a polynomial number of wires. This is at least as strong as probabilistic polynomial-time Turing machines. can generate values $h_0,h_t,h_t^{\prime }$, a step number $t$ and two proofs ${\pi }_t,{\pi }_t^{\prime }$, such that $h_t\ne h_t^{\prime }$, but the verifier accepts both the proof ${\pi }_t$ with $h_0,h_t,t$ and the proof ${\pi }_t^{\prime }$ with $h_0,h_t^{\prime },t$. Intuitively, this means that the verifier cannot be convinced of two “contradictory statements”, asserting that starting from some initial state (reflected by the hash $h_0$), after $t$ computation steps the system ends up in two different states (reflected by the hashes $h_t\ne h_t^{\prime }$).

The main and most challenging model we handle in this work is massively parallel computation (MPC) [7, 12], where $n$ space-bounded machines collaborate to compute over an input initially partitioned between them. Proving the correctness of MPC computations almost requires $\mathrm{𝖨𝖵𝖢}$: non-incremental verification typically requires access to the entire trace of the computation at once, which in the MPC model no single machine can store. Thus, while efficient distributed provers have already been developed for other distributed models [1, 2], no such construction is known for MPC, even if we do not insist on $\mathrm{𝖨𝖵𝖢}$ and are willing to settle for a non-incremental construction. Thus, our construction of $\mathrm{𝖨𝖵𝖢}$ for MPC addresses not only the problem of incrementality but also the more basic problem of proving the correctness of massively parallel computation.

We consider two use cases. (1) Reliable cloud delegation: a user with input $x$ outsources a heavy computation to a server farm or cloud provider, which returns both the output and a short correctness certificate. The user (a single weak machine) hashes $x$ once, never rereads it, and verifies the result in polylogarithmic time in $|x|$. (2) Internal MPC verification: the network itself verifies correctness so far (e.g., to detect faulty machines). Our distributed IVC maintains a short, continuously updatable certificate that any machine can use to verify locally against its own input. This resembles proof labeling schemes [13] but with polylogarithmic, rather than overall linear proof growth, and with each machine verifying independently without communication.

Our framework for constructing $\mathrm{𝖨𝖵𝖢}$ is modular and generic: we are able to construct $\mathrm{𝖨𝖵𝖢}$ for practically any model of deterministic computation for which we can prove the correctness of a single computation step. We demonstrate this by constructing, in addition to the $\mathrm{𝖨𝖵𝖢}$ for MPC discussed above, $\mathrm{𝖨𝖵𝖢}$ for streaming algorithms, where a low-space single machine processes a stream of elements that arrive over time and cannot all be stored at once, and for PRAM algorithms in the exclusive-read exclusive-write model (EREW), which captures parallel algorithms in shared memory. While for streaming algorithms, proving the correctness of a single computation step is trivial (as the step itself is represented succinctly by the state transition and the stream element), for the PRAM and MPC models we use cryptographic proof systems called succinct non-interactive arguments ($\mathrm{𝖲𝖭𝖠𝖱𝖦}$s): essentially, these are the non-incremental analog of $\mathrm{𝖨𝖵𝖢}$. Specifically, for PRAM we use the existing $\mathrm{𝖲𝖭𝖠𝖱𝖦}$ for PRAM of [9]. For MPC, no such construction is known, so we first construct a $\mathrm{𝖲𝖭𝖠𝖱𝖦}$ for one-round MPC, and then lift it into full-fledged $\mathrm{𝖨𝖵𝖢}$ for MPC. Unlike some commonly used heuristically sound $\mathrm{𝖲𝖭𝖠𝖱𝖪}$s ($\mathrm{𝖲𝖭𝖠𝖱𝖦}$s of knowledge) and $\mathrm{𝖨𝖵𝖢}$ [3, 10], all of our constructions are sound under standard cryptographic assumptions.

Proving that a computation ${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$ is correct boils down to proving the conjunction of $t$ statements: “for each $i=0,\mathrm{\dots },t-1$, the system transitions from state ${\mathrm{𝗌𝗍}}_i$ to state ${\mathrm{𝗌𝗍}}_{i+1}$ in one step”. In existing constructions of (non-incremental) $\mathrm{𝖲𝖭𝖠𝖱𝖦}$ from standard cryptographic assumptions [6, 16, 4], this is done using two cryptographic tools: batch arguments ($\mathrm{𝖡𝖠𝖱𝖦}$s) for $\mathrm{𝖭𝖯}$ and hash families with local openings (e.g., Merkle trees). Informally, a $\mathrm{𝖡𝖠𝖱𝖦}$ for an $\mathrm{𝖭𝖯}$-language $ℒ$ allows us to prove the conjunction of $k$ statements, each of the form “$x_i\in ℒ$”, using a proof whose length grows linearly with the length of a single $\mathrm{𝖭𝖯}$-witness, and only polylogarithmically with the number of statements $k$. A hash family with local openings allows us to hash an $n$-sized vector $v$ to a short hash value $h$, and in addition, given an index $i$, to produce a short opening ${\rho }_i$ to the $i$-th index. Given only $(h,i,v_i,\rho )$, one can verify that $x_i$ is indeed the $i$-th entry of the vector whose hash is $h$.

In prior constructions, to prove (non-incrementally) that ${\mathrm{𝗌𝗍}}_0\stackrel{t}{⟶}{\mathrm{𝗌𝗍}}_t$, the prover hashes the vector $({\mathrm{𝗌𝗍}}_0,\mathrm{\dots },{\mathrm{𝗌𝗍}}_t)$ using a hash with local openings to obtain a hash value $h$. Then it constructs a $\mathrm{𝖡𝖠𝖱𝖦}$ asserting that for each $i=0,\mathrm{\dots },t-1$, there exist states ${\mathrm{𝗌𝗍}}_i,{\mathrm{𝗌𝗍}}_{i+1}$ and openings ${\rho }_i,{\rho }_{i+1}$ such that $h$ opens to ${\mathrm{𝗌𝗍}}_i,{\mathrm{𝗌𝗍}}_{i+1}$ in positions $i,i+1$ (respectively), and ${\mathrm{𝗌𝗍}}_i$ transitions to ${\mathrm{𝗌𝗍}}_{i+1}$ in one step. Here, the states ${\mathrm{𝗌𝗍}}_i,{\mathrm{𝗌𝗍}}_{i+1}$ and the openings ${\rho }_i,{\rho }_{i+1}$ serve as an $\mathrm{𝖭𝖯}$-witness for the statement “the $i$-th step is reflected correctly in the hash $h$”.

When incrementally proving the correctness of a reactive or distributed computation, we do not know in advance what statements the prover will need to prove, as the state that the system will reach depends on the future inputs or messages. Thus, we cannot lay out the entire computation trace in advance, hash it, and prepare a $\mathrm{𝖡𝖠𝖱𝖦}$ proof. To overcome this, we design a scheme we call updatable hash-and-$\mathrm{𝖡𝖠𝖱𝖦}$ ($\mathrm{𝖴𝗉𝖡𝖠𝖱𝖦}$), which imitates the above hash-and-$\mathrm{𝖡𝖠𝖱𝖦}$ paradigm while allowing both the hash and the $\mathrm{𝖡𝖠𝖱𝖦}$ to be constructed incrementally, together. This scheme enables us to update a hash value and a proof for a conjunction of $\mathrm{𝖭𝖯}$-statements on-the-fly, without advance knowledge. To use our $\mathrm{𝖴𝗉𝖡𝖠𝖱𝖦}$ to construct $\mathrm{𝖨𝖵𝖢}$, we must overcome another difficulty, which is that without having the entire trace in advance, we cannot compute the openings that serve as $\mathrm{𝖭𝖯}$-witnesses even for the entries we already have. We show that we can compute the required openings in hindsight, using properties of tree-based hash families with local openings. Our techniques are inspired by the recent works on IVC for sequential deterministic computation [14, 8].

Our work is set in the common reference string (CRS) model. In this model, all parties have access to a string that is sampled randomly by a trusted setup process, denoted by $\mathrm{𝖦𝖾𝗇}$, which takes a security parameter $\lambda$. (This can be viewed as public randomness.) The security parameter governs the computational resources that must be invested to break the security of the protocol: we say that a task that involves the CRS is computationally hard if given $\mathrm{𝖼𝗋𝗌}\leftarrow \mathrm{𝖦𝖾𝗇}(1^{\lambda })$, no poly-size (in $\lambda$) adversary can succeed in the task, except with negligible probability in $\lambda$.

A batch argument ($\mathrm{𝖡𝖠𝖱𝖦}$) [5] allows a prover to succinctly prove the conjunction of $k$ $\mathrm{𝖭𝖯}$ statements, where the size of the proof barely grows with $k$, and is similar to the size of one witness. The interface is as follows:

• $\mathrm{■}$

  $𝒫(\mathrm{𝖼𝗋𝗌},ℳ,x_1,\mathrm{\dots },x_k,w_1,\mathrm{\dots },w_k)\to (\pi )$: takes a reference string $\mathrm{𝖼𝗋𝗌}$, a machine $ℳ$, instances $x_1,\mathrm{\dots },x_k$, and witnesses $w_1,\mathrm{\dots },w_k$, and outputs a proof $\pi$.

• $\mathrm{■}$

  $𝒱(\mathrm{𝖼𝗋𝗌},ℳ,\pi )\to b$: takes a reference string $\mathrm{𝖼𝗋𝗌}$, a machine $ℳ$, and a proof $\pi$ and outputs an acceptance bit $b$.

We say a $\mathrm{𝖡𝖠𝖱𝖦}$ is somewhere extractable if it allows the extraction of one witness from a convincing proof $\pi$, as follows:

• $\mathrm{■}$

  The $\mathrm{𝖼𝗋𝗌}$ generation procedure $\mathrm{𝖦𝖾𝗇}$ may be called in trapdoor mode. In trapdoor mode, $\mathrm{𝖦𝖾𝗇}$ takes as additional input an index $i\in [k]$, called the binding index. It outputs a pair $(\mathrm{𝖼𝗋𝗌},{\mathrm{𝗍𝖽}}_i)$, where $\mathrm{𝗍𝖽}$ is a trapdoor that can later be used to recover the $i$-th witness. In trapdoor mode, the $\mathrm{𝖦𝖾𝗇}$ procedure has a property called index hiding: given $\mathrm{𝖼𝗋𝗌}$ (without ${\mathrm{𝗍𝖽}}_i$), it is computationally hard to find the binding index $i$.

• $\mathrm{■}$

  The $\mathrm{𝖡𝖠𝖱𝖦}$ has the somewhere argument of knowledge property: There exists an efficient auxiliary extraction procedure, $ℰ({\mathrm{𝗍𝖽}}_i,ℳ,\pi )\to w_i$, which satisfies the following. Suppose we call $\mathrm{𝖦𝖾𝗇}$ in trapdoor mode with a binding index $i$, and obtain $(\mathrm{𝖼𝗋𝗌},{\mathrm{𝗍𝖽}}_i)$. Given only $\mathrm{𝖼𝗋𝗌}$, it is computationally hard to find a proof $\pi$ that is accepted by the verifier, such that when we extract a witness $w_i$ using $ℰ({\mathrm{𝗍𝖽}}_i,ℳ,\pi )$, we have $ℳ(x_i,w)\ne 1$.