To answer every part of this question in full details would require almost a book. Here, I’ll attempt to address all sub-questions and give a brief summary together with pointers each time. If you want me to develop some specific aspect, you can ask in the comments. Most of what I will say will not be specific to proving knowledge of a SHA-256 preimage, but follows from general results about zero-knowledge proofs.
EDIT: Bottom Line
Since my answer is long, here is a shorter bottom line:
There exists zero-knowledge proofs of knowledge for arbitrary NP statements (in particular, proving knowledge of a preimage to SHA256) with
- Tiny information flow (e.g. 768 bits in total, independently of the size of the statement)
- Minimal interaction (single round, assuming a global trusted reference string available to all parties)
- "Implementable" concrete efficiency (like, those proofs systems have been implemented, are used, and have reasonable performances on sufficiently simple statements)
- Bonus point : these proof systems (typically, SNARKs) have a tiny verifier computation (even shorter than checking that the statement is true given the witness!)
However, these "optimal features" come usually at a cost: high prover computation. The prover cost is often "asymptotically reasonable" (e.g. quasilinear in the size of the circuit checking the statement), but concretely very high (large constants are involved). Therefore, in practice it will most commonly be the case that one will prefer to give up on some of these optimal features, in exchange for a more reasonable prover cost. For example, the NIST candidate post-quantum signature Picnic v2 uses the latest developments in the line of work on ZK proofs from MPC-in-the-head (a line of work to which ZKBoo belongs), which leads to a proof linear in the size of the circuit, but much better computational costs. There are also tradeoffs, like Ligero, with "intermediate" prover costs, and smaller proof sizes on large instances (square root of the circuit size).
Additional Note: this is completely orthogonal to your question, but since you mention explicitly SHA256, you might be interested in knowing that there are important and fruitful lines of work that pursue the opposite direction: building new candidate collision-resistant hash functions (or block ciphers, stream ciphers, etc) which are zero-knowledge-friendly, in the sense that their structure is tailored to some existing zero-knowledge proof systems and seek to optimize the efficiency of proofs for these primitives. Standard examples include LowMC, Rasta, Trivium, Kreyvium, and many others. For example, the Picnic NIST candidate signature scheme is in fact a proof of knowledge of a preimage of a LowMC-based hash function.
Below is the detailed answer to the question.
Are there firm lower bounds on the necessary information flow in both
directions, number of exchanges, and probability $\varepsilon$ of reaching a
wrong conclusion?
This is a deep and vast question. Let me cut it into pieces.
Are there firm lower bounds on the number of exchanges?
What follows should also answer your last question:
Independently, can such proof be non-interactive (becoming a static
proof that knowledge of m hashing to ℎ was used in making the proof,
with no indication about the proof's origin or freshness)?
I gave some partial answer to this question here. The answer changes fundamentally if we assume that the parties are given access to some common reference string (CRS), generated honestly and given to all parties before the start of the protocol, or if we consider zero-knowledge in the plain model (where we do not assume a CRS, or any other trust assumption). Quoting from my answer:
Without a CRS:
« Assuming only one-way functions, we need a superconstant number of rounds to get zero-knowledge proofs for NP. Assuming further the existence of collision-resistant hash functions, we can build five rounds zero-knowledge proofs for NP. This is essentially the best we can hope for: under black-box simulation, a 4-round zero-knowledge proof for NP would collapse the polynomial hierarchy (but there exists some candidate constructions based on exotic assumptions, such as knowledge-of-exponent assumptions or keyless multi-collision resistant hash functions, with non-black-box simulation). Even with non-black-box simulation, a 3-round ZK proof for NP would break indistinguishability obfuscation. Furthermore, 2-round ZK proofs can simply not exist for languages outside BPP. »
With a CRS:
« Every language in NP has a non-interactive (1-round) zero-knowledge proof, under standard assumptions (e.g. factorization). »
Hence, without a CRS, 2 rounds is hopeless and 3 rounds seems very unlikely; with a CRS, one round suffices under standard assumptions.
(cautionary note: for the sake of simplicity I did not distinguished between common reference strings and common random strings; if one wants to delve into the full details of these characterization, this difference matters, but it is not of utter importance for a high level overview).
Are there firm lower bounds on the necessary information flow in both directions?
A trivial lower bound is that to reach soundness error $\varepsilon$, the total length of the prover messages must be at least $\log(1/\varepsilon)$: by the zero-knowledge property, there must exist one sequence of messages that cause the verifier to accept, even when proving a wrong statement (otherwise, we could not simulate), and just guessing this sequence would already contradict the soundness error bound if the total length is less than $\log(1/\varepsilon)$.
In fact, we cannot do much better - because we know zero-knowledge proof with very small information flow. Much, much smaller than the size of the statement itself. More precisely:
Interactive setting:
In the interactive setting, assuming collision resistant hash functions, every length-$n$ statement in NP can be proven in zero-knowledge using only $O(\log n)$ bits of total communication. This is the famous Killian protocol.
Non-interactive setting:
In the non-interactive setting (one round of communication, but we assume a CRS, which is necessary), this is more messy. In the random oracle model, you can apply the Fiat-Shamir heuristic and make Killian’s protocol non-interactive. This gives you a heuristic candidate non-interactive zero-knowledge argument (NIZK) with $O(\log n)$ communication.
But we can do even better!
Assuming a specific and very strong ‘knowledge of exponent’ assumption, there exists a NIZK proof system for any statement in NP, with total communication of 4 group elements - i.e., 1024 bits of total communication for any statement (assuming a 256-bit elliptic curve).
In the generic group model (which gives a heuristic construction in the standard model), we can even go further down, to only three group elements (768 bits).
Can we go even lower? A single element is impossible (in a model that treat the group as a black box). 2 group elements is open, as far as I know.
Eventually, assuming the very strong notion of indistinguishability obfuscation (iO), we can achieve optimally small NIZKs in the designated-verifier setting (where the verifier is allowed to have a secret key to check the proof): under iO, there is a designated-verifier NIZK which achieves soundness $1/2$ with a single bit of communication (hence, by parallel amplification, it achieves soundness error $\varepsilon$ with a communication $\log(1/\varepsilon)$). Since iO is completely inefficient, this construction is only of theoretical interest.
Summary: under strong assumptions and assuming a CRS, we can have both minimal communication and minimal interaction.
How far from that are current implementations?
It depends how computationally efficient you want your system to be - i.e., are you willing to pay for having small communication?
Succinct non-interactive proofs of knowledge (SNARKs), with constant-size proofs, are implemented and available. Here is an example; but since SNARKs are used in important applications, such as the cryptocurrency zcash, there are probably dozen of implementations available. Many should achieve constant size proofs, with 768 or 1024 bits in total.
However, the above solutions will usually be computationally very heavy on the prover side (not even mentioning that it relies on rather extreme assumptions). If you want better computational efficiency, it is common to trade it for proof size, and rely on proof systems with larger proofs (but smaller prover computation). ZKBoo is one possible choice, but it’s not state of the art anymore. The latest result in this line of work is the scheme of Katz et al, which refines ZKBoo and ZKB++ by introducing new techniques to improve the MPC-in-the-head paradigm on which these proof systems rely. The resulting proof is still of size linear in that of the boolean circuit computing the function you care about (in your case, SHA256), but with much smaller constants and a much better soundness error. This result is the basis of the latest version of the Picnic NIST candidate post-quantum signature scheme Picnic v2. This candidate has been fully implemented, optimized, and benchmark, and you should find all the data you want in their detailed specifications.
(Quick note: all the above are described as NIZK, but what they do is in fact constructing an interactive zero-knowledge proof system, and then making it non-interactive and heuristically secure using the Fiat-Shamir heuristic).
There are many other tradeoffs in between SNARKs and Picnic. Here, I could mention dozen of candidates (Aurora, STARKs…). One particularly interesting « middle spot » is Ligero: it achieves proof size $O(\sqrt{|C|})$ ($C$ being the boolean circuit computing SHA256, in the concrete case you consider), at reasonable computational costs. Actually, this protocol was used as the basis for a company providing solutions for decentralized anonymous cryptocurrencies.
Answering questions from the comments
One thing I do not get is which techniques would "just" encode SHA-256 as a boolean-SAT problem, or if (and how and to what degree) it is critical to make use of regularities. Like a lot of XOR, or a lot de 32-bit additions can come for free according to section 5.1 there. This matters because I could come with an approximation of the size fo SHA-256 as 3-SAT, but I do not understand if that's relevant.
Right, theoretical cryptographers have a tendency to forget about the "practical" issue of encoding your instance into the appropriate model the ZK proof is built upon :) But here are some details:
- protocols built from the MPC-in-the-head technique (ZKBoo, ZKB++, Picnic, Picnic v2) can essentially benefit from any "MPC-style" optimization. There are way too many variants of MPC protocols to cover every subtlety, but a good rule of thumb is as follow: MPC will deal with boolean circuits, or arithmetic circuits. XORs, or additions, will cost nothing. The default "cost" is the number of ANDs, or multiplications. If your function is well written as a mixture of arithmetic and boolean operations (like, XOR, AND, and addition over $\mathbb{Z}_{32}$), then you can use MPC protocols tailored to evaluate these operations efficiently. But I cannot tell you by default what will be the best choice: that depends on the current MPC literature, and that's hundreds of new papers per year.
If I use the Picnic signature scheme as an example, they use an MPC protocol which works especially well when the circuit is a boolean circuit, with XOR and AND gates, with an arbitrary number of XOR gates but as little AND gates as possible. This is why they replace SHA256 by another hash function, LowMC, chosen to minimize the number of AND gates in its boolean circuit.
- SNARKs, which achieve minimal proof sizes, rely on a different representation: quadratic span programs. Hence, to get a SNARK for SHA256, you must first encode SHA256 as a quadratic span program. I do not know how efficiently this can be done, but it has already been done: SHA256 is implemented in libsnark.
- Ligero relies on representing the function (e.g. SHA256) as an arithmetic circuit. Then, for each gate of the circuit, a constraint is added to some list of constraint, depending of the gate type, and an "Interactive PCP" is built on top of this representation as a list of constraints. As for ZKBoo and others, they can get a better result by not decomposing the additions over $\mathbb{Z}_{32}$ as XOR and ANDs, but by treating these ring additions as individual constraints directly (see the Ligero paper, page 2100). SHA256 is explicitly used as a benchmark in their paper: they achieve proof size 34kB, prover runtime 140ms, and verifier runtime 62ms.
Answering more globally the first part of your question:
One thing I do not get is which techniques would "just" encode SHA-256 as a boolean-SAT problem, or if (and how and to what degree) it is critical to make use of regularities.
All techniques can "just" encode SHA256 into the right representation (boolean circuit, arithmetic circuit, or quadratic span program). All concrete implementations will try to optimize as much as they can this representation ,e.g. by finding a way to deal directly with the ring operations involved in SHA256. Unfortunately, people do not usually implement the "naive, brainless" representation together with the optimized one, so it is hard to estimate what is the cost of not optimizing the representation. But just to give a very rough sense of it, naively representing SHA256 solely with XOR and ANDs can give a representation up to two orders of magnitude larger than when dealing with the ring additions in a more clever way.
