文章 视频 课程 百科图谱 线下集训
更多
  • 问答
  • 提问
  • 发表文章
  • 专栏
  • 活动
  • 文档
  • 工作
  • 集市
  • 发现
  • 文章
  • 问答
  • 视频
  • 课程
  • 线下集训
  • 专栏
  • 活动
  • 工作
  • 文档
  • 集市
搜索
  • 登录/注册
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
Veridise
贡献值: 75 学分: 56
使用形式化方法加强区块链安全性
0 关注 0 粉丝
关于
关于我们
社区公约
学分规则
Github
伙伴们
DeCert
ChainTool
GCC
合作
广告投放
发布课程
联系我们
友情链接
关注社区
Discord
Twitter
Youtube
B 站
公众号

关注不错过动态

微信群

加入技术圈子

©2025 登链社区 版权所有 | Powered By Tipask3.5|
粤公网安备 44049102496617号 粤ICP备17140514号 粤B2-20230927 增值电信业务经营许可证

发送私信

请将文档链接发给晓娜,我们会尽快安排上架,感谢您的推荐!

提醒

检测到你当前登录的账号还未绑定手机号
请绑定后再发布
去绑定
编辑封面图
封面预览