Proof is in the Pudding is a IRL series of whiteboard sessions hosted by Archetype and zkSecurity.
For Session 02, we cover zkTLS (also called zkOracles, HTTPz, or MPC-TLS). This includes public approaches like public oracles (chainlink), TEE approaches like TownCrier, TLS Notary and Deco style approaches that mix using MPC protocols or pure proxies.
Watch it on Archetype's channel!
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 think that Clean is the future of circuit development, so we created a programmer-first introduction to show circuit developers who have never used formal verification how they can build circuits faster, safer and better.
In Session 08 of "Proof is in the Pudding," we explore how different networks have approached privacy over the years. From E-Cash and Monero to MobileCoin and Zether, we break down blind signatures, Pedersen commitments, stealth addresses, ring signatures, and more. This session provides a comprehensive tour of the techniques used to break linkability, hide addresses, and obscure transaction data in the name of privacy and safety.
Curious about how zero-knowledge virtual machines (zkVMs) make computing more secure without the hassle? We delve into the fascinating world of zkVMs, where you can program in high-level languages like Rust or C and let cryptography handle the complexity. We'll explore the evolution of these innovative systems through projects like Cairo and RISC Zero, while touching on the unique benefits and technical insights each brings. Plus, learn about groundbreaking techniques for optimizing zkVMs with projects like Jolt, and discover a range of other influential zkVM initiatives. Get ready for an enlightening journey into secure computation!
Ever wondered how zkVMs simplify the use of zero-knowledge proofs in coding? We dive into how they let developers focus more on application logic by abstracting complex cryptographic aspects, using familiar languages like Rust or C++. But hold on, it's not all smooth sailing. Despite these benefits, a single bug anywhere in the complex system of compilers, proof systems, or verification can lead to serious security issues. In the post, we break down the zkVM workflow, explore common vulnerabilities at each phase, and highlight the importance of understanding these layers to build more secure, zk-powered applications. Curious about how this all plays out? Let’s unravel it together!
mpcsec.org is a new collaborative reference for common pitfalls in MPC implementations and the cryptographic primitives they rely on, built with contributors from zkSecurity, Trail of Bits, Partisia, and Zama. If you build, audit, or deploy threshold signatures, distributed key generation, or other MPC protocols, it's a starting point for the mistakes you don't want to repeat.
We recently teamed up with Lighter to dive deep into their custom ZK circuits used for a verifiable orderbook matching on a Layer 2 exchange. Our findings show solid and well-structured code, thanks to their cooperative engineering team. The post gives a fascinating look into how Lighter’s ZK rollup ensures valid state transitions on Layer 1 through zero-knowledge proofs and the innovative structure of their order book matching process. It explains the roles of the main operation and exit hatch circuits, while also touching on how users can exit in emergencies. It's a great read if you're curious about how these systems maintain security and efficiency in decentralized finance.
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!