区块链 Rollup 形式化基础研究
密码学与安全
2025-09-16 v3
摘要
比特币和以太坊等区块链彻底革新了数字交易，但仍面临可扩展性问题。Layer 2 解决方案（如有效性证明 Rollup，ZK-Rollup）旨在通过离链处理交易并在主链上验证来解决这些挑战。然而，安全性和抗审查能力仍是关切，尤其是 Layer 2 控制中心化，以及通过 Layer 1 智能合约不足以强制执行这些属性。当前的 L2 面临多签攻击，可能导致用户资金全盘损失。本工作采用 Alloy 规范语言进行形式化分析，考察和设计关键 Layer 2 功能，包括强制交易队列、安全黑名单和可升级性。通过该分析，我们识别了现有设计中的漏洞，提出了增强模型并通过模型检验证明其正确性。最后，我们提出了基于手动将 Alloy 属性翻译为属性测试不变量的完整端到端方法来分析 Rollup 的安全性和抗审查能力，树立了新标准。
引用
@article{arxiv.2406.16219,
title = {Towards a Formal Foundation for Blockchain Rollups},
author = {Stefanos Chaliasos and Denis Firsov and Benjamin Livshits},
journal= {arXiv preprint arXiv:2406.16219},
year = {2025}
}
备注
Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS '25), October 13--17, 2025, Taipei, Taiwan