bibibi.cc正在加载…
EthSystems称已完成隐私池从书面规范到Sepolia字节码的形式化验证，并发现6个问题。
EthSystems完成隐私池形式化验证，覆盖规范到Sepolia字节码
PANews 10月27日消息，以太坊机构隐私技术机构EthSystems宣布对其隐私池（shielded pool）完成了形式化验证，范围从书面规范一直到Sepolia测试网上运行的字节码。验证按层使用不同工具：模型、电路和哈希用Lean，合约用Halmos和Kontrol，钱包用Aeneas和Verus，验证器和部署通过逐字节重建核对。双花和价值守恒已由Lean定理机器验证。验证中共发现6个问题，其中3个出在验证工具本身。团队同时列出了仍然依赖的假设：哈希无碰撞、验证器会拒绝伪造证明、合约行为与模型一致。
原文链接：https://www.panewslab.com/zh/articles/01a17d43-5012-7152-b8bb-1985c4cfe78b
PANews报道称，EthSystems宣布完成其隐私池的形式化验证。
验证范围从书面规范延伸至Sepolia测试网上运行的字节码。
模型、电路和哈希使用Lean验证，合约使用Halmos和Kontrol，钱包使用Aeneas和Verus。
验证器和部署通过逐字节重建核对。
双花和价值守恒已由Lean定理机器验证。
验证共发现6个问题，其中3个出在验证工具本身。
团队列出的剩余假设包括：哈希无碰撞、验证器会拒绝伪造证明、合约行为与模型一致。
以下为辅助分析，与已报道事实分开展示；重要信息请进一步核实。
形式化验证是用工具按明确规则检查系统是否符合规范。此次工作覆盖模型、电路、哈希、合约、钱包、验证器和部署字节码，但结果仍建立在团队列出的若干假设之上。
这项验证声称覆盖了从规范到测试网字节码的多个层次，并检查双花和价值守恒等问题；同时，发现的问题和剩余假设说明验证并不等于所有风险都已消除。
新手应把它理解为一次范围较广的技术安全检查声明，而不是隐私池已被证明绝对安全，也不能据此确认其主网状态。
正在加载事件时间线…