$\newcommand{\pair}{\mathcal{e}}$ $\newcommand{\Gone}{\mathbb{G}_1}$ $\newcommand{\Gtwo}{\mathbb{G}_2}$ $\newcommand{\Gt}{\mathbb{G}_t}$ $\newcommand{\SP}{SnarkPack}$ $\newcommand{\vA}{\mathbf{A}}$ $\newcommand{\vB}{\mathbf{B}}$ $\newcommand{\vC}{\mathbf{C}}$
[TOC]
# SnarkPack Audit---Matteo Campanelli
Last Major Update: May 16th 2021
## Approach, Scope and Limitations of This Audit
- The general approach is convincing (as I elaborate below), so I focused on the specific building blocks, MIPP and TIPP
- Since MIPP and TIPP are mostly applications of the GIPA protocols in BMM+19, I mostly focused on the security aspects that were specific to SnarkPack. I have read the discussions and some of the proofs in BMM+19; I have not checked all their details.
- I have reviewed the top-level approach in the code---which seems correct. I spent additional time looking at the code portions related to the issues I mention below.
## Summary of This Audit
- The _overall_ approach of the SnarkPack protocol and its subprotocols look appropriate adaptations of the GIPA protocols in BMM+19.
- The non-interactive version presented in the document (the MT protocol) may not be applying the Fiat-Shamir transformation correctly.
- An earlier version of the document during this audit did not properly verify randomness-related challenges. This has been fixed during this audit.
I elaborate on some of the points above and others in the remainder of this report.
## The SnarkPack Construction
### Background
Groth16 is a popular zkSNARK based on pairings. Given a statement–instance pair $(x, \pi)$, a verifier can check it through the equation
$$ \pair(A,B) = Y e(C, D)$$
where $\pi := (A,B,C) \in \Gone\times\Gtwo\times\Gone$, $Y$ is computed from $x$ and $D$ is a constant in the SRS.
SnarkPack proposes a way to aggregate Groth16 proofs.
### Abstract Version of SnarkPack
The construction works roughly as follows.
Given $\mathbf{\pi} = (\mathbf{A}, \mathbf{B}, \mathbf{C})$ we do:
- Prover commits to $(\mathbf{A}, \mathbf{B})$ as $c_{AB}$; Commit to $\mathbf{C}$ as $c_C$
- Verifier (in the interactive version) sends random scalar $r$
- The prover sends $Z_{AB},Z_C$ correctly computed use commit-and-prove systems MIPP and TIPP to show that prover knows:
1. opening of $c_{AB}$ such that $e(\vA^\mathbf{r},\vB) == Z_{AB}$
2. opening of $c_C$ such that $\vC^\mathbf{r}$
where $\mathbf{r} := (r^1,\dots,r^n$)
- verifier checks the two proofs appropriately
The last two step is merged into one in the merged MIPP-TIPP but it's roughly the same.
### Security sketch (for abstract construction above)
If we assume the security of MIPP and TIPP and the binding of the respective commitment schemes they work on, then it is easy to argue knowledge soundness for the aggregation relation: the aggregation extractor uses the extractors for MIPP and TIPP to get all proofs. Then we invoke Schwartz-Zippel to claim the powers of the random challenge tests the AND of all verifications w.h.p.. (This security proof is in the ROM for the non-interactive version).
## On the Application of Fiat-Shamir
When applying Fiat-Shamir the first challenge should be computed including the whole public input to the verifier. It should be:
$$ H((T_{AB}, U_{AB}),(T_{C}, U_{C}), Z_{AB}, Z_C, r))$$
At the time of this writing [the code](https://github.com/filecoin-project/bellperson/pull/182) seems to be using an empty first input to the random oracle. It should be as above.
In the text this first challenge is undefined (step 5 of MT.Prove).
My suggestion in general is to change the text to an interactive version. Thus it can be easier to see how and where to apply Fiat-Shamir, especially if this protocol is composed with others. This may be useful in case of follow-up audits and in case the protocol is modified in the future.
I cannot come up with an attack on the above as of now, but I cannot argue its security otherwise.
**Note:** While writing this, this issue has already been fixed in the code. [Pull request 183](https://github.com/filecoin-project/bellperson/pull/183/files)
## Using r in MIPP-related Subprotocols
An earlier version of the protocol (then fixed in [this version](https://github.com/filecoin-project/bellperson/pull/182)) did not use the challenge $r$ (defined as in abstract construction above) properly during the verification of MIP. The same issue would arise in a certain form in the MT protocol.
It used to be that the prover would send a certain $r'$---an element related to $r$ and the challenges in the protocol---and the verifier would use that $r'$ in some exponentiation test without checking its honest computation. In MIPP overall the verifier would not use $r$ anywhere in its checks which could cause a malicious prover to make a statement about any vector $\mathbf{r}$.
The fix to the above (already implemented in both and text at the time of this writing) is for the verifier to compute honestly $r'$.
As discussed with Anca, it is possible that the MT protocol may not require such recomputation of $r'$ since that protocol already performs other checks related to $r$. Nonetheless, if one went in this direction, it should be proved that this preserves knowledge-soundness.
## Itemized List of Current Issues
On Fiat-Shamir:
1. (Critical) Change text so to apply Fiat-Shamir appropriately as described (define first challenge; use public input in it). Without that the described protocol should not be secure.
2. (Minor) The text has a few ambiguities w.r.t. hash functions. Some of these are probably just typos. The text uses $Hash_0,Hash_1, Hash_2, H$ for example, but $H$ is never introduced.
3. (Minor) Add an interactive version of the protocols to the text as it may be useful in case of future modifications.
On appropriately using $r$ in rescaled challenges:
4. (Major) One crucial part of of the protocols is the use of rescaled commitments keys. The rescaling also uses the challenge $r$ for polynomial $f_w$. The MT verifier in the text currently has no explicit rescaling of the keys. Please, also check TIPP for similar omissions. In general, it would be very useful to make explicit all the parameters that are passed around.
Others:
5. (Minor) Proof of Lemma 3 is correct, but is it possible that the statement should be for $q = n/2$ instead of $q=n$? Because in the assumption we assume access to $(2q-1)$-degree polynomials (in the exponent).
6. (Minor) Please fully state in what security model you are claiming the security of your protocols, under what assumptions, etc.