Audit of the Stwo-Cairo Verifier

Description.

Before drawing the interaction challenges, all the public claims about the execution trace are mixed in the Fiat-Shamir channel. This includes, in particular, all the public memory claims.

fn mix_into(self: @PublicMemory, ref channel: Channel) {
    let PublicMemory { program, public_segments, output, safe_call } = self;

    // Program is the bootloader and doesn't need to be mixed into the channel.
    let _ = program;

    // Mix public segments.
    public_segments.mix_into(ref channel);

    // Mix output memory section.
    channel.mix_memory_section(output);

    // Mix safe_call memory section.
    channel.mix_u64(safe_call.len().into());
    for (id, value) in safe_call.span() {
        channel.mix_u64((*id).into());
        // Mix each element of the array individually
        for val_element in (*value).span() {
            channel.mix_u64((*val_element).into());
        }
    }
}

Focusing on the output claim, it is a vector of pairs (memory_id, value). The mix_memory_section function mixes the memory ID values into the channel, but it does not mix the memory ID keys: notice how the first component of the pair is ignored in the following code.

fn mix_memory_section(ref self: Poseidon252Channel, data: @Array<(u32, [u32; 8])>) {
    // TODO(Gali): Make this more efficient.
    let mut flat_data = array![];
    for entry in data.span() {
        let (_, val) = entry;
        flat_data.append_span((*val).span());
    }
    self.mix_u32s(flat_data.span());
}

Later, interaction challenges are drawn from the challenge, and all the public memory claims are transformed into a vector of triples (address, memory_id, value) and are added into the LogUp sum. In particular, for the output claim, each pair (memory_id, value) is transformed into triples (final_ap + i, memory_id, value).

fn get_entries(
    self: @PublicMemory, initial_pc: u32, initial_ap: u32, final_ap: u32,
) -> Array<PubMemoryEntry> {
    let mut entries = array![];

    // [...]

    // Output.
    i = 0;
    for (id, value) in self.output.span() {
        entries.append((final_ap + i, *id, *value));
        i += 1;
    }

    // [...]
    entries
}

Then, for each triple (address, memory_id, value), the following LogUp sum is computed.

for entry in self
    .public_memory
    .get_entries(
        initial_pc: (*self.initial_state.pc).into(),
        initial_ap: (*self.initial_state.ap).into(),
        final_ap: (*self.final_state.ap).into(),
    )
    .span() {
    let (addr, id, val) = *entry;

    let addr_m31 = addr.try_into().unwrap();
    let id_m31 = id.try_into().unwrap();
    let addr_to_id = lookup_elements
        .memory_address_to_id
        .combine([addr_m31, id_m31])
        .inverse();

    // Use handwritten implementation of combine_id_to_value to improve performance.
    let alpha = *lookup_elements.memory_id_to_value.alpha;
    let mut combine_sum = combine::combine_felt252(val, alpha);
    combine_sum = combine_sum * alpha
        + id_m31.into()
        - *lookup_elements.memory_id_to_value.z;
    let id_to_value = combine_sum.inverse();

    sum += addr_to_id + id_to_value;
}

This sum roughly corresponds to the following equation:

where $\alpha$, $\beta$ and $z$ are challenges drawn from QM31. Our observation is that, in particular in the case of the output claim, the memory ID values are not mixed into the Fiat-Shamir channel, and thus can be changed by a malicious prover after knowing the interaction challenges, and in particular after knowing the values of $\alpha$, $\beta$ and $z$.

Impact. Since the memory ID values are not mixed into the Fiat-Shamir channel, the potential impact is that a malicious prover can manipulate the LogUp sum to be zero, even if the lookup relations are not satisfied. For the purposes of the attack, all address and values can be considered “fixed”, as they are included in the Fiat-Shamir channel before the interaction challenges are drawn. This means that the attacker succeeds in forging a proof if they can find values ${\text{id}}_1,{\text{id}}_2,\dots ,{\text{id}}_k$ such that the following equation holds:

