TritonVM / triton-vm

Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
https://triton-vm.org
Apache License 2.0
244 stars 36 forks source link

Missing authentication of a_values in the FRI rounds? #225

Closed yczhangsjtu closed 7 months ago

yczhangsjtu commented 1 year ago

Following is the loop through the rounds in the prover. Only the b_values are fed into enqueue_auth_pairs. https://github.com/TritonVM/triton-vm/blob/3331a8daea64404f9d521a809d4e8d992479ff54/triton-vm/src/fri.rs#L160-L172 Although the initial a_indices are enqueued, the new indices computed in each of the rounds are not. https://github.com/TritonVM/triton-vm/blob/3331a8daea64404f9d521a809d4e8d992479ff54/triton-vm/src/fri.rs#L154

Following is the loop through the rounds in the verifier. https://github.com/TritonVM/triton-vm/blob/3331a8daea64404f9d521a809d4e8d992479ff54/triton-vm/src/fri.rs#L346-L390 At the end of this loop a_indices and a_values are assigned the values of the c_indices and c_values. However, neither a_indices nor c_indices are authenticated against the Merkle roots.

jan-ferdinand commented 1 year ago

Thanks for the question!

The indices are deterministically, pseudo-randomly sampled using the Fiat-Shamir heuristic. The transcript at the point of index sampling contains the commitments to all the polynomials in all the rounds of FRI. Given the indices for round $n$, deriving the indices for round $n+1$ is deterministic as well.

Because the verifier computes the indices itself, no further authentication of the correctness is necessary; in a sense, computing them implies verification they were computed correctly.

jan-ferdinand commented 1 year ago

Perhaps some of the confusion comes from the name of the method enqueue_auth_pairs? The “pair” in that method's name does not refer to (indices, polynomial_evaluations_at_indices) but to (authentication_paths, polynomial_evaluations_at_indices).

aszepieniec commented 1 year ago

The issue that Yuncong is alluding to is (I think) the following:

It is not obvious that this variant as as secure as traditional FRI. However, I don't see how to attack it either.

The case where the TritonVM FRI verifier accepts but the traditional FRI verifier rejects implies A = C but for some reason this value disagrees with some codeword (or Merkle leaf) in an intermediate round. This would imply that the claim is true (the first codeword does have a low degree interpolant) but the malicious prover produces a faulty proof in order to trigger this disparity.

jan-ferdinand commented 1 year ago

Yuncong, apologies for reading your question incorrectly; for some reason, I thought you were talking about the indices, not the partially revealed codewords (or “values”).

Alan has summarized the difference beautifully. In addition to his justification, I can offer this picture of a proof sketch we did back we changed our FRI to what you describe above:

It's possibly not the cleanest way to write things up, but maybe it's convincing enough or can be used to construct something convincing; if the former, I'd be interested in creating the latter.

jan-ferdinand commented 12 months ago

Note that with the merging of #226 (61073e2), the code for FRI looks quite different but behaves as before. Notably, it should be a lot more explicit that the partial codeword “a” (what used to be called “a_values”) of the last round is computed, not received:

https://github.com/TritonVM/triton-vm/blob/61073e2b6666885ae1bfcab13656911242c81a71/triton-vm/src/fri.rs#L293-L298

Furthermore, the code now spells out more explicitly which partial codewords are received and authenticated:

https://github.com/TritonVM/triton-vm/blob/61073e2b6666885ae1bfcab13656911242c81a71/triton-vm/src/fri.rs#L307-L317

I'm aware none of this resolves the primary question (“Is it sound to compute the folded partial codeword instead of receiving, authenticating, and verifying it?”) but simply wanted to point out that even though the code has changed drastically, the behavior has not.

jan-ferdinand commented 7 months ago

Closing due to inactivity. Feel free to re-open if so desired.