Paper 2024/1834

Scutum: Temporal Verification for Cross-Rollup Bridges via Goal-Driven Reduction

Yanju Chen, University of California, Santa Barbara
Juson Xia, Orbiter Finance
Bo Wen, Orbiter Finance
Kyle Charbonnet, Ethereum Foundation
Hongbo Wen, University of California, Santa Barbara
Hanzhi Liu, University of California, Santa Barbara
Yu Feng, University of California, Santa Barbara
Abstract

Scalability remains a key challenge for blockchain adoption. Rollups—especially zero-knowledge (ZK) and optimistic rollups—address this by processing transactions off-chain while maintaining Ethereum’s security, thus reducing gas fees and improving speeds. Cross-rollup bridges like Orbiter Finance enable seamless asset transfers across various Layer 2 (L2) rollups and between L2 and Layer 1 (L1) chains. However, the increasing reliance on these bridges raises significant security concerns, as evidenced by major hacks like those of Poly Network and Nomad Bridge, resulting in losses of hundreds of millions of dollars. Traditional security analysis methods such as static analysis and fuzzing are inadequate for cross-rollup bridges due to their complex designs involving multiple entities, smart contracts, and zero-knowledge circuits. These systems require reasoning about temporal sequences of events across different entities, which exceeds the capabilities of conventional analyzers. In this paper, we introduce a scalable verifier to systematically assess the security of cross-rollup bridges. Our approach features a comprehensive multi-model framework that captures both individual behaviors and complex interactions using temporal properties. To enhance scalability, we approximate temporal safety verification through reachability analysis of a graph representation of the contracts, leveraging advanced program analysis techniques. Additionally, we incorporate a conflict-driven refinement loop to eliminate false positives and improve precision. Our evaluation on mainstream cross-rollup bridges, including Orbiter Finance, uncovered multiple zero-day vulnerabilities, demonstrating the practical utility of our method. The tool also exhibited favorable runtime performance, enabling efficient analysis suitable for real-time or near-real-time applications.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint.
Keywords
Cross-Rollup BridgeFormal VerificationSecurityProgram Analysis
Contact author(s)
yanju @ ucsb edu
zerokpunk @ orbiter finance
wenbo @ orbiter finance
kylecharbonnet @ gmail com
hongbowen @ ucsb edu
hanzhi @ ucsb edu
yufeng @ ucsb edu
History
2024-11-08: revised
2024-11-08: received
See all versions
Short URL
https://ia.cr/2024/1834
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2024/1834,
      author = {Yanju Chen and Juson Xia and Bo Wen and Kyle Charbonnet and Hongbo Wen and Hanzhi Liu and Yu Feng},
      title = {Scutum: Temporal Verification for Cross-Rollup Bridges via Goal-Driven Reduction},
      howpublished = {Cryptology {ePrint} Archive, Paper 2024/1834},
      year = {2024},
      url = {https://eprint.iacr.org/2024/1834}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.