文章
视频
课程
百科图谱
线下集训
更多
问答
提问
发表文章
专栏
活动
文档
工作
集市
发现
Toggle navigation
文章
问答
视频
课程
线下集训
专栏
活动
工作
文档
集市
搜索
登录/注册
Veridise
文章
专栏
问答
视频
课程
集市作品
活动
招聘
TA的视频
TA的合集
RISC Zero 如何实现持续且可证明的零知识安全性?
该视频总结了 Risk Zero 和 Veridise 合作,使用 Veridise 的 PyKIS 工具对 Risk Zero 的 Ketchak 电路进行形式化验证,证明其确定性的过程和意义。 **核心内容/主要观点:** * Risk Zero 和 Veridise 成功合作,使用 PyKIS 工具形式化验证了 Risk Zero 的 Ketchak 电路的确定性。 * 形式化验证对于确保零知识证明系统的安全性至关重要,可以有效防止“欠约束”漏洞。 * 此次合作不仅验证了特定电路,也为持续验证和优化 Risk Zero 的电路提供了自动化流程。 **关键论据/关键信息:** * **确定性的重要性:** 确定性是零知识电路的关键属性,确保电路的行为是可预测的,防止出现意外或恶意解。 * **PyKIS 工具:** Veridise 开发的 PyKIS 工具可以检查零知识电路的确定性,并能生成反例或进行形式化验证。 * **合作过程:** Veridise 在初期审计时就发现了 Risk Zero 电路中的漏洞,促成了双方的合作。Risk Zero 积极配合,快速迭代,最终完成了验证。 * **形式化验证的文化:** Risk Zero 非常重视形式化验证,将其视为确保系统安全性的重要手段。 * **DSL 的作用:** Risk Zero 使用的领域特定语言 (DSL) Zergen,其模块化设计和明确的语义使得电路更易于验证。 * **未来方向:** 双方都计划在形式化验证方面进行更多探索,包括验证编译器、电路的功能正确性,以及开发更通用的验证工具。Veridise 正在开发LLCK,一个用于电路DSL的底层中间表示,旨在构建更广泛的安全工具。 * **形式化验证的假设:** 视频中也提到了形式化验证依赖于一些假设,例如代码翻译的正确性,以及验证工具本身的正确性。未来需要进一步加强这些方面的保证。
15
0
0
4天前
Veridise
关注
贡献值: 75
学分: 56
使用形式化方法加强区块链安全性
0 关注
0 粉丝
×
发送私信
请将文档链接发给晓娜,我们会尽快安排上架,感谢您的推荐!
发给:
内容:
提醒
检测到你当前登录的账号还未绑定手机号
请绑定后再发布
去绑定
×
编辑封面图
封面预览
取消
确认