Runtime Verification conducts a design audit on Zorp’s Eden zkVM
Runtime Verification is pleased to announce the completion of the design audit for the Zorp’s Eden zkVM. Eden is a Turing-complete instruction set derived from Nock along with arithmetization techniques to enable its use in zkVMs. The Eden zkVM is part of the Urbit ecosystem and is a zero-knowledge virtual machine used for proving Eden computations within a zk-STARK proof system.
Audit Scope
Before conducting a code review, it is beneficial for projects to undergo a design review, especially in the early stages of development. Design reviews help auditors gain a deeper understanding of how a protocol works, with the aim of identifying high-level protocol design issues that, if not fixed, could later affect the logic and code. In this case, we conducted a design review with Zorp to assess the feasibility of using their zkVM design to validate arbitrary Eden computations. The proposed framework verifies program integrity by ensuring that the arithmetization captures necessary aspects of computation and guarantees its integrity. In addition, the protocol correctly introduces and makes use of randomness.
This audit focused on reviewing computation primitives, arithmetization, and computation verification using tables. Additionally, a formal proof was created as part of the audit for an important theorem in Isabelle/HOL.
The audit scope is limited to the design documents hosted by Zorp HackMD. Further information on the audit can be found in the report.
Methodology
Runtime Verification conducted a design review for a period of two weeks and delivered a detailed report on June 23rd, 2023.
The audit methodology involved manual review of documents, creation of diagrams, and proving a bijection between Dyck words and binary trees using a proof assistant. The process was iterative, with daily reviews of new sections or content, in which suggestions and questions were thoroughly discussed and then resolved in subsequent versions of the design description.
The audit began with a review of primitives: full binary trees and their encoding to Dyck words. A formal proof of the bijection between full binary trees and Dyck words was created using Isabelle/HOL. This proof confirms the accuracy of the algorithms used to encode and decode full binary trees. Each statement in the Eden computation is a formula that can be represented as binary trees, with opcodes transforming the tree during the computation. These trees are called nouns, which are pairs containing a subject and a formula that applies to the subject. Omitting details and theory, there are two important facts to understand our work at this stage:
- Any Eden computation can be represented as a transformation of full binary trees after each computational step.
- ZK arithmetization requires the representation of computation steps in the form of polynomials.
Dyck words are used at this point. A Dyck word encodes the structure of the full binary tree as a binary vector (a string that contains only 1 or 0 digits). The first step of arithmetization is converting nouns to vectors, a leaf vector containing values from the tree and a Dyck word encoding the shape of the tree. We formally verified, in Isabelle, several facts:
- Their procedure for encoding and decoding is safe, meaning we can always encode any tree as a unique vector and safely recover our tree from the vector using their decoding technique. No collision can happen since we proved the bijection for maps.
- They are using two definitions of Dyck words: inductive and canonical.
- An inductive definition is one that recursively defines how to compose a new Dyck word using two others, connecting them together as 0a1b, where a and b are Dyck words.
- A canonical definition specifies that any Dyck word must contain at most the same number of ones as zeroes in any given prefix and an equal number 0 and 1 digits in the entire word.
In their case, the inductive definition is more useful, and they rely on it in practice when working on key concepts behind the arithmetization. We have shown that these two definitions are equivalent. This means that users of the zkVM can be mathematically certain that a binary vector introduced in the computation after their encoding has the required properties.
We then focused on the arithmetization of primitives. After obtaining leaf vectors and Dyck words from each noun, they need to be converted into polynomials over a prime field. Polynomials are either identical or differ almost everywhere, and this key polynomial property is vital for probabilistic identity checking used in the design of tables and checking the cons relation. The use of the finite field allows, in turn, avoiding infinite numbers, which is very handy as any hardware has performance limitations. Probabilistic identity checking is implemented using probabilistic data structures such as p-multisets and p-stacks, which are just computation procedures for mapping binary vectors and tuples to field elements. The correctness and efficiency of these procedures are chief ingredients in the design of the zkVM.
We reviewed the underlying mathematics to ensure that their use of polynomials for data structure encoding is accurate and follows the general zk-STARK arithmetization approach.
The final, and perhaps most important, object of study was understanding the design of tables. Tables are a technical procedure for storing values computed by polynomials discussed before. Each algorithm for building a polynomial from a data structure can be considered a brick, and tables would be a house. Our main concern was to ensure the bricks used to build the house were excellent, and the architecture was flawless. Meaning that all necessary aspects of computations were captured by their tables and consequently validated without the risk of obtaining a fake computation that would fool the zk-STARK verifier (e.g. to steal tokens or get them from thin air).
Results
The audit identified and highlighted some issues along with some informative findings. The RV team provided feedback on security and correctness concerns in the zkVM design and the changes were made accordingly. The proposed design meets the principal requirements of a zkVM solution and allows for proving arbitrary limited-in-size Eden computations. However, it should be noted that the auditing team only worked with the high-level design, and the correctness of the implementation and some parts of the design, such as jetting, were out of the scope of this audit.
The design of the system was stable and was not significantly changed during the audit. However, its description was incomplete at the beginning of the audit. Technical details, motivation of certain technical decisions, and minor corrections were added later.
Readers interested in a more detailed and technical explanation of the findings can go over the full report in our GitHub repository.
About Zorp
Zorp is a startup focused on developing best-in-class zero-knowledge proof systems, emphasizing minimalist computing architectures.
About Runtime Verification
Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.