Now is the time to learn and dive deep into ZK application development. A large class of security errors can crop up if you’re not careful when starting to build ZK applications. These issues often stem from having the wrong frame of reference in your head and paying attention to the wrong details. Read this article to learn about the mindset you need, and the gotchas to look out for when programming with zero-knowledge proofs.

Background

When I started working on what would become Mina Protocol in fall of 2017, writing applications using zero-knowledge in production was extremely rare. However, today there is a boom of ZK programming in the crypto/web3 space, and, soon, I believe there will be a boom in the web2 space too. Early on, to manage complexity of large ZK applications, developers needed to build their own DSLs and SDKs, but these days there are many to choose from: A few zkSecurity auditors including myself currently maintain SnarkyJS at O(1) Labs, for example. Tools like SnarkyJS or Noir or Cairo1.0 and execution runtimes like Mina Protocol or Aleo make it easier for developers to get started writing ZK applications — and they are starting! There are now ZK meetups, conferences, podcasts, workshops, hacker houses and companies, teams, and at this point an uncountable number of developers starting to use this technology first for fun, but then in production. If you’re curious, this is a great time to start yourself!

As David mentioned in ZK programmability adds a whole new layer to worry about, there are many facets of developing ZK applications where security issues can poison your application. I want to focus on sharing an understanding that prover computation must be fully constrained in your ZK application or you’ll be proving nonsense as this was something I personally struggled to really understand when I was first getting started with ZK programming five years ago.

Preliminaries

Let’s make sure we’re on the same page before we get into these under-constraining issues with some informal definitions:

A real-world ZK application is an application that includes a phase separation in computation between at least two parties — a prover and a verifier. Typically, the prover does extra work and is creating and manipulating and working with private data either for scalability or privacy purposes. The verifier can check a ZK proof that if defined and constructed correctly can efficiently verify computations without observing the private data. The verifier reasons about private variables as existentially quantified ones in other words thinking that “there exists some data, w, that the prover knows that I don’t, such that some properties hold on w”. Sometimes the values corresponding to the private variables are referred to as a witness since they act as a witness, a form of proof by evidence that the existential variables do exist. Note that the prover and verifier(s) don’t trust one another, and we must think adversarially — ie. that the prover will try to cheat the verifier if they are able.

Since the verifier computation does not work with the private data directly, rules for your application are imposed by introducing assertions or constraints about certain properties of the data. The implementation details of these constraints materialize differently in different proof systems, but if you are working with a decent SDK that abstracts away those details, most of the time you just need to think about what assertions you need.

Finally, under-constraining private data describes a class of security errors that arise when these existentially quantified variables do not have enough assertions about them for the verifier to properly enforce that the shape of the data is what is needed for applications.

When building a ZK application, you must constantly jump between the prover and verifier worlds. Different toolkits take different approaches to exposing these universes to their developers. For example, Noir assumes that prover computation happens elsewhere and Noir code just describes the verifier side of the computation.

// my current age is the sum of my age at account creation time and years since account created
// somewhere else: Go lookup the account information and check the signature before returning it, thread that value through your code until this function call

struct AccountInfo { startAge: Field, yearsSince: Field }

fn getMyAgeIfNotChild(retrievedAccountInfo : AccountInfo) -> Field {
   let age = retrievedAccountInfo.startAge + retrievedAccountInfo.yearsSince;
   assert(age >= 18);
   age
}

SnarkyJS, on the other hand, interleaves these worlds by asking the developer to witness the existential variables in order to simultaneously define the prover and verifier computations.

// my current age is the sum of my age at account creation time and years since account created

class AccountInfo extends Struct({ startAge: Field, yearsSince: Field }) {}

function getMyAgeIfNotChild(userid: String, serverPk: PublicKey): Field {
  const accountInfo = Provable.witness(AccountInfo, () =>
     const accountInfo = loadAccount(userid);
     if (!accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature])) {
       throw new Error("my account database is busted");
     }
     return new AccountInfo({ ...accountInfo });
  );

  const age = accountInfo.startAge.add(accountInfo.yearsSince);
  age.assertGreaterThanOrEqual(18);
  return age;
}

Common Mistake: Failing to recognize the prover/verifier phase separation

In either case, we can’t assume any properties hold on the data without checking them! For developers new to working with ZK, the biggest mistake I have seen which leads to underconstraining errors is failing to acknowledge this phase separation and thinking that the verifier side will inherit properties of the proving side of the computation. Acknowledge the difference! Did you catch that we forgot to constrain that the signature was valid inside the verification phase in the above examples?

// my current age is the sum of my age at account creation time and years since account created
// somewhere else: Go lookup the account information and check the signature before returning it, thread that value through your code until this function call

struct AccountInfo { startAge: Field, yearsSince: Field, signature: [u8;64] }

