ZK/SEC Research notes from zkSecurity
All posts
noname · Part 1 of 4

noname: ZK app developers should be able to see down to the constraints

noname

As we've explained before, zero-knowledge apps (or ZK apps) will come in two different shapes: VM instructions and arithmetic circuits.

VM instructions should sound familiar. Reading them is like reading assembly, and they're a level of abstraction higher than arithmetic circuits (as pointed out by this post).

Whatever they're writing, real programmers need to see what their programs compile down to (according to John Carmack). That's how you find unoptimized bits as a low-level code monkey, but it's also how you find some security issues and bugs. It's not just that compilers have bugs, it's also that ZK developers are facing a new kind of programming. That is, when they'll be writing circuits (the VM-side of the ZK coin is not so new after all).

When writing zkApps, or ZK programs, that compile down to circuits, developers will be faced with a restricted and unsafe environment. Restricted because they will have to optimize their code to fit into the circuit size limits, and unsafe because they will need to ensure that what needs to be constrained is correctly constrained (we'll be writing more on that!).

Low-level developers know exactly what this means: they need access to the machine-generated code, the "assembly", the lowest possible layer. They need the source of truth.

For zkApps in proof systems like PlonK, that source of truth is the list of gates, and the wires, that describe the circuit. This list of gates and the wiring is often obtained by compiling a program written in a higher-level language or framework.

SnarkyJS is one example of a framework that helps developers write circuits in typescript without having to think about or understand circuits, or having to learn a new language.

snarkyjs

As you can see, it mostly looks like typescript decorators and library function calls. On the other hand, Leo is one example of a made-up programming language that offers the same thing.

leo

Both of these approaches offer different benefits and downsides. The framework approach can rely on the preexisting tooling of the language the framework is written in. On the other hand the DSL approach prevents developers from making some types of mistakes by mixing in logic that does not get constrained (but that's not always true depending on the DSL, as Circom has shown us).

What the children of both approaches all seem to be lacking though, is a way to see the "assembly" a program compiles down to.

Better toolings need to become available.

At zksecurity.xyz, we've experimented with a new programming language called noname (initially meant as a placeholder name). noname allows developers to write zkApps in a high-level language that looks like a mix of Golang and Rust:

use std::crypto;

fn main(pub public_input: Field, private_input: [Field; 2]) {
    // checks that they add up to 2
    let res = private_input[0] + private_input[1];
    assert_eq(res, 2);

    // checks that one is the hash of the other
    let digest = crypto::poseidon(private_input);
    assert_eq(digest[0], public_input);
}

The particularity of noname is that you get extensive debug information on how such programs compile down to gates. For example, passing the --debug argument to noname gets you an output describing the "assembly". A list of gates, where each gate is accompanied with an explanation as to why it exists and what line of code it comes from.

In addition, the wiring is also displayed at the end with similar information about the source of their existence:

noname, at the moment, is more of a toy language that we've used to understand other compilers, and the type of compiler bugs that can occur. We've also used it to teach how to read ZK circuits!

While the project is still experimental, we're excited to see if this will inspire more people to build better debugging tools, as well as lead to students (in school or at heart) using noname to learn about how arithmetic circuits are constructed.

Head over to our repo to try it out!

Keep reading
Recommended

noname 2.0: Unlocking Numeric Generics, Folding Schemes, and a Playground

We're excited to introduce the preview of noname 2.0, packed with features that make developing advanced ZK circuits easier than ever. This update includes flexible generic-sized arrays, seamless integration with folding schemes for IVC, and an interactive online playground to test and share code. We've also optimized R1CS constraint generation to boost performance. Plus, there are numerous community-driven enhancements and bug fixes that make the language more robust and user-friendly. Dive in to explore the specifics of our journey, learn from the contributions of our vibrant open-source community, and see how noname is evolving into a more versatile tool for developers.

ZK/SEC · August 08, 2024

noname 3.0: Native Hints, Standard Library, Compiler Visualizer, And More!

We're super excited to introduce noname 3.0, our zk programming language inspired by Rust and Golang, now achieving full feature parity with Circom. This update brings native hints, a standard library, debugging features, and a lot more to enhance developer experience. Dive into how hint functions work with an 'unsafe' keyword to balance innovation and security, explore our new stdlib modules, and see how the compiler pipeline visualizer can help you understand the compiling process. Plus, check out our next steps and how you can contribute to shaping noname's future.

ZK/SEC · November 13, 2024

noname meets Ethereum: Integration with SnarkJS

We're excited to share that our programming language, noname, now supports R1CS, making it easier to write zero-knowledge (ZK) circuits and deploy them on Ethereum using SnarkJS. This update introduces an alternative to the common Circom language, with a simple and intuitive syntax inspired by Rust and Golang. In this post, we illustrate how to deploy a noname-based Sudoku circuit on Ethereum, demonstrating core benefits like proving a solution's correctness without revealing it. Dive in to explore how noname could potentially unify the fragmented zkSNARK ecosystem and simplify your circuit writing process!

Katat Choi · June 01, 2024
More to explore

Public report of auditing Penumbra's circuits

We conducted an audit of Penumbra's main circuits and found eight issues, including the critical "double spend" and "double vote" bugs, which the Penumbra team promptly fixed. Our findings highlight Penumbra's robust documentation and code testing. Readers will get insights into how Penumbra uses zero-knowledge proofs for privacy, its decentralized exchange features, and its governance model. The post also provides detailed pseudocode for various cryptographic protocols, emphasizing how Penumbra ensures secure and private transactions. It's a deep dive into the technical details for those intrigued by privacy-focused blockchain technologies.

ZK/SEC · August 24, 2023

Public report of Sui's zkLogin audit

We just finished an audit of the Sui Foundation's zkLogin application and we're sharing what we found: the code is well-documented, tested, and specified. The zkLogin is set to make user authentication on the blockchain secure but simple, replacing cryptographic keys with familiar SSO methods like Google or Facebook while preserving user privacy. We also dive into the technical details behind JWT verification, non-native arithmetic for RSA, and vector programming. Plus, learn about the trusted setup process for zkLogin, ensuring maximum security through a decentralized multi-party ceremony. If you're curious about the intricate mechanics behind zkLogin, this is a must-read.

ZK/SEC · November 07, 2023

The Final Form of Software Development

What if the final form of software development was just watching code and proof popping up while you sip a drink? Letting AI agents write assembly directly alongside Lean proofs sidesteps the whole compiler-trust problem. With a peek at real EVM 256-bit addition code and its specification, you'll see why the assembly + Lean paradigm is final in both the historical and category theoretic sense.

Yoichi Hirai · April 29, 2026