登录后可观看高清视频
ZKP MOOC 第 15 课：使用形式方法的安全 ZK 电路
41次播放
2025-02-12
在这段视频中，Yu Feng教授讨论了如何通过形式化方法来确保零知识电路（ZK circuit）的安全性。他强调了区块链软件中的漏洞可能导致严重的安全问题，尤其是在智能合约和零知识证明等层面。教授提到了一些具体的案例，例如闪电贷漏洞和Solana协议的拒绝服务漏洞，强调了这些漏洞可能导致巨额资金损失。
视频的核心内容包括：
- 形式化方法的定义与重要性：形式化方法是一系列数学上严格的技术，用于发现软件中的错误并证明其正确性。它们可以分为动态和静态技术，教授主要关注静态技术，如抽象解释和形式验证。
- 静态分析与形式验证的应用：教授介绍了两种项目，第一种是利用轻量级静态分析快速识别ZK电路中的常见漏洞，第二种是通过形式验证确保ZK电路在特定属性下的数学正确性。
关键论据和信息包括：
- 漏洞的严重性：区块链软件中的逻辑错误和安全漏洞可能被攻击者利用，导致资金损失。
- 形式化方法的优势：通过适当的形式化方法，可以大幅减少软件中的错误。
- 抽象解释的应用：抽象解释可以有效捕捉Web3智能合约中的多种漏洞，如重入攻击和整数溢出。
- 形式验证的必要性：形式验证能够提供更强的保证，确保程序的行为符合预期，但需要提供形式化的规范。
- ZK电路的特定问题：教授详细讨论了ZK电路中可能出现的过约束和欠约束问题，并提出了相应的检测和验证方法。
最后，教授总结了形式化方法在确保软件安全性方面的重要性，并鼓励对ZK安全感兴趣的研究者与他联系。