fn getMyAgeIfNotChild(retrievedAccountInfo : AccountInfo, serverPkX : pub Field, serverPkY : pub Field) -> Field {
   let chunk1 = retrievedAccountInfo.startAge.to_be_bytes(2);
   let chunk2 = retrievedAccountInfo.yearsSince.to_be_bytes(2);
   let data = combine_arrays(chunk1, chunk2); // assume combine_arrays exists
   verify_signature(serverPkX, serverPkY, retrievedAccountInfo.signature, data);

   let age = retrievedAccountInfo.startAge + retrievedAccountInfo.yearsSince;
   assert(age >= 18);
   age
}

// my current age is the sum of my age at account creation time and years since account created

class AccountInfo extends Struct({ startAge: Field, yearsSince: Field, signature: Signature }) {}

function getMyAgeIfNotChild(userid: String, serverPk: PublicKey): Field {
  const accountInfo = Provable.witness(AccountInfo, () =>
     const accountInfo = loadAccount(userid);
     if (!accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature])) {
       throw new Error("my account database is busted");
     }
     return accountInfo;
  );

  accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature]).assertTrue();

  const age = accountInfo.startAge.add(accountInfo.yearsSince);
  age.assertGreaterThanOrEqual(18);
  return age;
}

Ultimately, this is the root of all errors related to under-constraining. And, unfortunately, even with a good prover/verifier phase-separate mindset there is space for more subtle errors to slip in: Computations with private data can taint future assertions. This is best demonstrated through a few examples.

Division

The division operation is typically provided to you as a primitive in ZK languages. However, if we look at implementing it ourselves, it’s a nice example: One way to divide in a circuit is to structure the logic such that the prover computes division privately and then asserts correctness by verifying that this valued multiplied.

// dividend / divisor = quotient (in psedocode)
function unsafeDivide(dividend: Field, divisor: Field): Field {
  let quotient = witness { dividend / divisor };
  constraint(quotient * divisor == dividend);
  return quotient;
}

However, what about zero! Division is supposed to be undefined at zero. But if we pass zero as a divisor, we can prove anything is the quotient! This error typically leads to disastrous security issues.

To fix, we can make sure that the divisor can’t be zero:

// dividend / divisor = quotient (in psedocode)
function safeDivide(dividend: Field, divisor: Field): Field {
  let quotient = witness { dividend / divisor };
  constraint(quotient * divisor == dividend);
  constraint(quotient != 0);
  return quotient;
}

Square Root

The square root operation is also interesting. Similarly to division, we compute via inverse. Though, this time, square root is well-defined at zero. Due to nuances we won’t get into in this post, let’s just assume that we’ve already ensured that square root is defined at the input presented.

// sqrt(x) = root (in pseudocode)
function unsafeSqrt(x: Field): Field {
  let root = witness { sqrt(x) };
  constraint(root * root == x);
  return root;
}

More generally any invertible operation with a single deterministic output can safely be represented in this way when working with ZK. But wait, square root doesn’t have a deterministic output! Both positive and “negative” values are valid!

What does a “negative” value even mean in a field? The kinds of fields we use in practice are typically Z_p for some prime p. Essentially, positive integer values that wrap-around at p. So -root is equal to p - root. Since p is prime is must be odd, and this means that -root will have a different parity (odd vs even) than root. It suffices to check that the parity of input is the same as the root to find a reasonable canonical square root.

// sqrt(x) = root (in pseudocode)
function saferSqrt(x: Field): Field {
  let root = witness { sqrt(x) };
  constraint(root * root == x);
  constraint(parity(x) == parity(root));
  return root;
}

Review and Audit

In order to catch these under-constraining errors, it is important to have a strong review and audit process in place. For instance, at my day-to-day job working on Mina, I not only rely on third-party audits but also push my coworkers and myself to invest engineering time to audit our own ZK computations, looking for these kinds of under-constraining errors.

At zkSecurity, we have encountered many of these sorts of issues in real-world scenarios, and we are well-equipped to help you prevent such bugs from affecting your applications. Sometimes, having a fresh and experienced perspective can make all the difference in identifying potential issues. If you’re interested in our expertise, feel free to reach out to us at [email protected].

Conclusion

As more and more developers venture into building ZK applications, it is crucial for them to develop a deep understanding of the prover and verifier worlds. By recognizing their distinctions and remembering that the “do” is in secret, while assertions are the only thing verifiers see, developers can avoid common pitfalls.

Even with this mindset, it is important to remain vigilant about how certain partial operations can taint future assertions. Accepting that even the most diligent individuals can make mistakes is key to maintaining a strong development process. Always conduct code reviews and seriously consider getting an audit to ensure the security and correctness of your ZK applications. Our team at zkSecurity would be more than happy to assist you in your journey to building secure and efficient ZK applications.

As the world of ZK programming continues to grow, developers must remain mindful of the potential security issues that can arise. By understanding the nuances of ZK programming, leveraging the right tools and libraries, and investing in a robust review and audit process, developers can create secure applications that maximize the potential of zero-knowledge proofs.