{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:16:33Z","timestamp":1773479793405,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","funder":[{"name":"Estonian Research Council","award":["PSG749"],"award-info":[{"award-number":["PSG749"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765115","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:37:25Z","timestamp":1763854645000},"page":"2714-2728","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards a Formal Foundation for Blockchain ZK Rollups"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5414-4120","authenticated-orcid":false,"given":"Stefanos","family":"Chaliasos","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom and zkSecurity, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1267-7898","authenticated-orcid":false,"given":"Denis","family":"Firsov","sequence":"additional","affiliation":[{"name":"Input Output, Tallinn, Estonia and Tallinn University of Technology, Tallinn, Estonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4921-8452","authenticated-orcid":false,"given":"Benjamin","family":"Livshits","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_3_2_1_2_1","unstructured":"Barry Whitehat. 2018. Roll Up Token. https:\/\/github.com\/barryWhiteHat\/roll_up_token. Accessed: 2024-03-19."},{"key":"e_1_3_2_1_3_1","volume-title":"Sui Lutris: A blockchain combining broadcast and consensus. arXiv preprint arXiv:2310.18042","author":"Blackshear Same","year":"2023","unstructured":"Same Blackshear, Andrey Chursin, George Danezis, Anastasios Kichidis, Lefteris Kokoris-Kogias, Xun Li, Mark Logan, Ashok Menon, Todd Nowacki, Alberto Sonnino, et al., 2023. Sui Lutris: A blockchain combining broadcast and consensus. arXiv preprint arXiv:2310.18042 (2023)."},{"key":"e_1_3_2_1_4_1","volume-title":"Aline Inacio Cunha, and Nuno Macedo","author":"Brunel Julien","year":"2021","unstructured":"Julien Brunel, David Chemouil, Aline Inacio Cunha, and Nuno Macedo. 2021. Formal Software Design with Alloy 6. https:\/\/haslab.github.io\/formal-software-design\/overview\/index.html. Accessed: 2025-07-14."},{"key":"e_1_3_2_1_5_1","volume-title":"Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?. In Proceedings of the International Conference on Software Engineering.","author":"Chaliasos Stefanos","year":"2024","unstructured":"Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, and Benjamin Livshits. 2024a. Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?. In Proceedings of the International Conference on Software Engineering."},{"key":"e_1_3_2_1_6_1","volume-title":"SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs. arXiv preprint arXiv:2402.15293","author":"Chaliasos Stefanos","year":"2024","unstructured":"Stefanos Chaliasos, Jens Ernstberger, David Theodore, David Wong, Mohammad Jahanara, and Benjamin Livshits. 2024b. SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs. arXiv preprint arXiv:2402.15293 (2024)."},{"key":"e_1_3_2_1_7_1","unstructured":"Kelvin Fichter. [n.d.]. Why is the Optimistic Rollup challenge period 7 days? https:\/\/kelvinfichter.com\/pages\/thoughts\/challenge-periods\/."},{"key":"e_1_3_2_1_8_1","unstructured":"Denis Firsov and Benjamin Livshits. 2024. The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation. Cryptology ePrint Archive Paper 2024\/768. https:\/\/eprint.iacr.org\/2024\/768 https:\/\/eprint.iacr.org\/2024\/768."},{"key":"e_1_3_2_1_9_1","volume-title":"Foundry: Blazing fast, portable and modular toolkit for Ethereum application development. https:\/\/github.com\/foundry-rs\/foundry. Accessed: 2025-04-14.","author":"Foundry","year":"2021","unstructured":"Foundry contributors. 2021. Foundry: Blazing fast, portable and modular toolkit for Ethereum application development. https:\/\/github.com\/foundry-rs\/foundry. Accessed: 2025-04-14."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437378.3437879"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3550355.3552462"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22178"},{"key":"e_1_3_2_1_13_1","volume-title":"A Rollup Comparison Framework. arXiv preprint arXiv:2404.16150","author":"Gorzny Jan","year":"2024","unstructured":"Jan Gorzny and Martin Derka. 2024. A Rollup Comparison Framework. arXiv preprint arXiv:2404.16150 (2024)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3565383.3566107"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_3_2_1_16_1","article-title":"Alloy: a lightweight object modelling notation","volume":"11","author":"Jackson Daniel","year":"2002","unstructured":"Daniel Jackson. 2002. Alloy: a lightweight object modelling notation. Transactions on software engineering and methodology (TOSEM), Vol. 11, 2 (2002).","journal-title":"Transactions on software engineering and methodology (TOSEM)"},{"key":"e_1_3_2_1_17_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson Daniel","unstructured":"Daniel Jackson. 2012. Software Abstractions: logic, language, and analysis. MIT press."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/226295.226322"},{"key":"e_1_3_2_1_20_1","volume-title":"USENIX Security Symposium.","author":"Kalodner Harry","year":"2018","unstructured":"Harry Kalodner, Steven Goldfeder, Xiaoqi Chen, S Matthew Weinberg, and Edward W Felten. 2018. Arbitrum: Scalable, private smart contracts. In USENIX Security Symposium."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3631310.3633493"},{"key":"e_1_3_2_1_22_1","volume-title":"Hugo Daniel Macedo, Steve Schneider, Peter WV Tran-J\u00f8rgensen, and James Woodcock.","author":"Kulik Tomas","year":"2022","unstructured":"Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter WV Tran-J\u00f8rgensen, and James Woodcock. 2022. A survey of practical formal methods for security. Formal aspects of computing, Vol. 34, 1 (2022)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3065880"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICBC56567.2023.10174993"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3410699.3413800"},{"key":"e_1_3_2_1_26_1","volume-title":"SoK: Decentralized sequencers for rollups. arXiv preprint arXiv:2310.03616","author":"Motepalli Shashank","year":"2023","unstructured":"Shashank Motepalli, Luciano Freitas, and Benjamin Livshits. 2023. SoK: Decentralized sequencers for rollups. arXiv preprint arXiv:2310.03616 (2023)."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/NTMS.2019.8763832"},{"key":"e_1_3_2_1_28_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system.","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008)."},{"key":"e_1_3_2_1_29_1","unstructured":"Chandrakana Nandi Mooly Sagiv and Daniel Jackson. 2025. Certora Technology White Paper: Unveiling the Power and Limitations of Certora's Smart Contract Verification Technology. https:\/\/www.certora.com\/blog\/white-paper Accessed: 2025-04-14."},{"key":"e_1_3_2_1_30_1","volume-title":"SoK: Comprehensive Analysis of Rug Pull Causes, Datasets, and Detection Tools in DeFi. arXiv preprint arXiv:2403.16082","author":"Sun Dianxiang","year":"2024","unstructured":"Dianxiang Sun, Wei Ma, Liming Nie, and Yang Liu. 2024. SoK: Comprehensive Analysis of Rug Pull Causes, Datasets, and Detection Tools in DeFi. arXiv preprint arXiv:2403.16082 (2024)."},{"key":"e_1_3_2_1_31_1","volume-title":"Blockchain scaling using rollups: A comprehensive survey","author":"Thibault Louis Tremblay","year":"2022","unstructured":"Louis Tremblay Thibault, Tom Sarry, and Abdelhakim Senhaji Hafid. 2022. Blockchain scaling using rollups: A comprehensive survey. IEEE Access, Vol. 10 (2022)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07535-3_12"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589334.3645431"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318041.3355457"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-48731-6_5"},{"key":"e_1_3_2_1_36_1","volume-title":"Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper","author":"Gavin Wood","year":"2014","unstructured":"Gavin Wood et al., 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, Vol. 151, 2014 (2014)."},{"key":"e_1_3_2_1_37_1","volume-title":"Solana: A new architecture for a high performance blockchain v0. 8.13. Whitepaper","author":"Yakovenko Anatoly","year":"2018","unstructured":"Anatoly Yakovenko. 2018. Solana: A new architecture for a high performance blockchain v0. 8.13. Whitepaper (2018)."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/IWBOSE.2019.8666514"},{"key":"e_1_3_2_1_39_1","unstructured":"Zeeve. [n.d.]. https:\/\/paragraph.xyz\/@zeeve\/a-holistic-view-of-solutions-to-reduce-7-day-finality-in-op-rollups."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179435"},{"key":"e_1_3_2_1_41_1","volume-title":"Solutions to scalability of blockchain: A survey. Ieee Access","author":"Zhou Qiheng","year":"2020","unstructured":"Qiheng Zhou, Huawei Huang, Zibin Zheng, and Jing Bian. 2020. Solutions to scalability of blockchain: A survey. Ieee Access (2020)."}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","location":"Taipei Taiwan","acronym":"CCS '25","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:22:10Z","timestamp":1766442130000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":41,"alternative-id":["10.1145\/3719027.3765115","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765115","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}