In the week from February 12th to February 16th 2024, zkSecurity performed a security audit of Darkfi's built-in contracts and circuits. The audit was performed on the public darkfi repository.
security · zk · audit
Keep reading
Latest
Checking the Checkers and Auditing the Ironwood FV
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.
Archetype x zkSecurity - Proof is in the Pudding: zkML
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.
Intro to Clean for Devs.
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.
Recommended
Archetype x zkSecurity - Proof is in the Pudding: Privacy in Payment Networks
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.
FRIDA: Data-Availability Sampling from FRI
We've just dropped a blog post exploring the cool world of Ethereum's latest EIP-4844 upgrade and how it tackles the data-availability conundrum with Proto-Danksharding. Get ready to dive into the intricacies of making data more accessible (and less pricey) by using nifty concepts like blobs and polynomial evaluations. Plus, we dish on the role of FRI in data-availability sampling and how it can streamline things even more. Curious? Check out the details and see how this all shapes Ethereum's future!
Become a Halo2 Hero: Master Zero-Knowledge Proofs with Our New Course
We're teaming up with the Zircuit team to bring you a new course on Halo2 development that's perfect for Rust developers eager to dive into creating Halo2 circuits from scratch. No need to be a cryptographer or have prior knowledge of Halo2, PlonK, or zkSNARKs. Our course starts with the basics and guides you through building increasingly complex circuits. By the end, you'll be a Halo Hero! Plus, you'll have access to complete, runnable code examples on GitHub. Ready to start your Halo2 journey? Check it out!
More to explore
BitVM: Unlocking Arbitrary Computation on Bitcoin Through Circuit Abstractions
We're diving into the world of Bitcoin's UTXO model and how recent advancements like BitVM can overcome its limitations, allowing for more complex computations without changing Bitcoin's core. This blog post explores cutting-edge techniques like covenants, statefulness, and circuit models, showing how they enable intricate logic on Bitcoin. We'll break down how these innovations make trustless cross-chain transactions possible, and highlight the potential of optimistic protocols to optimize the on-chain footprint. If you're curious about the future of Bitcoin's capabilities, this is the deep dive you need!
ZPrize Came To An End! Who And How Did They Win $500,000?
In an exciting collaboration with ZPrize, we embarked on a journey to discover the fastest proofs for ECDSA signatures, ultimately crowning two standout approaches as winners. The blog post delves into the innovative solutions that captured the $500,000 prize by pushing the boundaries of zero-knowledge proofs. The story offers a fascinating glimpse into how these cutting-edge techniques might pave the way for privacy-focused applications. Curious to know which teams came out on top and how they did it? Dive in to explore the thrilling results and what's next in the ZK space!
Introducing zkvmBlast: Differential Fuzzing for Ethereum's zkVMs
zkVMs are moving to the center of Ethereum's roadmap, which means a bug in a zkVM is turning into a bug in Ethereum itself. We built zkvmBlast, a zkVM-agnostic differential fuzzer that runs the same program across SP1, RISC0, OpenVM, Pico, Zisk, and Airbender against a reference simulator and flags any disagreement. It hunts for both soundness and completeness bugs, with a deliberate focus on completeness, an under-explored class that can turn a single valid block into a liveness failure. We share the first batch of findings.