where ${\gamma }_i$ and ${\chi }_i$ are constants over QM31 which can be computed after drawing the challenges, and $c$ is a target sum value also over QM31. The interesting part is that the values ${\text{id}}_1,{\text{id}}_2,\dots ,{\text{id}}_k$ have to be from the base field M31, which makes this equation non-trivial to solve. Therefore, intuitively for a solution to exist, the number of memory IDs $k$ must be at least $4$ to cover the degrees of freedom of the equation.

We provide one generic attack strategy, which can be used to solve this equation: the idea is to use a generic birthday paradox attack to find a $k$-sum. This attack is based on the Wagner’s attack described in this paper.

• The attacker precomputes lists of values $1/({\text{id}}_i+{\gamma }_i)+1/({\text{id}}_i+{\chi }_i)$ for all $i$. Since the values ${\gamma }_i$ and ${\chi }_i$ are effectively random, the list values can be thought as random.
• Now, the attacker needs to find values in those lists that sum to $c$, which is exactly an instance of the $k$-sum problem.

Interestingly, for a $4$-sum problem, the Wagner’s attack can be used to find a solution in $O(2^{n/3})$ time, where $n$ is the number of bits of the challenge space. In this case, the work required is roughly $2^{41}$. However, we conjecture that if we increase $k$ to be $2^{10}$, then the cost of the attack is reduced to approximately $2^{22}$, which is feasible on a modern computer.

As a final remark, this particular attack is completely generic, and we believe that more efficient attacks may exist, e.g., based on solving the equation directly using Groebner bases or other algebraic techniques.

Recommendation. We recommend to mix the memory ID values into the Fiat-Shamir channel, so that they cannot be manipulated after the interaction challenges are drawn.

Description. Several components of the Cairo AIR are optional. Whether or not the verifier adds those components is determined by the CairoClaim that is part of a Cairo proof:

pub struct CairoProof {
    pub claim: CairoClaim,
    pub interaction_pow: u64,
    pub interaction_claim: CairoInteractionClaim,
    pub stark_proof: StarkProof,
}

For example, claim.blake_context.claim is of type Option<BlakeClaim>, and if the option is None, the Blake components are not added; which means the verifier will not include the components’ constraints in the composition polynomial.

impl BlakeContextComponentsImpl of BlakeContextComponentsTrait {
    fn new(
        claim: @BlakeContextClaim,
        interaction_elements: @CairoInteractionElements,
        interaction_claim: @BlakeContextInteractionClaim,
    ) -> BlakeContextComponents {
        if let Some(claim) = claim.claim {
            BlakeContextComponents {
                components: Some(
                    BlakeComponentsImpl::new(
                        claim,
                        interaction_elements,
                        interaction_claim.interaction_claim.as_snap().unwrap(),
                    ),
                ),
            }
        } else {
            BlakeContextComponents { components: None }
        }
    }

A CairoProof also holds a CairoInteractionClaim that contains the claimed LogUp sums of all components, and similarly contains options for sums of optional components. If the claimed sum of an optional component is present, it is added to the overall LogUp sum:

pub fn lookup_sum(
    claim: @CairoClaim,
    elements: @CairoInteractionElements,
    interaction_claim: @CairoInteractionClaim,
) -> QM31 {
    // ...

    sum += interaction_claim.blake_context.sum();

    // ...
}

// ...

impl BlakeContextInteractionClaimImpl of BlakeContextInteractionClaimTrait {
    // ...

