Adversarial Audit of Ironwood's Formal Verification

We subjected Ironwood's formal verification to an unprecedented, exhaustive third-party audit. No soundness issues were discovered.

Zcash's largest shielded pool, Ironwood, is formally verified, ruling out the possibility of undetectable counterfeiting bugs. In a traditional software audit, a team of experts scours the code for security flaws. Formal verification goes further: it captures the protocol's intended behavior in precise mathematical terms, then proves that the implementing code matches that specification.

On its own, though, "formally verified" says very little. A machine-checked proof establishes with certainty that a piece of software satisfies some security or correctness property. But is that property defined correctly, or is the claim vacuous? And is the software that ships actually the subject of the analysis?

Project Tachyon contracted zkSecurity, the leading auditing and formal analysis firm for ZK proofs, to audit the formal verification of Ironwood's zk-SNARK. Rather than reviewing the protocol and implementation for conventional bugs, they red-teamed the verification itself: they hunted for flaws in the proof structure that would allow a soundness bug to pass unnoticed. We are not aware of any prior audit that attacked a machine-checked security proof this way.

zkSecurity · Technical report Adversarial Testing of the Ironwood Formal Verification Download the report ↓

zkSecurity maintains a large repository of known ZK vulnerabilities that they and others have found in zk-SNARKs and arithmetic circuits. Using these as a guide, they injected soundness flaws of many kinds into the Ironwood zk-SNARK construction and checked whether the machine-checked proof still went through.

The audit found no soundness bugs that escaped Ironwood's formal verification, and no plausible attack that invalidates its formalized soundness guarantees. What they did find were some theoretical gaps, many of independent interest. We hope that this audit serves as a foundation for future analysis of Zcash and other protocols.

From zkSecurity's report:

During the audit we did not find any ability to bypass the formal verification within the scope, beyond the known limitations of the formalization itself. Conversely, we found a number of interesting observations at the “periphery” of the formalization, things that are not strictly within the scope of the formalization itself, but ways that a fault in the implementation, honest or malicious, could go undetected by the formalization.

They cover the audit in more depth in their own blog post.

Exponential-Size Extractors

In many cryptographic protocols, including Zcash, it is not enough for a zero-knowledge proof to establish that a statement is true. We also need to know that whoever produced the proof knows why it is true, that is, that they hold a "witness" for the statement.

The notion that captures this is knowledge soundness. Our goal is to show that any adversary able to convince the verifier can also be used to recover a valid witness. The algorithm that does this is called an extractor, which can rerun the prover against fresh verifier challenges, rewinding it until the transcripts collectively produce a valid witness.

An extractor with unlimited time could find a witness by brute force, and an extractor with no obligation to succeed could do nothing, so the definition has to bound two things at once:

• Knowledge error (): an upper bound on the probability that the verifier accepts while the extractor fails to return a witness. Thus, if the prover succeeds with probability , extraction succeeds with probability at least .
• Extractor cost: in the standard expected-time definition, if the prover convinces the verifier with probability , the extractor must recover a witness in expected time that grows at most inversely with , up to a polynomial factor.

The extractor in our proof is straight-line, meaning it never rewinds the prover, and this is deliberate.¹ The proof system is analyzed in the algebraic group model (AGM), where the prover supplies coefficients expressing each group element it sends as a linear combination of group elements it has received. These coefficients exist only in the security analysis.

From there the witness is recovered in two steps, both of which are plain functions in the Lean development:

• Circuit witness. This is computed deterministically from the prover's AGM messages. Against an adversary using at most Vesta group operations and random-oracle queries, the certified endpoint turns a prover that convinces the verifier without a valid circuit witness into a Vesta discrete-log solver running within group operations and queries.
• Specification witness. This is read directly off the circuit witness, with no further knowledge error. In our proof this is a simple sequence of cell reads, so its cost is evident by inspection. But the resource bounds we prove count group operations and random-oracle queries, and nothing in the formal contract bounds the extractor's actual running time. This is a theoretical gap that zkSecurity highlights, even though our extractors do not require extra effort.

Within this model, an adversary's advantage is the probability that it makes the verifier accept while extraction fails. Considering the computational part of that advantage, the certified profile gives:

Here bounds a Vesta discrete-log solver's success probability with oracle queries and group operations. The Ironwood book explains the full bound and its assumptions.

Encoding extractor complexity into the notion is difficult in Lean, where no standard model for studying computational complexity has yet emerged. Caliper, a Lean DSL for concrete running-time bounds that zkSecurity is developing, is a natural fit for closing this.

Superadaptive Soundness

During the development of Orchard, the protocol that Ironwood is based on, we paid close attention to adaptive soundness: an attacker who sees the public parameters before choosing its false statement still shouldn't be able to convince the verifier.

Less appreciated is the control a malicious prover may have had over the protocol itself, as its designer. Imagine that the Zcash developers searched an enormous space of candidate protocols, each separately satisfying the same soundness theorem, and found one that accepted a forged proof of their choosing. They could publish that one and abandon the rest without ever disclosing the search.

It is difficult to rule this out: offline work is usually invisible to a security analysis. What can help is ensuring that parts of the protocol contain no degrees of freedom that would allow such a search. This is why free constants in cryptographic designs are set to "nothing-up-my-sleeve" values such as the digits of π, and why curve designers demand rigidity: a curve should be the first output of a simple, stated search procedure.

Orchard's designers followed these practices. zkSecurity found a location in the construction where the protocol could be changed to inject an artificial degree of freedom, and then showed how to use it to break soundness through a search. But this change was very conspicuous, and no other area of our protocol contains a parameter that can be targeted in this way.

As a mitigation, our soundness definitions could be rewritten to anticipate protocol designers as adversaries, so that things like rigidity and degrees of freedom can be reasoned about mathematically. But this is not a well-studied area of cryptographic analysis, and today's ZKP cryptography is likely too complex to be subjected to it.

Conclusion

zkSecurity found no soundness bugs in our actual protocol, but they did find interesting ways to change our protocol so that it could survive the same kind of formal verification process we applied. In most cases they required impossibly powerful machines, conspicuous additional degrees of freedom, or violations of pre-existing trust boundaries. But in some cases they identified places where formal definitions could be tightened or expanded to capture more kinds of attacks.

Machine-checked proofs are only as useful as their statements, their models, and their connection to the system that ships. The way to earn confidence in all three is to attack them, and to publish what the attacks find. Ironwood's verification has now survived that treatment once.

Disclosure: zkSecurity was also hired to contribute parts of the Ironwood formal specification, but the principal contributor of that effort did not lead or contribute substantially to this audit.