超越L2的成熟度：构建安全区块链Rollups的形式化方法 - ZKSECURITY

2024 年，我们与 Matter Labs 合作发布了一篇关于区块链 Rollup 安全性的论文。该论文分析了区块链 rollup 的安全性，并引入了一个正式的模型来推理不同的机制。你可以在 arxiv 上找到该论文。在这篇博文中，我们将讨论 Rollup 的安全性，并对我们在论文中所做的工作进行简单介绍。

Vitalik Buterin 在他最近的博客文章中强调，虽然以太坊的目标是成为一个稳健的、多用途的区块链，但它自身能处理的事务量是有限的。为了保持去中心化和安全性，以太坊本身必须抵制捷径——从而限制了我们能从基础层中挤出多少容量（“可扩展性”）。

进入 Rollup

Rollup 通过将交易从主链转移到 Layer 2 (L2) 链来缓解这个问题，从而在仍然继承以太坊安全性的同时显著提高吞吐量（稍后会详细介绍）。已经出现了两种流行的 rollup 类型：

• Optimistic Rollups: 假设“批量处理”的交易是正确的，如果怀疑有错误，则依赖于链上挑战或欺诈证明。
• ZK-Rollups: 依赖于密码学证明（零知识证明——或者更准确地说，简洁证明），因此无效的批次根本无法在以太坊上最终确定。

Vitalik 的博文强调，rollup 不仅仅是一个短期解决方案。它们现在是以太坊长期愿景的核心要素，将包括增加数据可用性的更广泛的路线图联系在一起。通过“链下”捆绑交易并在“链上”确认它们，rollup 以一种纯粹的链上扩展无法完成的方式平衡了可扩展性和安全性而不会损害其他方面。

在实践中，rollup 是新的链，它们在 L1 区块链上发布和验证其状态更新（或交易）。

L2BEAT 以及更安全、更便宜交易的竞赛

L2BEAT 团队做出了重大努力，以提高人们对 L2 解决方案（尤其是 rollup）的增长和成熟度的认识。除了增长指标外，L2BEAT 还引入了一个“阶段”框架，旨在阐明每个 L2 的成熟度。这些“阶段”不衡量代码的复杂性；它们反映了治理结构、sequencer 的去中心化，以及如果出现问题用户可以多快退出。

总结 L2BEAT 阶段的要点：

• Stage 0: 具有中心化或“辅助轮”模型的早期项目。
• Stage 1 & 2: 朝着对升级和证明进行更去中心化的控制迈进。对运营商仍存在一些信任。
• Stage 3 & Beyond: 最终或接近最终的成熟度，具有强大的抗审查性、对运营商的最小信任以及具有时间锁或社区治理的明确定义的升级路径。

L2BEAT 的观点有助于社区理解“足够去中心化”不是一个单一的时刻。相反，它是一个增量变化的路线图，最终提供与以太坊相同的信任属性。

超越成熟度标签

到目前为止，我们一直认为 L2 继承或受益于以太坊的安全性。L1 上的安全性意味着攻击者需要破坏网络中很大一部分节点才能使单个交易失败。要说 L2 继承了 L1 的安全性和抗审查性，必须满足一些属性。据我们所知，目前没有通用 rollup 真正继承了 L1 的安全性。请注意，L2 区块链通常非常中心化，以实现更高的吞吐量和成本效率（在大多数情况下，只有一个集中的运营商）。

直观地说，L2 用户必须能够验证他们的交易是否已包含在 L1 上并已正确执行（L1 上的数据可用性加上密码学证明或欺诈证明以及挑战期）。除此之外，如果 L2 审查它们，用户必须能够通过 L1 提交交易。最后，L2 上的升级应该在 L1 上宣布，并有一个时间锁，直到它们被应用，因此如果升级对他们有害，用户可以退出。