    fn sum(self: @BlakeContextInteractionClaim) -> QM31 {
        if let Some(interaction_claim) = self.interaction_claim {
            interaction_claim.sum()
        } else {
            Zero::zero()
        }
    }
}

The issue is that the verifier never checks that optionality of components and their corresponding sums is consistent with each other. Specifically, the prover can set the Blake interaction claim to Some(value) even if the Blake claim is None. In that case, the interaction claim is added to the overall sum but is not constrained in any way, because the components that would normally constrain it are missing. That makes it easy for the prover to manipulate the total LogUp sum.

Almost all optional components are affected by this issue:

• Pedersen
• Poseidon
• Blake
• Opcodes
• all builtins

The case of Pedersen, Poseidon, and builtins is similar to Blake, where options for claim and interaction claim are not checked to be consistent.

For opcode components, the proof contains a vector of claims, which leads to a vector of components to be added, and similarly there’s a vector of interaction claims. However, the lengths of claims and interactions claims are not checked to be equal, so the prover can add extra unconstrained terms to the LogUp sum by appending them to the interaction claims vector.

The only optional components not vulnerable are the memory_id_to_value components, that also come with vectors of claims and interaction claims. In this case, the issue is prevented by the following consistency check (in CairoAirNewImpl::new()):

assert!(
    cairo_claim
        .memory_id_to_value
        .big_log_sizes
        .len() == interaction_claim
        .memory_id_to_value
        .big_claimed_sums
        .len(),
);

Impact. The issue enables attackers to forge proofs that are invalid in a number of ways.

As a proof-of-concept, we modify the prove_cairo() function to generate a valid proof for an incorrect output claim of the example Cairo program included in the repository. The modified prover performs the following operations:

• It arbitrarily changes the first output value claim.
• It computes the interaction challenges, and then compute the original LogUp sum, which will not be zero.
• At this point, it adds a claimed_sum value in an unused interaction claim set to exactly the negative of the modified LogUp sum, so that the final LogUp sum is zero.

In the end, verification passes thanks to the zero LogUp sum, despite the incorrect output claim.

pub fn prove_cairo<MC: MerkleChannel>(
    input: ProverInput,
    pcs_config: PcsConfig,
    preprocessed_trace: PreProcessedTraceVariant,
) -> Result<CairoProof<MC::H>, ProvingError>
where
    SimdBackend: BackendForChannel<MC>,
{
    // [...]

    // Run Cairo.
    let cairo_claim_generator = CairoClaimGenerator::new(input);
    // Base trace.
    let mut tree_builder = commitment_scheme.tree_builder();
    let span = span!(Level::INFO, "Base trace").entered();
-   let (claim, interaction_generator) = cairo_claim_generator.write_trace(&mut tree_builder);
+   let (mut claim, interaction_generator) = cairo_claim_generator.write_trace(&mut tree_builder);
    span.exit();
+
+    // Modify the first output value claim to be another value, e.g., 0x41.
+    claim.public_data.public_memory.output[0].1 = [0x41, 0, 0, 0, 0, 0, 0, 0];

    claim.mix_into(channel);

    // [...]

-    let interaction_claim =
+    let mut interaction_claim =
        interaction_generator.write_interaction_trace(&mut tree_builder, &interaction_elements);
+
+   // since we modified an output claim, the lookup sum will not be zero
+   let modified_lookup_sum = lookup_sum(&claim, &interaction_elements, &interaction_claim);
+   println!(
+       "Modified lookup sum: {}",
+       modified_lookup_sum.to_string()
+   );
+
+   // Add an unused claimed sum to make it zero.
+   // In this specific case, the add_mod_builtin is null in the
+   // original proof.
+   interaction_claim.builtins.add_mod_builtin = Some(InteractionClaim {
+       claimed_sum: -modified_lookup_sum
+   });

    // [...]

    // Validate lookup argument.
    debug_assert_eq!(
        lookup_sum(&claim, &interaction_elements, &interaction_claim),
        SecureField::zero()
    );

    interaction_claim.mix_into(channel);
    tree_builder.commit(channel);

    // [...]

    Ok(CairoProof {
        claim,
        interaction_pow,
        interaction_claim,
        stark_proof: proof,
    })
}

The output of the prover is the following:

Modified lookup sum: (704398217 + 987329512i) + (1683849168 + 1389614104i)u
New lookup sum: (0 + 0i) + (0 + 0i)u

and the modified proof is accepted by the verifier.

Recommendation. Add consistency checks for all optional components, which guarantee that if a component is not used, its LogUp sum contribution is zero.

Description. Some instances of hashes in the code base exhibit collisions due to zero padding. For example, hash_node() in poseidon_hasher.cairo:

    if !column_values.is_empty() {
        let mut word = (*column_values.pop_front().unwrap_or(@BaseField { inner: 0 }))
            .inner
            .into();

        for _ in 1..M31_ELEMENTS_IN_HASH {
            let v = (*column_values.pop_front().unwrap_or(@BaseField { inner: 0 }))
                .inner
                .into();
            word = word * M31_SHIFT + v;
        }

        hash_array.append(word);
    }

Note that zeros replace any elements missing to make the input length a multiple of M31_ELEMENTS_IN_HASH = 8. In particular, inputs like [1] and [1,0] and [1,0,0] will all yield the same hash value.

This particular zero-extension collision was fixed in a commit shortly after the audit freeze, but another collision is still present in the same function : The special case where there are no child nodes and exactly 4 column values [v0, v1, v2, v3] seems to collide with the case of 8 column values [v0, v1, v2, v3, 0, 0, 0, 0].

A similar zero-extension collision happens in mix_u32s() in the Poseidon channel implementation, where input u32s are zero-padded up to a multiple of 7. In current usage of mix_u32s(), this should not present an issue.

A slightly different type of hash collision is prevalent throughout cairo_air/src/lib.cairo: Collisions due to flexible data structures, where only the content but not the exact structure serves as hash input. For example, this is how the PublicSegmentRanges are mixed into the channel:

impl PublicSegmentRangesImpl of PublicSegmentRangesTrait {
    fn mix_into(self: @PublicSegmentRanges, ref channel: Channel) {
        for segment in self.present_segments() {
            segment.mix_into(ref channel);
        }
    }

The return value of present_segments() is some sublist of 11 different public memory segments, 10 of which are optional. The hash cannot distinguish which of the segments are present.

Similarly, when optional claims are mixed into the channel, it looks like this:

impl BuiltinsClaimImpl of BuiltinsClaimTrait {
    fn mix_into(self: @BuiltinsClaim, ref channel: Channel) {
        if let Some(claim) = self.add_mod_builtin {
            claim.mix_into(ref channel);
        }
        if let Some(claim) = self.bitwise_builtin {
            claim.mix_into(ref channel);
        }
        if let Some(claim) = self.mul_mod_builtin {
            claim.mix_into(ref channel);
        }
        // ...

There are hash collisions because, for example, values of self.add_mod_builtin = Some(X) and self.bitwise_builtin = None yield the same hash as self.add_mod_builtin = None and self.bitwise_builtin = Some(X).

Other optional claims like BlakeContextClaim, PoseidonContextClaim and memory_id_to_big::Claim have the same issue. On the other hand, OpcodeClaim avoids the issue by mixing the length of vectors into the channel together with their content.

Impact and recommendation. We did not find a way to exploit any of the hash collisions found. However, given how prevalent these collisions are and how they could interact in complex ways, we believe it would be safer to remove them. In general, this is easily accomplished by hashing an indicator of the data structure along with the data itself, such as the length of an input array or a bit in the case of an option.

Description. In the Poseidon channel implementation, draw_base_felts() first draws a felt252 and from that extracts 8 M31 elements:

fn draw_base_felts(ref channel: Poseidon252Channel) -> [M31; FELTS_PER_HASH] {
    let mut cur: u256 = draw_secure_felt252(ref channel).into();
    [
        extract_m31(ref cur), extract_m31(ref cur), extract_m31(ref cur), extract_m31(ref cur),
        extract_m31(ref cur), extract_m31(ref cur), extract_m31(ref cur), extract_m31(ref cur),
    ]
}

// ...

fn extract_m31(ref num: u256) -> M31 {
    let (q, r) = DivRem::div_rem(num, M31_SHIFT_NZ_U256);
    num = q;
    M31Trait::reduce_u128(r.low)
}

extract_m31() works by

• extracting the first 31 bits of the input: div_rem() by M31_SHIFT_NZ_U256$=2^{31}$ in the code above, and
• reducing the result modulo the M31 field; this happens inside reduce_u128().

Since $(2^{31}-1)mod\text{M31}=0$ while $xmod\text{M31}=x$ for all other 31-bit strings, this operation introduces a bias: Drawing 0 is twice as likely as drawing any other M31 element.

Impact. The chance for the prover to draw a zero base felt is $2^{-30}$ instead of the ideal $2^{-31}$. When drawing a QM31 extension field element, which uses the first 4 outputs of draw_base_felts(), the chance of drawing an overall zero is $2^{-120}$ instead of $2^{-124}$. Drawing 0 for a challenge in any place likely lets an attacker forge an invalid proof, so the bias reduces the maximum security level that Stwo can target, by 4 bits.

Recommendation. The blake2s channel implementation already handles the bias correctly by rejecting samples that fall outside a multiple of the M31 range. We recommend to do the same for Poseidon.

Description. In the Cairo version of verify_cairo(), the validity of preprocessed traces is checked by comparing the preprocessed root to a hard-coded value (which depends on the blowup factor).

// Preprocessed trace.
let expected_preprocessed_root = preprocessed_root(pcs_config.fri_config.log_blowup_factor);
let preprocessed_root = stark_proof.commitment_scheme_proof.commitments[0].clone();
assert!(preprocessed_root == expected_preprocessed_root);

The same check is missing from the Rust version of verify_cairo().

Impact. The values in preprocessed traces are not determined by polynomial constraints, but hard-coded to specific values. A check like the above is therefore essential, otherwise the prover can set the values in preprocessed traces arbitrarily.

The issue is only marked with low severity because the Rust verifier was outside the audit scope and we are told it is mainly intended for debugging.

Recommendation. Add the missing check in the Rust verifier.

Description. In verify_values(), the implementation zips self.trees (an array of length 4, created by the verifier) with queried_values which is taken from the proof. If the prover supplies queried_values shorter than self.trees, zip() will only iterate up to the shorter length. This causes the verifier to skip tree.verify() on some of the trees, which is one of the core checks in the protocol.

for (tree, queried_values) in self.trees.span().into_iter().zip(queried_values.span()) {
    let decommitment = decommitments.next().unwrap();

    // The Merkle implementation pops values from the query position dict so it has to
    // be duplicated.
    let query_positions = query_positions_by_log_size.clone_subset(unique_column_log_sizes);

    tree.verify(query_positions, *queried_values, decommitment);
}

Impact. There is no concrete impact, because insufficient numbers of trees in queried_values will later cause queried_values_at_row in accumulate_row_quotients() to be shorter than expected, and cause an array out-of-bounds error. This can’t be circumvented by the prover, so it is not possible to get the verifier to succeed after skipping Merkle opening checks.

However, this failure seems coincidental and could be accidentally removed by refactoring accumulate_row_quotients(), in which case the skipped checks would be catastrophic.

Recommendation. In general, data from the proof should be validated before it is allowed to structure the verifier algorithm. In the case of zip(), we recommend to assert that the lengths of the zipped arrays are equal.

assert!(self.trees.len() == queried_values.len());

for (tree, queried_values) in self.trees.span().into_iter().zip(queried_values.span()) {
  // ...

Description. The Stwo whitepaper features the concept of a channel $ℒ$ that captures communication between AIR tables: Each gate/table can use a number of elements from the channel, as well as yield other elements to the channel:

The paper allows each of these vectors to be of its own dimension.

The flat AIR relation requires that the set of all used elements, from all tables, is contained in the set of all yielded elements:

Note that here we are potentially trying to equate vectors of different dimension.

In the IOP, vectors $(z_0,\dots ,z_{n-1})$ are reduced to scalars by summing over elements times powers of a challenge, $z_0+\alpha z_1+\dots +{\alpha }^{n-1}{z}_{n-1}$. These scalars participate in a shared LogUp protocol.

The problem is that vectors of different dimensions can interact in the LogUp sum if one of them has trailing zeros, e.g. a vector $(z_0,0)$ interacts with a scalar $z_0$ because $z_0+\alpha 0=z_0$. On the other hand, $(z_0,0)$ can not interact with $z_0$ in the original “uses $\subseteq$ yields” inclusion.

This means we have a soundness issue: the LogUp relation can be satisfied even if the original inclusion relation isn’t.

In particular, Lemma 5 (Soundness, Round 1a) in Appendix A.4 of the paper is false. To give a simple counter-example, assume that we have a single table of two columns $(x_i,y_i)$ of length $N$, a single “use” constraint $U(x,y)=(x,y)$, a single “yield” constraint $V(x)=x$, and constant yield multiplicities $m_i=1$. Then Lemma 5 claims that the equality of rational functions

implies the set inclusion $\{(x_i,y_i):i<N\}\subseteq \{x_i:i<N\}$. This is clearly not true because the rational function equation can be satisfied with $y_i=0$ for all $i$, while the set inclusion is never satisfied (for $N>0$).

Impact. Implementing lookup channels of heterogeneous dimension as specified by the whitepaper would not be secure. For stwo-cairo, there is no impact, because all existing lookup relations use the same dimension everywhere.

Recommendation. There are ways to fix the IOP to incorporate multiple dimensions. For example, the dimension could be aggregated into the scalar: $n+\alpha z_0+\dots +{\alpha }^n{z}_{n-1}$.

However, it’s questionable to us if different dimensions in one lookup relation are even useful. An alternative would be to remove this possibility from the flat AIR definition.

Description. The zero check (composition) round of the Stwo protocol as implemented in code deviates from the description given in the Stwo whitepaper (Protocol 1).

In particular, the whitepaper specifies that the prover sends commitments to the quotient polynomials $q^{(1)},\dots ,q^{(\tau )}$ corresponding to each of the $\tau$ AIR components. The verifier then performs the point evaluation and zero check for each table individually.

On the other hand, the stwo-rs and stwo-cairo provers both send a single commitment to the batched composition quotient.

Impact. The security analysis of the protocol implemented in code differs from that presented on paper.

Our intuition is that the paper version of the protocol admits a simple, straightline method for extracting individual composition quotients by leveraging the extractability of Merkle tree in the ROM. In contrast, the code version might require a rewinding argument to recover the individual composition quotients from the batched composition quotients. We do not assess whether the (round-by-round) security proof requires to extract individual composition quotients or whether rewinding security proofs are suitable to prove the desired real-world security properties of Stwo.

Recommendation. Align the paper and code to follow the same method. The choice of method should be dictated by the proven security properties that are required of the real-world deployment of stwo-cairo.

Description. In the Poseidon version of hash_memory_section(), individual memory values represented as 8 u32s are concatenated into a single felt252 by construct_f252(), to compute the hash input.

The concatenation effectively takes the input modulo the 252-bit field, and therefore causes hash collisions between memory values that are a multiple of $p_{252}$ (the felt252 prime) apart.

This could have an impact in two possible scenarios:

• The input memory values are unchecked and can occupy the full 256-bit range. In this case, there are up to $\lceil 2^{256}/p_{252}\rceil =32$ collisions per unique memory value.
• The input memory values are independently checked to fit in 28 9-bit limbs, as is done in the “memory id to big value” tables. In this case, since $9·28=252$ and $p_{252}$ is just slightly larger than $2^{251}$, there are 2 collisions for most unique memory values.

Impact. In the code base at the time of audit, there is no issue, because the only memory values fed to hash_memory_section() are the contents of the public program, which are forced to consist of small values by the constraints of the verify_instruction table. However, the function seems to be intended to hash any memory section, and care will be required when applying it to arbitrary memory values in the future.

Recommendation. Only pack 7 u32s into one felt252 instead of 8, as is already done in mix_u32s().

Description. The Stwo whitepaper’s presentation of the LogUp part of Protocol 1 is less general than what is actually implemented.

The whitepaper (in Definition 6) specifies a flat AIR to consist of a single lookup relation where the union over all “uses” are contained in the union over all “yields”:

However, to implement the Cairo AIR, stwo-cairo needs multiple lookup relations, each with their own independent use-yield inclusion. (In the code, independent relations are tagged with identifiers like “Opcodes”, “MemoryIdToBig”, “VerifyInstruction”.) Using terminology from the paper, the Cairo AIR actually features multiple lookup channels $ℒ$.

This generalization is not as straight-forward as it sounds, because instead of constraining the LogUp sums of each channel separately, the implementation sums them all together. Therefore, the claimed sum for every table combines the LogUp terms of all channels appearing in that table. In the end, the verifier checks that the sum total of these claimed sums equals zero.

As we argue in the introduction, this is sound if a unique pair of interaction challenges is used for each lookup channel. This is exactly what the code does.

Impact. The soundness analysis of the paper doesn’t cover the case of combining multiple lookup channels in the same LogUp sum, so it falls short of establishing soundness of the implemented protocol.

Recommendation. Align the paper with the code and cover the case of multiple lookup channels.

Description. The whitepaper specifies the following constraints to verify the LogUp relation:

In particular, there are boundary constraints to fix running sums $w^{(t)}$ to the initial value of $0$ and final value of ${\gamma }_t$.

Instead, stwo-cairo uses the following, single constraint:

where $N_t=2^{n_t}$ is the column size. This works as well because, when summing that equation over all rows, the $w^{(t)}$ terms wrap around and cancel out, resulting in the correct equation for ${\gamma }_t$:

Interestingly, in this formulation the verifier doesn’t care about the values of $w^{(t)}$ modulo any constant added to the entire column.

Recommendation. Update the paper to follow the same method as the code.

Description. The vector commitment scheme being used is a non-standard variant of Merkle trees. To the best of our knowledge, there are no security proofs for the extractability of such commitments or whether an IOP can be compiled to a SNARK/STARK using such commitments.

Impact. The code’s security properties may differ from the proven security in the whitepaper.

Recommendation. Prove that these multi-vector and multi-sized Merkle commitments are extractable.

Description. The formula used to compute the security level of the polynomial commitment scheme (PCS) makes multiple assumptions:

1. the calculation assumes that the PCS soundness error is dominated by the ${(1-\theta )}^s$ term from the FRI soundness error.
2. the calculation assumes that a strengthened version of the cross-domain correlated agreement theorem holds for distance parameters up to the capacity bound for Reed-Solomon codes (and therefore Circle codes).

See fn security_bits in verifier_core/src/pcs.cairo.

Impact. These assumptions will lead to a miscalculation of the security level for users who want to operate within proven security regimes or who wish to target higher security guarantees.

For example, a user may increase the number of repetitions of the FRI query phase n_queries in hope of increasing the security level by log_blowup_factor * n_queries bits. However, it may be the case that eventually n_queries becomes large enough that the FRI soundness error is dominated by other terms (e.g., the folding phase). In an extreme scenario, the increase in n_queries might not change the security level at all.

Recommendation. Clearly document the assumptions underlying the security bits calculation and provide users with guidance on how to set parameters to achieve their desired security level.