Check out the latest episode of Node Guardians to see our cofounder David Wong talk about ZK security and the future of ZK with Sam. In this episode, David discusses the different workflows that can be used for blockchain auditing, the importance of math in auditing, and the scope of work that blockchain auditors typically perform. He also talks about the challenges of working in different contexts, how vulnerabilities are rated, and the usefulness of formal verification.
Mathias and Giorgio join Anna Rose and fellow zkSecurity teammates Nico and Kobi on the Zero Knowledge podcast to talk about Clean, zkGolf, and what happens when AI agents compete to build better circuits with proofs of correctness.
Cryptographic software is error-prone and failures are catastrophic, therefore formal verification is a powerful and increasingly practical tool for greatly improving the assurances of our cryptographic software. But who verifies the formal verification? Formal verification itself is software too, what is proved, under which assumptions and its relation to the real-world implementation lie beyond the scope of the machine-checked proof. In this post, we want to give some insights into our three-week audit of the Ironwood formalization and some of the common pitfalls that formal verification more broadly can encounter.
In Session 11 of "Proof is in the Pudding," we look at what it takes to prove model inference. We cover transformer computation, sumcheck, GKR, lookup arguments, quantization, and KV caching, then discuss scaling and possible uses for verifiable ML.
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!
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.
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.
Zero-knowledge proofs (ZKPs) have come a long way from theory to real-world applications like blockchains and private transactions. We’ve been busy auditing various ZKP implementations and developing tools to improve circuit safety and security. In this blog post, we’ll explore how vulnerabilities can crop up in SNARK systems and the current state of tools designed to spot these issues. From circuit bugs to the often-overlooked frontend and backend layers, we cover how various analysis techniques and formal verification approaches are evolving to ensure robust ZKP systems. Dive in to discover the potential and current challenges in ZKP security!
Ever wondered if you could create a ciphertext that's only decrypted when a polynomial inside a commitment has a particular value? We’ve explored this notion using KZG commitments in our latest Asiacrypt 2024 paper. Dive into the elegant world of Witness Encryption and see how it can be applied in cool ways like Laconic Oblivious Transfer. This approach keeps things as efficient as regular KZG operations and might just spark some creative applications of your own! Curious to learn more? Let’s explore together!
This post is the second part of our series on Circom pitfalls. While part 1 covered issues with assertions, hints, and aliasing, this one explores unsafe component usage and the subtle fact that Circom’s comparison operators work over signed integers.