目前，在大多数 L2 中，如果攻击者设法控制了控制 L1 上 L2 智能合约的多重签名，他们可能会通过应用恶意升级来“rug”L2 并掠夺所有用户资金。例如，在 ZK-Rollup 中，他们可以更新验证器以接受任何证明。由于某些 L2 可能还需要“良性”的黑名单机制（例如，出于监管原因），因此它们可能需要复杂的附加功能才能满足所有这些要求。

Rollup 安全性的正式基础

虽然成熟度框架（如 L2BEAT 的阶段）给出了 rollup 去中心化程度和用户友好程度的高级概述，但它们并不总是深入研究精确的、正式的保证。我们的论文“迈向区块链 Rollup 的正式基础”旨在做到这一点：

1. 提出 rollup 协议必须满足的关键安全属性的严格规范。
2. 使用形式化方法（特别是通过 Alloy 进行的模型检查）来验证 rollup 的设计是否支持这些属性。

特别是，我们的工作深入研究了定义真正最小化信任的 rollup 的三个关键机制：

1. 强制交易（强制队列）
   • 它是什么: 用户绕过 sequencer 审查的一种方式，通过将交易直接推送到以太坊的 L1 合约。
   • 为什么重要: 即使 rollup sequencer 宕机或恶意，用户交易也无法被阻止。
2. 安全黑名单
   • 它是什么: 如果 rollup 选择合并黑名单（例如，出于监管原因），则必须以不会捕获合法用户交易或破坏强制队列的方式进行。
   • 为什么重要: 平衡了现实世界中需要将某些地址列入黑名单的需求与用户对其资金控制权的基本原则。
3. 可升级性
   • 它是什么: Rollup 合约通常需要发展，无论是为了添加功能还是修复错误，但幼稚的升级可能会被利用或用于“rug pull”用户资金。
   • 为什么重要: 通过强制执行链上强制等待期并保证所有强制交易在升级之前得到处理，用户有足够的时间在不同意更改时退出。

形式化分析如何提供帮助

使用 Alloy —— 一种最著名的高级建模工具 —— 我们可以系统地探索高达一定范围的 rollup 状态转换的每种可能的组合。这种方法突出了设计阶段的极端情况，有效地让我们说：“如果存在强制交易仍然受到审查的情况，Alloy 会发现它。”

这与 L2BEAT 的阶段是互补的，L2BEAT 的阶段定义了减少信任的渐进式路径。换句话说，虽然 L2BEAT 告诉你 rollup 在去中心化旅程中的位置，但形式化分析有助于确保 rollup 的核心合约逻辑是严密的 —— 并且它真正强制执行它声称提供的最小信任假设。

为什么这对以太坊的未来很重要

• 保护数十亿美元的资产: Rollup 越来越多地保护重要资金。形式化方法可以帮助保证不可能出现极端情况下的“rug pull”或永久性交易审查。
• 建立生态系统可信度: 正如 Vitalik 的博文所强调的那样，rollup 是以太坊路线图的核心部分。严格地指定和验证它们可以增强用户和生态系统开发人员之间的信任。
• 与成熟度模型保持一致: 我们的形式化方法可以改进 L2BEAT 阶段，使其更具信息性。如果 rollup 声称是 Stage 3，则形式化验证可以证明其强制交易队列或升级路径是否真正符合该标准。

结论

正如 Vitalik 的博文中所强调的那样，以太坊正在更深入地进入以 rollup 为中心的未来。L2BEAT 的成熟度阶段帮助我们了解不同的 L2 在去中心化旅程中的进展情况。但是，为了确保这些 rollup 真正按照他们声称的方式运行 —— 尤其是在最坏的情况下 —— 我们需要对其关键机制进行正式的、数学的验证。这正是我们的论文着手要做的事情。

如果你想了解更多关于我们框架的信息，或者你正在开发 L2 并希望将我们的 Alloy 模型应用于你的机制，请随时与我们联系。

• 原文链接： blog.zksecurity.xyz/post...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～