Pectra 系统合约通过 Halmos 进行形式化验证
realtime news Feb 01, 2025 15:24
Pectra 硬分叉引入了使用汇编语言的系统合约，引起了安全性方面的担忧。利用 Halmos，形式化验证确保了这些合约的正确性和安全性。
以太坊网络计划通过 Pectra 硬分叉增强其区块链，该分叉引入了几种用汇编语言编写的系统合约。据a16zcrypto.com介绍，这些合约旨在优化 gas 效率，但由于其底层特性，也引发了重大的安全挑战。
系统合约中使用汇编的挑战
计划于今年年初进行的 Pectra 硬分叉包含了 11 个以太坊改进提案（EIPs），其中三个涉及执行链上逻辑的系统合约。值得注意的是，这些合约使用汇编语言来提高性能。因此，它们绕过了编译器安全检查，增加了漏洞风险。缺乏编译器强制执行的安全检查要求开发者手动实施安全措施，这一过程易于出现人为错误。
形式化验证：解决方案
为了应对这些挑战，使用 Halmos 工具进行形式化验证，确保合约的汇编代码是安全且正确的。这一过程涉及通过数学证明验证系统合约是否符合其规范。生成的验证工件不仅加强了 Pectra 升级的安全性，还为其他汇编代码开发者提供了示例。
Pectra 的特定 EIPs 及其功能
Pectra 硬分叉包括几个值得注意的 EIPs：
- EIP-2935：此提案引入了一个用于存储最后 8191 个区块哈希的系统合约，促进无状态执行。
- EIP-7002：它使验证者能够直接发起退出和提款，利用一个专用的系统合约。
- EIP-7251：此 EIP 提议增加验证者的最大有效余额，使其能够有效整合操作。
形式化验证的蓝图
形式化验证过程分为两个主要阶段：模型验证和精化证明。模型验证涉及形式化规范和证明关键属性，而精化证明确保实现与这些规范一致。诸如 Halmos 之类的工具通过自动验证 EVM 字节码来促进这一过程，降低人为错误的风险。
效率和持续验证
Halmos 在初始和持续验证过程中都被证明是有效的。它能够在代码更新后进行有效的再次验证，确保实现始终正确和安全。这个持续的验证过程非常重要，因为它在代码重构过程中检测到了错误，强调了其在维护代码可靠性方面的重要性。
通过使用类似 Halmos 的形式化验证工具，开发者可以在性能和安全性之间取得平衡，确保优化不会以牺牲安全性为代价。这种方法不仅增强了对低级实现的信心，也证明了在区块链开发中安全性可以与效率共存。
Image source: Shutterstock