31 min listen
Episode 284: Using Formal Verification on ZK Systems with Jon Stephens
FromZero Knowledge
ratings:
Length:
80 minutes
Released:
Jul 12, 2023
Format:
Podcast episode
Description
This week Anna Rose (https://twitter.com/annarrose) chats with Jon Stephens (https://twitter.com/FormallyJon), Computer Science Ph.D. student in the UToPiA group (https://utopia.cs.utexas.edu/) at UT Austin and co-founder of Veridise (https://veridise.com/). Veridise is a blockchain auditing firm that audits smart contracts and ZK systems. They discuss what led Jon to work on system security, what tools are available to test the security of ZK systems and the process of performing formal verification on ZK systems. They also cover general ZK security, why this topic matters and ways we can incentivise ethical disclosures when bugs and vulnerabilities are found.
Additional reading for this week's episode;
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts by Stephens, Ferles, Mariano, Lahiri, and Dillig (https://www.cs.utexas.edu/~isil/SmartPulse.pdf)
Certifying Zero-Knowledge Circuits with Refinement Types by J. Liu, Kretz, H. Liu, Tan, Wang, Sun, Pearson, Miltner, Dillig, and Feng (https://eprint.iacr.org/2023/547.pdf)
Practical Security Analysis of Zero-Knowledge Proof Circuits by Wen, Stephens, Chen, Ferles, Pailoor, Charbonnet, Dillig and Feng (https://eprint.iacr.org/2023/190.pdf)
Episode 67: Formal Verification with Martin Lundfall (https://zeroknowledge.fm/67-2/)
Episode 70: Digging into DAI with Rune Christensen from Maker (https://zeroknowledge.fm/70-2/)
Episode 255: Verifying Consensus On-Chain with Succinct (https://zeroknowledge.fm/255-2/)
Boogie: An Intermediate Verification Language (https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/)
Circom-lib (https://docs.circom.io/circom-language/circom-insight/circom-library/)
How Coders Hacked Back to ‘Rescue’ $208 Million in Ethereum (https://www.vice.com/en/article/qvp5b3/how-ethereum-coders-hacked-back-to-rescue-dollar208-million-in-ethereum)
zkSummit 10 is happening in London on September 20, 2023! Apply to attend now -> zkSummit 10 Application Form (https://9lcje6jbgv1.typeform.com/zkSummit10)
Polygon Labs (https://polygon.technology/) is thrilled to announce Polygon 2.0: The Value Layer for the Internet (https://polygon.technology/roadmap).
Polygon 2.0 and all of our ZK tech is open-source and community-driven. Reach out to the Polygon community on Discord (https://discord.gg/0xpolygon) to learn more, contribute, or join in and build the future of Web3 together with Polygon!
Anoma’s (https://anoma.net/) first fractal instance, Namada (https://namada.net/), is launching soon!
The MASP circuit's latest update enables shielded set rewards directly in the shielded set, a novel feature that funds privacy as a public good.
Follow Namada on twitter @namada (https://twitter.com/namada) for more information and join the community on Discord discord.gg/namada (https://discord.com/invite/namada).
If you like what we do:
* Find all our links here! @ZeroKnowledge | Linktree (https://linktr.ee/zeroknowledge)
* Subscribe to our podcast newsletter (https://zeroknowledge.substack.com)
* Follow us on Twitter @zeroknowledgefm (https://twitter.com/zeroknowledgefm)
* Join us on Telegram (https://zeroknowledge.fm/telegram)
* Catch us on YouTube (https://zeroknowledge.fm/)
Additional reading for this week's episode;
SmartPulse: Automated Checking of Temporal Properties in Smart Contracts by Stephens, Ferles, Mariano, Lahiri, and Dillig (https://www.cs.utexas.edu/~isil/SmartPulse.pdf)
Certifying Zero-Knowledge Circuits with Refinement Types by J. Liu, Kretz, H. Liu, Tan, Wang, Sun, Pearson, Miltner, Dillig, and Feng (https://eprint.iacr.org/2023/547.pdf)
Practical Security Analysis of Zero-Knowledge Proof Circuits by Wen, Stephens, Chen, Ferles, Pailoor, Charbonnet, Dillig and Feng (https://eprint.iacr.org/2023/190.pdf)
Episode 67: Formal Verification with Martin Lundfall (https://zeroknowledge.fm/67-2/)
Episode 70: Digging into DAI with Rune Christensen from Maker (https://zeroknowledge.fm/70-2/)
Episode 255: Verifying Consensus On-Chain with Succinct (https://zeroknowledge.fm/255-2/)
Boogie: An Intermediate Verification Language (https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/)
Circom-lib (https://docs.circom.io/circom-language/circom-insight/circom-library/)
How Coders Hacked Back to ‘Rescue’ $208 Million in Ethereum (https://www.vice.com/en/article/qvp5b3/how-ethereum-coders-hacked-back-to-rescue-dollar208-million-in-ethereum)
zkSummit 10 is happening in London on September 20, 2023! Apply to attend now -> zkSummit 10 Application Form (https://9lcje6jbgv1.typeform.com/zkSummit10)
Polygon Labs (https://polygon.technology/) is thrilled to announce Polygon 2.0: The Value Layer for the Internet (https://polygon.technology/roadmap).
Polygon 2.0 and all of our ZK tech is open-source and community-driven. Reach out to the Polygon community on Discord (https://discord.gg/0xpolygon) to learn more, contribute, or join in and build the future of Web3 together with Polygon!
Anoma’s (https://anoma.net/) first fractal instance, Namada (https://namada.net/), is launching soon!
The MASP circuit's latest update enables shielded set rewards directly in the shielded set, a novel feature that funds privacy as a public good.
Follow Namada on twitter @namada (https://twitter.com/namada) for more information and join the community on Discord discord.gg/namada (https://discord.com/invite/namada).
If you like what we do:
* Find all our links here! @ZeroKnowledge | Linktree (https://linktr.ee/zeroknowledge)
* Subscribe to our podcast newsletter (https://zeroknowledge.substack.com)
* Follow us on Twitter @zeroknowledgefm (https://twitter.com/zeroknowledgefm)
* Join us on Telegram (https://zeroknowledge.fm/telegram)
* Catch us on YouTube (https://zeroknowledge.fm/)
Released:
Jul 12, 2023
Format:
Podcast episode
Titles in the series (100)
Episode 13: Bloom filters, PoA and what's up with ERP?: The gang catches up on what's been going on in the blockchain world for the past month, sharing some nuggets of learning around bloom filters, Proof of Authority, upcoming events, the Dfinity paper and some comments on what all the fuzz around this ERP is. by Zero Knowledge