University of Applied Sciences Northwestern Switzerland — School of Computer Science

Trusty — DSL for Cryptographic Protocols with Zero-Knowledge Properties

Protocols written in Trusty run inside of zero-knowledge virtual machines (zkVMs) which generate a verifiable cryptographic proof of correct execution. The language features simple protocol-focused syntax and high-level abstractions for cryptographic primitives. Trusty's command-line interface (CLI) is capable of running programs as well as both generating and verifying proofs.

A Proof of Knowledge written in Trusty, as well as generating and verifying a proof A «Proof of Knowledge» written in Trusty.
Proofs of Knowledge are a simple type of zero-knowledge proof where knowledge is proven by revealing a derived value; in this case, the secret's hash.

Initial situation

As more and more services become accessible online, it is becoming increasingly difficult to control who can and cannot access sensitive information. Traditional cryptography alone may no longer suffice to prevent unnecessary data leakage. For example, proving someone's eligibility to vote should ideally not require them to reveal their exact birth date.

Zero-knowledge proofs (ZKPs) address this issue by allowing a verifying party to ensure the correctness of a statement without revealing the underlying secret data itself. A simple example of a ZKP is the colorblindness test, where you prove to a colorblind person that you can differentiate two colors. The colroblind person (the verifier) swaps or doesn't swap the colors behind their back, and you (the verifier) say whether they were swapped. After enough correct answers, the verifier can eventually ensure that you didn't just guess luckily, but actually see 2 distinct colors, without ever knowing what the colors are.

Zero-knowledge virtual machines (zkVMs) take this one step further and provide a way to prove that a program was executed correctly given a set of inputs, without revealing the inputs. zkVMs thus make it easier to implement protocols for ZKPs, but their developer experience leaves much to be desired. They are difficult to use, require a lot of wrapper code, and developers must learn the intricacies of the host programming language and cryptographic libraries.

Project goal

This project explores how a domain-specific programming language (DSL) can be designed to efficiently run in zkVMs, as well as whether any additional measures to conventional language construction techniques must be taken in order to make the approach viable. The result should be a simple language providing high-level abstractions around common cryptographic primitives (hashin, digital signatures, and encryption) which is able to be executed inside a zkVM.

Usage

Usage of the Trusty CLI, showing the execution of a script, as well as generating and verifying a proof

The prover runs a script using the CLI, which executes the program inside the zkVM and generates a proof. The source code and proof are can then be sent to a verifier, who can use their own installation of the CLI to verify the proof and ensure that the prover used the provided source code.

AST

A simple AST generated from a Trusty script, showing the different nodes representing values and operations

The AST is an abstract representation of the source code, where each node represents either a value or an operation. The AST is evaluated by the interpreter from the bottom up.

Architecture

Architecture of the Trusty DSL, showing the host-side compiler and AST interpreter running inside the zkVM

Trusty's implementation consits of several components. From left to right: The host is the abstraction provided by the CLI; the lexer turns source code into tokens, which are small meaningful units of the language; the parser turns the tokens into an abstract syntax tree (AST), which is an abstract representation of the source code; the optimizer performs certain precomputations on the AST to improve performance inside the zkVM; the AST interpreter executes the AST inside the zkVM, which produces a proof of correct execution and a program fingerprint.

Solution developed and its benefits

Trusty is an open-source, external DSL for implementing cryptographic protocols with zero-knowledge properties on top of zkVMs. A host-side compiler turns Trusty source code into an abstract representation. This is done outside of the zkVM to improve performance, as source code translation does not need to be verifiable. The representation, an abstract syntax tree (AST) in this case, is then executed by an interpreter inside the zkVM. The zkVM produces a proof of correct evaluation of the tree, and Trusty's command-line interfave (CLI) provides a standardized workflow for running scripts, generating, and verifying proofs across multiple zkVMs.

The language features

  • a simple, pseudocode-inspired syntax;
  • explicit differentiation bewteen public and private values, where only public values may be encoded into the proof;
  • built-in cryptographic primitives for hashing, creating and verifying digital signaures, encrypting and decrypting data, generating cryptographically secure random data, as well as parsing of cryptographic keys;
  • high-level abtractions for configuration of cryptographic primitives, which each of the primitives supporting a variety of different algorithms;
  • a static type system, improving the error reporting for mis-handled values;
  • a compiler capable of checking the source code for both syntactic and semantic errors, such as invalid keywords, unsupported algorithms, or data leaked through visibility violations;
  • an optimizer which precomputes certain parts of the AST to improve runtime performance inside the zkVM;
  • a CLI capable of running programs, generating and verifying proofs;
  • support for the RISC Zero and Pico zkVMs with optional GPU acceleration.

Trusty allows developers to focus on the fundamental logic of cryptographic protocols, rather than worrying about implementation details. The language is simple and the program is portable with no low-level interactions wtih the zkVM, further simplifying the use of the technology. The implemented AST optimizations yielded good results in improving the runtime performance by up to 40%.

The language successfully bridges the gap bewteen protocol design and zero-knowledge execution and enables developers to implement verifiable cryptographic protocols with significantly reduced effort and simultaneously provides safeguards for sound protocol design.

Key terms

  • Abstract Syntax Tree (AST) Abstract representation of source code where each node represents a value or operation.
  • Command-Line Interface (CLI) A text-based interface for interacting with a program, as opposed to a graphical user interface (GUI).
  • Compiler A program that translates source code from a high-level programming language into a machine-readable format.
  • Cryptographic Primitives Basic algorithms and protocols that serve as building blocks for cryptographic systems, such as hashing, digital signatures, and encryption.
  • Domain-Specific Language (DSL) A programming language designed for a specific domain or application, providing abstractions and syntax tailored towards it.
  • Interpreter A program that executes instructions in an abstract representation of source code rather than machine code.
  • Zero-Knowledge Proof A cryptographic method by which one party (the prover) can prove to another party (the verifier) that a statement is true without revealing any information beyond the validity of the statement itself.
  • Zero-Knowledge Virtual Machine (zkVM) A virtual machine that executes programs in a zero-knowledge manner, allowing for the verification of computations without revealing the underlying data.

Customer

University of Applied Sciences Northwestern Switzerland — School of Computer Science

Institute for Mobile and Distributed Systems (IMVS)
University of Applied Sciences Northwestern Switzerland
School of Computer Science
www.fhnw.ch/imvs

Team

Mladen Branković
Marcel Pfeuti

Advisors
Markus Knecht
Daniel Kröni