# Towards a Formal Foundation for
Blockchain Rollups

Stefanos Chaliasos13, Denis Firsov2, and Benjamin Livshits12  1Imperial
College London, United Kingdom 2Matter Labs 3zkSecurity

###### Abstract

Blockchains like Bitcoin and Ethereum have revolutionized digital
transactions, yet scalability issues persist. Layer 2 solutions, such as
validity proof Rollups (ZK-Rollups), aim to address these challenges by
processing transactions off-chain and validating them on the main chain.
However, concerns remain about security and censorship resistance,
particularly regarding centralized control in Layer 2 and inadequate
mechanisms for enforcing these properties through Layer 1 contracts. This work
presents a formal analysis using the Alloy specification language to examine
and design key Layer 2 functionalities, including forced transaction queues,
safe blacklisting, and upgradeability. Through this analysis, we identify
potential vulnerabilities in current mechanisms and propose enhanced models to
strengthen security and censorship resistance, setting new standards for the
security of rollups.

##  1 Introduction

Blockchain technology, exemplified by major chains such as Bitcoin [1] and
Ethereum[2], has revolutionized finance and various other fields by enabling
decentralized transactions. Despite its innovations, the adoption of these
technologies has highlighted significant scalability challenges. The limited
transaction throughput of these networks has led to ongoing research and
development of various scalability solutions within the community [3].

Two primary strategies have emerged to enhance scalability. The first strategy
involves developing new blockchain architectures from scratch, designed for
higher transaction throughput than traditional platforms like Ethereum [4, 5],
often at the expense of reduced security and network effects. The second
strategy focuses on Layer 2 (L2) solutions, particularly rollups, which have
become prominent in practical applications [6]. Rollups enhance scalability by
executing transactions on a secondary blockchain (L2) and subsequently posting
the state roots and transaction data back to the primary blockchain (L1). This
approach allows rollups to inherit the security properties of the underlying
L1 blockchain through the use of validity proofs [7], i.e., Zero-Knowledge
Proofs (ZKPs) [8], or fraud proofs [9].

However, simply submitting transaction batches for verification by L1
contracts does not fully secure L2 users. Centralized control of L1 contracts
through mechanisms like multi-signature wallets poses some significant
security risks. If a malicious party gains control of the majority of the
keys, they could potentially redirect or steal funds. Notably, even if a
proper governance protocol is in place, the issues that might occur from
instant upgrades still hold. Further, the potential for censorship by L2
operators poses another major challenge, as users could be prevented from
executing transactions.

###  1.1 Motivating Examples

Blast incident. A recent incident involving the Blast
rollup,111https://x.com/miszke_eth/status/1775196752993255613 which holds over
$3 billion in total value locked (TVL), highlights these issues. Following a
major exploit in one of the protocols deployed on Blast, the operators quickly
intervened to censor the attacker by upgrading the system. Although well-
intentioned, this action highlighted that L2s currently do not offer the same
level of security and censorship resistance as their underlying L1
blockchains, as rapid changes could lead to substantial asset losses. Further,
it highlights the upgrade power of the rollup operator without any safety
mechanism in place to protect users. The code change in contract
OptimismPortal.sol222https://etherscan.io/address/0xA280aEBF81c917DbD2aA1b39f979dfECEc9e4391#code#F1#L449
shown in Figure 1 highlights the rapidly deployed contract changes used by the
Blast rollup operator to censor the attacker.

⬇

439address from = msg.sender;

440if (msg.sender != tx.origin) {

441 from = AddressAliasHelper.applyL1ToL2Alias(msg.sender);

442}

443// ...

444require(

445 from != 0x6E8836F050A315611208A5CD7e228701563D09c5 &&

446 from != 0xc207Fa4b17cA710BA53F06fEFF56ca9d315915B7 &&

447 from != 0xbf9ad762DBaE603BC8FC79DFD3Fb26f2b9740E87

448);

Figure 1: Censoring changes in the Blast OptimismPortal.sol contract.

dydx concerns. Concerns regarding the excessive authority of the rollup
operator to execute a rug pull [10] on its users apply to the dydx rollup,
which is controlled via a 3-out-of-5 multi-
sig333https://www.odaily.news/en/post/5191266, which means that only three
rogue parties are enough to hijack the entire rollup and lead to an immediate
code upgrade.

[leftmargin=0pt, vskip=0pt] Anyone who wants to upgrade the Layer 2 contract
must be subject to the time lock delay limit, and the contract upgrade should
take effect later than the mandatory withdrawal. For example, the contract
upgrade of dydx now has a delay of at least 48 hours, so the delay for the
forced withdrawal/escape hatch mode to take effect should be reduced to within
48 hours. In this way, after users discover that the dYdX project team wants
to incorporate malicious code into the new version of the contract, they can
withdraw their assets from Layer 2 to Layer 1 before the contract is updated.

In the rest of this paper, we show that the situation is even more complex: as
demonstrated in Section 4.5, a timelock alone is insufficient; A secure
upgrade process that must be followed by the rollup operator, regardless of
who controls the upgrade decision, is essential.

Linea hack. In June 2024, the Linea chain was halted in response to a project
on Linea that was compromised, and some addresses were black-listed. Citing
the Linea team’s
communications444https://x.com/LineaBuild/status/1797283402745573837
555https://cryptoslate.com/linea-under-scrutiny-for-unilateral-block-
production-halt-amid-velocore-hack/; this issue had similar implications to
the _Blast incident_ :

[leftmargin=0pt, vskip=0pt] The sequencer was paused from block 5081800 and
5081801. During this pause, we gave the @Velocorexyz time team to support
their efforts of triaging the vulnerability. We also censored the hacker’s
addresses. This significantly reduced the ecosystem impact on Linea users. …
Linea’s team made a decision to halt block production by pausing the sequencer
and censor attacker addresses to protect the users and builders in our
ecosystem. Like other L2s, we are still in the "training wheels" phase of
existence, giving us safeguards to use. … Meanwhile, teams at Velocore and
Linea have requested to CEX to freeze the exploited funds, and Velocore is
setting up an onchain negotiation process.

###  1.2 Paper Overview

In this work, we are the first, to the best of our knowledge, to formalize and
analyze essential mechanisms that L2 rollups must implement to truly inherit
the security and censorship resistance of their underlying L1 blockchains.
Using the Alloy specification language, we define and test critical security
properties that these mechanisms should exhibit. Our framework aims to guide
the development of robust L2 mechanisms, providing concrete security
guarantees to L2 users. We focus on ZK-Rollups, regarded as some of the most
secure solutions, and explore the following critical mechanisms:

Forced Queue. A mechanism implemented in the L1 contracts that allows users to
bypass potential L2 censorship by submitting transactions directly to the L1.
This mechanism is supported, or planned to be supported, by some of the top
rollups, both optimisitic and several ZK-Rollups, as shown on the L2beat Risk
page.666https://l2beat.com/scaling/risk

Blacklisting. Recognizing that strong guarantees of the previous mechanism
could lead to regulatory challenges, we propose a secure optional mechanism
for enforcing blacklisting policies. This mechanism prevents immediate
blocking of users, as highlighted in Section 1.1, and should ideally be
updated through a governance process.

Upgradeability. We outline a secure approach to upgrading system components
that preserves user security and is compatible with previous mechanisms. The
need for secure upgrades is further justified by recent rollup incidents where
block production was stopped, followed by an immediate upgrade. We also
highlight common pitfalls in the state-of-the-art upgradeability mechanisms
and demonstrate potential vulnerabilities through counter-example-driven
reasoning.

In this work, we introduce mechanisms grounded in formal modeling of rollup
protocols designed to mitigate issues such as those discussed in Section 1.1.
Specifically, we describe a safe upgradeability mechanism that is required to
resolve all three examples (Section 4.5). Additionally, for scenarios outlined
in the first and third examples, we describe a secure blacklisting mechanism
(Section 4.4) that further helps address the issues.

###  1.3 Contributions

  * •

Formal model for ZK-Rollup security: Together with a threat model (Section 3),
we introduce the first formal model for ZK Rollup smart contracts operating on
Layer 1 blockchains, responsible for the security of L2 (Section 4.2). This
model is designed to be both adaptable and extensible, facilitating
comprehensive analyses of core design properties essential for the development
of secure ZK-Rollups. This model aims to guide implementers and operators of
ZK-Rollups.

  * •

Analysis of key mechanisms: We conduct a detailed analysis of three essential
mechanisms integral to ZK-Rollups: the forced queue, safe blacklisting, and
upgradeability (Section 4). Our analysis identifies common design pitfalls and
offers robust designs that integrate these mechanisms securely, ensuring they
function correctly. We also outline security properties that each mechanism
must satisfy. We aim to provide correct-by-construction models for these
mechanisms as opposed to post-factum analysis of either code or designs.

  * •

Evaluation of state-of-the-art mechanisms: Using our Alloy model, we analyze
current ZK Rollup designs, highlighting issues in upgrade policies with
concrete counterexamples (Section 5). We show that our proposed upgradeability
mechanism is secure, setting a new standard for ZK Rollup security. We also
discuss how the Alloy models can be used for design-time testing (Section 6).
Finally, we demonstrate that the Alloy-based approach is practical in terms of
running time while effectively identifying critical counterexamples (Section
7).

We share our Alloy code at the following location:
https://github.com/StefanosChaliasos/zk-rollup-security.

##  2 Background

###  2.1 Blockchain Scalability and ZK-Rollups

Blockchain scalability has been a persistent challenge, particularly for
established networks like Ethereum [2], which processes only tens of
transactions per second (TPS).777https://l2beat.com/scaling/summary The
scalability trilemma [11] posits that blockchain systems cannot simultaneously
achieve scalability, decentralization, and security without compromises. This
has led to efforts to enhance scalability, focusing on two primary strategies:
base layer scaling (or Layer 1 — L1) and Layer 2 (L2) scaling solutions. Base
layer scaling, which includes techniques such as sharding [12] and novel
consensus protocols [13], involves either the modification of existing
blockchains – a complex and daunting task – or the development of new
blockchain architectures. While modern blockchains like Solana [4] and Sui [5]
have demonstrated success, they often lack the established security,
liquidity, and comprehensive ecosystem found in legacy blockchains like
Ethereum.888As of 10/5/2024, Ethereum has 57.85% of the total TVL for all
chains, while Solana only has 4.46%, according to
https://defillama.com/chains.

Rollups [6] have emerged as hybrid L2 solutions, distinguishing themselves by
offloading computation off-chain while retaining and validating data on-chain,
thus addressing the data availability issue while inheriting L1’s security.
Rollups batch and execute transactions on an L2 blockchain and submit the
results into L1.

The execution of transactions in the L2 instead of L1 allows rollups to
process significantly more transactions per second than their L1 counterparts.
By submitting a single L1 transaction for a batch, which might include up to
4K L2 transactions at the moment999That is the current batch size for zkEsync
Era., to the underlying blockchain, rollups not only scale the total TPS but
also ensure data availability and inherit the security properties of the L1
network. Altering the L2 state recorded on L1 would require breaking
substantial security, which would be both difficult and costly. This
architecture enables rollups to offer an efficient and secure scaling solution
for legacy blockchains. This model, i.e., rollup-centric scaling, has gained
traction as the principal method for scaling Ethereum, with two predominant
variants: optimistic rollups [9] and ZK-Rollups [7].101010As of 10/5/2024,
rollups have more than 37B USD TVL according to https://l2beat.com.

Optimistic rollups rely on a system of trust, assuming transactions are valid
unless challenged, which makes the implementation of the L2 simpler but
introduces delays and adds complexity to rollup’s contracts logic due to the
fraud-proof mechanism. In contrast, ZK-Rollups use ZKPs to validate
transactions in the L1 as soon as a proof has been created off-chain and
submitted to the L1 contracts, ensuring faster finality but a higher
computational and complexity cost in the L2 level. While Optimistic rollups
are generally easier to implement, they suffer from potential delays in
withdrawals (currently, most L2s apply a 7-day long challenge period); ZK-
Rollups, on the other hand, offer faster finality and more compression
opportunities (e.g., state diffs — not all transaction data need to be posted
in the L1) to the data submitted to the L1, leading to smaller costs.

Figure 2: High-level architecture overview of ZK-Rollups. EOA: Externally
owned address.

Components of ZK-Rollups. As illustrated in Figure 2, ZK-Rollups consist of
several key L2 components, including the Sequencer and the Prover. The
Sequencer is responsible for processing, ordering, and executing transactions
into batches. Although currently often centralized, there is ongoing research
aimed at decentralizing this component to enhance system trustworthiness and
resilience [14]. The Prover, on the other hand, generates cryptographic proofs
of the correctness of these batches. Note that both components can be split
into various other components (e.g., executor, L1-L2 relayer, and prover
coordinator). The rollup’s smart contracts, deployed on the L1, are essential
to the overall architecture, executing various critical operations. These
contracts must be analyzed to determine if they meet the properties detailed
in Section 3.

L1 Smart Contract Operations. L1 contracts are used to _(i)_ commit the
transaction batches prepared by the Sequencer, which includes posting
transaction data necessary for proof generation, verification, and
reproduction of the L2 state. L1 contracts also _(ii)_ verify the
cryptographic proofs produced by the Prover to ensure that all transactions in
a batch are correctly executed. Further, _(iii)_ in cases where transactions
need to be pushed through despite potential censorship, downtime, or
adversarial actions by the L2 operators, the L1 contracts can enforce
transactions. Smart contracts on L1 also _(iv)_ manage protocol upgrades,
which can include changes to the rollup’s operational logic or security
parameters, ensuring that upgrades occur smoothly without compromising ongoing
operations or security. Finally, _(v)_ these contracts manage cross-layer
transactions for depositing and withdrawing from the L2.

Transaction lifecycle in ZK-Rollups. The process begins when a user signs and
submits a transaction to the L2 network, marking it as Pending. It quickly
becomes Preconfirmed once the sequencer processes and includes the transaction
in a block. The transaction then becomes Committed when included in a batch
that is submitted to the L1 contract, which allows for reconstruction and
verification of the L2 state based on data posted to L1. Finally, the
transaction reaches the Verified/Finalized stage when the batch’s proof is
validated by the L1 contract, ensuring the transaction and its associated
state are immutable and secure on L2. Additionally, transactions can also be
submitted directly through the L1 contracts in scenarios where L2 operators
may be censoring transactions or in cases of L2 downtime, ensuring robustness
against operational failures or malicious activities.

###  2.2 Formal Modeling of Software Design

Formal modeling enhances the correctness and robustness of software systems
through a rigorous analysis of their designs. By providing a precise
mathematical description, formal modeling facilitates the verification of
properties and behaviors before implementation, thereby reducing errors and
improving system reliability.

Alloy [15, 16] is a declarative specification language using first-order
relational logic to model complex systems succinctly, ideal for expressing
constraints and behaviors in software designs. The Alloy Analyzer automates
checking these models against specified properties, leveraging SAT solvers to
find solutions or identify inconsistencies within a bounded scope.

Alloy has been used in various research projects to model and verify the
properties of software architectures and protocols. For instance, Akhawe et
al. [17] utilized Alloy to model web security mechanisms, demonstrating the
language’s utility in capturing complex interactions and verifying security
properties while revealing three previously unknown vulnerabilities. This
exemplifies how Alloy facilitates a deep understanding and validation of
complex systems in practical applications.

In this paper, we use Alloy to specify and examine the security attributes of
ZK-Rollups. We create formal models of the contract interactions within ZK-
Rollups, outlining key properties for mechanisms such as forced transactions
and upgradeability. Using the Alloy Analyzer, we not only validate the
accuracy of certain designs, but also uncover weaknesses in simplistic
designs, highlighting their security issues. To quote the Alloy book [15],
_“In this respect, the Alloy language and its analysis are a Trojan horse: an
attempt to capture the attention of software developers, who are mired in the
tar pit of implementation technologies, and to bring them back to thinking
deeply about underlying concepts”_.

##  3 Threat Model and Goals

###  3.1 Threat Model

We construct a robust adversary model to rigorously assess the security of the
mechanisms presented in this paper. This model assumes that the L2 network is
malicious, with no trust assumptions regarding its correct operation. We
consider an adversary capable of gaining complete control over the L2 network,
emphasizing the importance of properly designing ZK-Rollups’ mechanisms and
smart contracts.

Principals. The main principals in ZK-Rollups are users, rollup operators, and
rollup administrators.

Users. Users interact with the L2 either by submitting their transactions
directly to the L2 network, i.e., the rollup operators, or by submitting them
through the rollup’s contract on the L1 via the forced queue.

Rollup operators. Rollup operators handle the components that sequence user
transactions in the L2 into batches, commit them in the L1, and request
validity proofs (c.f. Figure 2). They may also receive the proofs and submit
them to the L1. Currently, in most L2s, there is a single centralized entity
operating the L2, but in our model, the operator could be controlled by one or
many entities that do not need to be trustworthy.

Rollup administrators. In addition to rollup operators, some entities have
administrator capabilities for the L1 blockchain smart contracts of the L2.
Administrators can be white-listed or elected via governance mechanisms. These
administrators have the ability to request system upgrades or update
blacklists. In practice, currently, the administrator capabilities are
assigned to a multi-sig that could be controlled by some distinct entities.
The mechanisms we describe in this paper should maintain security even if
administrators are malicious.

Security assumptions.

  * •

The underlying _L1 remains secure_ and maintains liveness to enable progress
of L2 operations. Should L1 face downtime, L2 operations might be delayed as
well, but the security of the L2 would remain intact, thus preserving system
safety.

  * •

The _cryptographic primitives (ZKPs) and their implementation are assumed to
be secure_ [18], ensuring that no verifier accepts an invalid proof of
execution. This assumption also extends to the correctness of any trusted
setup procedures, the deployed verification keys on the L1 verifier contract,
and the smart contract code responsible for proof verification.

  * •

_Smart contracts operating L2 functionalities on the L1 blockchain are
considered secure_ against _conventional_ vulnerabilities, such as re-entrancy
attacks [19], and are modifiable only through a well-defined upgrade process.
In other words, in this paper, we focus on what may be called logical
vulnerabilities.

  * •

_The initial state of the system_ is empty, i.e., the system has not processed
or finalized any transactions and computed any proofs. Furthermore, the
system’s initial policies and contracts are non-malicious and secure for
users, meaning that if a user can interact with the L2, the user’s funds
cannot be locked or lost before an adversarial upgrade is enforced.

Strong Adversary Model. Any of the parties mentioned above — users, operators,
and administrators — can become malicious. Users can perform DoS attacks,
operators can engage in transaction censorship, and rollup administrators can
execute malicious upgrades that could lead to the theft of all user assets.
Despite these possibilities, the saving grace is that rollup contracts
deployed on the underlying L1, together with the economic security that the L1
provides, allow us to use decentralized trust to address these issues. This
comes down to the ability to analyze [20] these rollup contracts.

For example, zkSync Era has contracts such as Verifier.sol, which process
validity proofs and can be upgraded by a multi-
sig111111https://github.com/matter-labs/era-contracts. It is critical that
this verifier can only be updated through a safe process because if it becomes
malicious, users can lose their money. Hence, users should have a sufficient
mechanism to exit the rollup in case of adversarial or questionable upgrades.
While our model is extensible, this paper largely focuses on functional
security, sidestepping DoS concerns.

###  3.2 User-centric Security Goals

In this work, our objective is to provide robust safety guarantees to L2
users, even under a strong adversarial model where the L2 network and L2
administrator can be fully compromised.

Weak liveness. A key goal is to ensure that any user transaction submitted to
the forced queue is processed as long as the L2 continues to make progress.
This guarantee is crucial to protecting users against potentially compromised
or malicious L2s or even adding L1-like censorship resistance for centralized
L2s. Moreover, our proposed design ensures that even when L2 contracts enforce
transaction blacklisting, transactions cannot be halted if they have already
been submitted to the forced queue. This mechanism is vital to maintain the
integrity and safety of ZK-Rollups. In summary, weak liveness in the context
of rollups means that either the L2 will eventually process user transactions
submitted through L1 (i.e., inheriting the liveness of the L1), or the rollup
will be frozen. In Section 4.3 we design forced queue mechanism which enforces
weak liveness.

Secure upgrades and user assets protection. In addition, we provide and
analyze designs for securely upgrading L2’s contracts. In practical terms,
this means that if there’s an undesirable upgrade, users have time to exit the
rollup. This includes mechanisms to prevent “rug pulls” (see Section 1.1 for
some examples of this) or sudden, unanticipated changes that may compromise
user assets. Ensuring that users receive sufficient notice and have effective
mechanisms to respond to changes is essential for maintaining trust and
stability within L2 environments.

##  4 Implementation in Alloy

In this section, we present the implementation details of our ZK Rollup model
using the Alloy specification language. We first give a brief technical
introduction to Alloy, followed by the Alloy model for a "strawman" ZK Rollup
and three critical mechanisms, highlighting our reasoning and essential
security properties. In Section 5, we demonstrate how to use our model to
detect issues in flawed designs. Our approach directly encourages finding
problems early, at the design stage, as opposed to later.

###  4.1 A Brief Introduction to Alloy

Alloy [15, 16] is a declarative modeling language that uses first-order
relational logic to specify and check the properties of software systems. Data
types in Alloy are represented as relations defined by _signatures_ , which
can be abstract or concrete. _Abstract signatures_ categorize general types
that are refined by more specific _concrete signatures_ , creating a flexible
and powerful type system. The language enforces the integrity of the model
through _facts_ , which are constraints that must always hold within the
model. _Functions_ and _predicates_ in Alloy are named expressions and logical
formulas, respectively; these allow the parametrization and reuse of complex
logical constructs throughout the model.

Reasoning about models in Alloy is facilitated by the _Alloy Analyzer_ , which
translates the code into a satisfiability problem. The resulting SAT instance
is then tackled using SAT solvers, which amounts to _bounded model checking_
within a specified model _scope_. Commands check and run are instrumental in
this process: check is used to verify whether a given predicate can be
invalidated, thus checking for counterexamples within the constraints of the
model, while run finds instances that satisfy all conditions of the model up
to a certain scope, allowing effective testing of various scenarios.

The Alloy analysis is always limited to a specified scope. However, the
_small-scope hypothesis_ states that a high proportion of errors can be found
by analyzing a system for all test inputs within some small scope [21].

This structured approach to modeling with Alloy ensures a rigorous
verification of properties and behaviors in software systems, making it an
invaluable tool in the development and analysis of reliable software
architectures. In the upcoming sections, we present how we used Alloy to
design and verify the correctness of critical elements of ZK-Rollup logic.

###  4.2 Strawman ZK Rollup Model

In this section, we formalize a simple ZK rollup model that notably lacks
mechanisms to process forced transactions through its L1 contract and
similarly lacks any mechanism for safely upgrading its contracts. In this
model, rollup operators and administrators may arbitrarily censor user
transactions. Furthermore, in scenarios where the L2 becomes malicious or
experiences downtime, user funds can be frozen. In subsequent sections, we
will enhance this model to include support for forced transactions and enable
safe upgrade protocols.

Data model specification. The data model of our simple ZK rollup is structured
around the following key elements:

  * •

Inputs: Represented by abstract datatypes, inputs represent transactions
submitted by end-users. This model deliberately omits additional attributes
such as sender, receiver, or transaction amounts, as these details are not
particularly relevant to our analysis.

  * •

Block: Blocks hold an ordered sequence of inputs, forming the basic building
block of our model. Although our model could be extended to include batches of
blocks, we currently limit it to blocks for simplicity.

  * •

Commitment and proof: We track two fields for both commitments and proofs:
_state_ and _diff_. The state is represented as an ordered sequence of blocks,
and the diff refers to the current block for which we commit to the L1
contract and produce a proof. It is important to note that in practice, the
diff could encompass all transaction data for the block or even a state diff.

  * •

L1: This component models the L2 rollup’s representation on the underlying L1
chain, incorporating the finalized state of blocks along using sets of
submitted commitments and proofs.

In typical rollup systems, the state could be represented by a short digest
(for example, the root of the Merkle tree), but in our model, we represent a
state by the sequence of all finalized blocks from the genesis block. The
Alloy code describes the data model as follows. Note that seq indicates an
ordered list in Alloy and one is a multiplicity which forces variable to
always be a singleton set.

⬇

1var sig Input{}

2var sig Block { var block_inputs $\colon$ seq Input }

3

4var abstract sig ZKObject {

5 var state $\colon$ seq Block,

6 var diff $\colon$ one Block

7}

8var sig Proof extends ZKObject{}{

9 not state.hasDups

10 diff not in state.elems

11}

12var sig Commitment extends ZKObject{}{

13 not state.hasDups

14 diff not in state.elems

15}

16one sig L1 {

17 var finalized_state $\colon$ seq Block,

18 var commitments $\colon$ set Commitment,

19 var proofs $\colon$ set Proof,

20}{ not finalized_state.hasDups }

Processing logic and events. The core functionalities of the L1 contract(s)
are represented by a series of actions that are essential to the operation of
the system; these actions are:

  * •

Receiving commitments: The L1 contract is responsible for receiving and
storing commitments. It ensures there is no duplication (line 2) by checking
that the commitment does not already exist within the current set of
commitments. Additionally, it maintains a sequence that extends the existing
state of the L2 (lines 3 and 4). This is achieved by verifying that the state
sequence within the commitment aligns precisely with the current finalized
state up to the last element. This check ensures that each new commitment
builds directly upon the most recent confirmed state, thereby preserving the
integrity and continuity of the blockchain’s transaction history.

⬇

1pred receive_commitment[c $\colon$ Commitment] {

2 no c & L1.commitments

3 c.state.subseq[0,sub[#L1.finalized_state,1]] $=$ L1.finalized_state

4 L1.commitments’ $=$ L1.commitments + c

5}

Alloy supports common set operators like membership (`in`), intersection
(`&`), union (`+`), etc. To refer to an expression in the next state we use
the apostrophe operator `’`. For example, `x’ = x + c` means that the value of
`x` in the next state is the union of `c` and the value of `x` in the current
state.

  * •

Receiving proofs: Similar to commitments, proofs are also received and stored
by the L1 contract. These proofs are aligned with the current state to
maintain consistency and ensure the validity of the L2 as in the case above.

  * •

Single-step rollup update: This critical functionality of the L1 contract
involves processing both commitments and proofs to securely advance the state
of L2, as outlined in the Alloy predicate rollup_process. The process begins
by confirming that both the commitment $c$ and the proof $p$ are present
within the respective sets managed by the L1 contract (lines 2–3). It then
verifies that both the commitment and the proof agree on the current state and
the proposed state transition (lines 4–6), affirming that they are intended to
advance the L2 from the same state. The predicate also ensures that the
proposed state transition, or diff, has not been previously processed (line 7,
`s.idxOf[x]` returns the first index where `x` appears in `s`). After this
check, the finalized state of the L2 is advanced to include this diff (line
8); commitment and proof sets are updated to remove processed or outdated
entries (lines 9–10), maintaining the rollup’s integrity.

⬇

1pred rollup_process[c$\colon$ Commitment, p$\colon$Proof] {

2 c in L1.commitments

3 p in L1.proofs

4 c.state $=$ p.state

5 c.diff $=$ p.diff

6 c.state $=$ L1.finalized_state

7 (no L1.finalized_state.idxOf[c.diff])

8 L1.finalized_state’ $=$ L1.finalized_state.add[p.diff]

9 L1.proofs’ $=$ L1.proofs - (p + { q $\colon$ Proof | #q.state < #L1.finalized_state })

10 L1.commitments’ $=$ L1.commitments - (c + { q $\colon$ Commitment | #q.state < #L1.finalized_state })

11}

While these are omitted for brevity, our Alloy implementation includes _frame
conditions_ to ensure that parts of the system that are not affected by a
particular operation remain unchanged.

Strawman rollup properties (SRPs). Transaction processing within the rollup is
implemented as a series of events, obeying the following rules.

$\triangleright$ SRP 1. Event Granularity: At any given time, only one event
occurs. This property ensures that the granularity of events is correct and
that we do not have overlapping events in the model of the system.

$\triangleright$ SRP 2. Monotonic State: The finalized state is guaranteed to
grow monotonically. In other words, at any given moment, the system can only
append new blocks to the finalized state, but previously finalized blocks
never change.

⬇

always (finalized_state in finalized_state’)

$\triangleright$ SRP 3. Justified State: If a block reaches the finalized
state, then once (i.e., at least at one point in the history) there was a
proof and a commitment for it that corresponded to the then-current state,
ensuring all finalized transactions are valid and verified.

⬇

1always(

2 all b $\colon$ Block | some L1.finalized_state.idxOf[b]

3 implies

4 (once some c $\colon$ Commitment, p $\colon$ Proof |

5 c in L1.commitments

6 and p in L1.proofs and

7 c.diff $=$ p.diff and b $=$ c.diff

8 and c.state $=$ L1.finalized_state)

9)

$\triangleright$ SRP 4. State Progression Validity: A commitment or proof that
is smaller than the current state is never successfully processed.

Checking. As we mentioned above, the Alloy Analyzer does bounded model
checking; the scope of checking is provided. For example, the following
command checks whether property _SRP2_ holds in the scope, which contains 10
objects of every signature and in traces up to 20 steps.

⬇

check monotonic_state for 10 but 1..20 steps

The check command tells the Alloy Analyzer to find a counterexample within the
specified scope. If the counterexample is not found, we know that the property
holds within the specified scope.

Strictly speaking when we checked the property for 20 steps it still can fail
for 21 steps. However, _small-scope hypothesis_ states that a high proportion
of errors can be found by checking a program for all test inputs within some
small scope [21].

###  4.3 Forced Queue

In the previous section, we described a strawman ZK Rollup that does not
support user transactions submitted through the L1 to force their inclusion by
the L2. This section extends the strawman model to enable that functionality,
providing users with stronger guarantees. Our goal is to ensure that forced
transactions are processed by the L2; otherwise, the L2 cannot progress (i.e.,
extend the finalized state).

Data model extensions. We introduce a new abstract signature called
ForcedEvent, and another signature called ForcedInput that extends it.
ForcedInput contains a field tx that represents a transaction submitted to the
contracts of the L2 in the L1. Additionally, in the L1 type, we add a field
called forced_queue that is an ordered sequence of ForcedEvents. The relevant
Alloy code is provided below.

⬇

1var abstract sig ForcedEvent {}

2

3var sig ForcedInput extends ForcedEvent {

4 var tx $\colon$ one Input

5}

6

7one sig L1 {

8 var forced_queue $\colon$ seq ForcedEvent

9 // + previously introduced fields

10}

Processing logic. Initially, we define the logic to add forced inputs to the
forced queue. This process simply checks that the forced input does not
already exist in the forced queue and adds the new input to the end of the
queue. The respective Alloy predicate is as follows:

⬇

1pred receive_forced[f $\colon$ ForcedEvent] {

2 no L1.forced_queue.idxOf[f]

3 L1.forced_queue’ $=$ L1.forced_queue.add[f]

4}

Next, we update the rollup_process predicate to take into account the forced
queue. If the forced queue is empty, then the rollup should process
transactions as before. If it is not empty, then every new finalized block
needs to include the head of the forced queue and can also include other
transactions from the forced queue.

⬇

1some L1.forced_queue

2 implies

3 (L1.forced_queue.first in ForcedInput

4 and some c.diff.block_inputs.idxOf[L1.forced_queue.first.tx])

Upon being finalized, elements need to be removed from the forced queue. In
Alloy, we ensure that no transactions in the current processing batch remain
in the updated forced queue (line 1). The FIFO transaction order is
maintained; transactions are moved closer to the queue’s head to expedite
processing while preserving their relative positions (line 3). This
preservation of order is crucial for fairness and for ensuring that,
eventually, all transactions are processed. We also check that the relative
positions of the elements do not change (line 8). Finally, to maintain the
integrity of the forced queue, the model prohibits adding new elements during
processing (line 12).

⬇

1no (L1.forced_queue’.elems.tx & p.diff.block_inputs.elems)

2

3all x $\colon$ ForcedInput | (x.tx not in p.diff.block_inputs.elems

4 and (some L1.forced_queue.idxOf[x]))

5 implies L1.forced_queue’.idxOf[x] < L1.forced_queue.idxOf[x]

6 and (some L1.forced_queue’.idxOf[x])

7

8all x, y $\colon$ ForcedEvent | some L1.forced_queue’.idxOf[x] and some L1.forced_queue’.idxOf[y]

9 and L1.forced_queue.idxOf[x] < L1.forced_queue.idxOf[y] implies

10 L1.forced_queue’.idxOf[x] < L1.forced_queue’.idxOf[y]

11

12all x $\colon$ ForcedEvent | x not in L1.forced_queue.elems

13 implies x not in L1.forced_queue’.elems

Forced queue properties (FQPs). We summarize the desired properties of the
forced queue below.

$\triangleright$ FQP 1. Guaranteed Processing: If the forced queue is non-
empty and a new state is finalized, then the head of the forced queue must be
processed and removed.

⬇

1always (

2 (some L1.forced_queue and some (L1.finalized_state’ - L1.finalized_state))

3 implies

4 L1.forced_queue.first.tx in new_finalized_inputs

5 and not L1.forced_queue.first.tx $=$ L1.forced_queue’.first.tx

6)

$\triangleright$ FQP 2. Forced Queue Stable: If the finalized state did not
change, then the forced queue did not decrease.

$\triangleright$ FQP 3. State Invariant: If the forced queue is non-empty and
did not change, then the finalized state remains unchanged.

$\triangleright$ FQP 4. Forced Inputs Progress: Forced inputs that were not
processed move closer to the head of the forced queue.

⬇

1always (

2 (some L1.forced_queue

3 and #L1.finalized_state < #L1.finalized_state’) implies

4 (all x $\colon$ ForcedEvent |

5 (some L1.forced_queue.idxOf[x]

6 and some L1.forced_queue’.idxOf[x])

7 implies

8 L1.forced_queue’.idxOf[x] < L1.forced_queue.idxOf[x])

9)

$\triangleright$ FQP 5. Order Preservation: Forced inputs retain their
relative order within the queue.

$\triangleright$ FQP 6. Finalization Confirmation: If an input was in the
forced queue and then disappeared from it, it was finalized.

⬇

1always (

2 all fi $\colon$ ForcedInput | fi in L1.forced_queue.elems

3 implies always(fi not in L1.forced_queue.elems implies fi.tx in
all_finalized_inputs)

4)

These properties combined result in the following guarantee that ensures that
a user’s transactions can be processed, even if the L2 operators arbitrarily
and immediately decide to censor that user.

Guaranteed Transaction Processing in the Forced Queue For any transaction $t$
in the forced queue of an L2, if the L2 progresses, then $t$ will eventually
be processed.

###  4.4 Forced Queue with Blacklisting

In recent years, transaction and address censorship has become a prominent
issue for the Ethereum ecosystem. For example, 6% of Ethereum blocks are
constructed to be OFAC-compliant [22], and Circle (USDC) maintains a list with
blacklisted addresses [23]. Some L2 networks may choose to censor transactions
to be OFAC compliant, potentially to be determined through their governance
protocol. Next, we describe an “enshrined” blacklisting mechanism; this
mechanism was meticulously designed, formalized, and checked with Alloy
Analyzer to ensure it does not violate forced queue properties.

A naive blacklisting mechanism could violate the main property of the forced
queue that a transaction in the forced queue must be processed, or it could be
abused to prevent users from exiting the L2. Our mechanism receives
blacklisting policies through the forced queue as special inputs that can be
processed only when they are at the head of the queue. Importantly, once a
blacklisting policy is processed, new transactions that do not comply with
this policy cannot be added to the forced queue. Note that if a transaction
that would otherwise be blacklisted by the policy is already in the queue
before the policy is processed, then the L2 must process it; otherwise, the
system will freeze.

Data Model Extensions. Two changes are required to support blacklisting.
First, we introduce a new signature that extends ForcedEvent called
ForcedBlacklistPolicy, which describes a set of inputs that should be
rejected. In practice, this could target anything from specific addresses to
specific transactions. Here, for simplicity, we narrow it down to a set of
Inputs. Furthermore, we include a new field blacklist in L1, which is a set of
Inputs that holds the currently active blacklisting policy.

⬇

1var sig ForcedBlacklistPolicy extends ForcedEvent {

2 var predicate $\colon$ set Input

3}

4

5one sig L1 { var blacklist $\colon$ set Input }

Processing Logic. To integrate blacklisting policies into our forced queue
mechanism, we need to make some changes to our model. Firstly, we update
receive_forced to append blacklist updates and only accept forced inputs that
are not currently blacklisted by the active or pending forced blacklist
policy.

⬇

1no L1.forced_queue.idxOf[f]

Next, we need to add a predicate to update the blacklist in the contract when
it reaches the head of the forced queue. This predicate enforces that the
blacklist is updated and the blacklist policy is removed from the queue.

⬇

1pred update_blacklist[f $\colon$ ForcedBlacklistPolicy] {

2 L1.forced_queue.first $=$ f

3 L1.blacklist’ $=$ L1.forced_queue.first.predicate

4 L1.forced_queue’ $=$ L1.forced_queue.delete[0]

5}

Finally, we update the predicate rollup_process to prevent processing
blacklisted blocks (line 1) and only allow processing inputs that are ahead of
the next blacklist policy in the forced queue (line 3). It is important to
understand that blacklisting changes the operation of the forced queue. Now,
if a new blacklisting policy was added to the forced queue, then after that,
the forced queue cannot accept inputs that are blacklisted by the queued but
not yet enforced policy. Without this extra check, Alloy tells us that we can
reach a state when the head of the forced queue is blacklisted, which
effectively means that finalized state becomes immutable.

⬇

1no (L1.blacklist & c.diff.block_inputs.elems)

2

3all x $\colon$ ForcedBlacklistPolicy, y $\colon$ ForcedInput |

4 some L1.forced_queue

5 and x in L1.forced_queue.elems

6 and y.tx in L1.forced_queue.elems.tx

7 and y.tx in c.diff.block_inputs.elems

8 implies L1.forced_queue.idxOf[y] < L1.forced_queue.idxOf[x]

Blacklisting properties.

$\triangleright$ BP 1. Non-blacklisted Finalization: If an input is finalized,
then it is not in the blacklist.

⬇

1always(

2 all x $\colon$ Input |

3 x in L1.finalized_state’.elems.block_inputs.elems

4 and x not in

5 L1.finalized_state.elems.block_inputs.elems

6 implies x not in L1.blacklist

7)

$\triangleright$ BP 2. Forced Queue Integrity under Censorship: If a censored
input is at the head of the forced queue, then the finalized state will never
change.

$\triangleright$ BP 3. Head Position Security: It never happens that head
position of the queue is blacklisted.

$\triangleright$ BP 4. Future Policy Compliance: All inputs that follow a new
blacklist policy in the forced queue are not blacklisted by it.

⬇

1always (

2 all x $\colon$ ForcedBlacklistPolicy, y $\colon$ ForcedInput |

3 x in L1.forced_queue.elems

4 and y in L1.forced_queue.elems

5 and L1.forced_queue.idxOf[x] < L1.forced_queue.idxOf[y]

6 implies y.tx not in x.predicate

7)

$\triangleright$ BP 5. Following Active Policy: If an input got forced and
there is no queued blacklisting policy, then the input is not in the
L1.blacklist.

⬇

1always (

2 all y $\colon$ ForcedInput |

3 no L1.forced_queue.elems & ForcedBlacklistPolicy

4 and y in L1.forced_queue.elems

5 implies y.tx not in L1.blacklist

6)

Given the properties outlined above, our model provides the following
guarantee for users.

Integrity of Processed Inputs under Blacklisting Mechanism For any input
processed in the L2 using a forced queue with blacklisting, the following
conditions hold: 1) Any input that is processed is not blacklisted at the time
of its processing. 2) When the input from the forced queue reaches the head of
the queue, it is not blacklisted by the active policy.

###  4.5 Forced Queue and Upgradeability

So far, we have discussed a basic model and presented mechanisms for forced
queues and safely implementing a blacklist. In this section, we formalize a
mechanism for applying upgrades to L2 contracts, noting that these upgrades
could update the verifier key, indicate changes to the ZKP circuits, and even
implement critical EIPs 121212Ethereum Protocol Improvements
(https://github.com/ethereum/EIPs) or other upgrades. Furthermore, these
upgrades could alter the mechanisms previously presented. Hence, it is crucial
that users have the opportunity to exit before an upgrade is enforced. To the
best of our knowledge, we are the first to present a complete formalization
and analysis of such a mechanism for rollups.

The upgrade mechanism operates in the following manner:

  1. 1.

First, the upgrade is announced, including all relevant details, and this
announcement is posted on L1.

  2. 2.

Following the announcement, the system collects forced inputs for a specified
duration.

  3. 3.

Once this duration elapses, meaning the timeout is reached, the rollup ceases
to accept forced events and begins processing the forced queue until it is
cleared.

  4. 4.

Once the forced queue is cleared, the upgrade is deployed, and the rollup
shifts to a new operational mode. During this timeout period, only forced
queue events are processed, which pressures the L2 operator to swiftly handle
the forced queue. Halting the acceptance of forced transactions risks the
assurance of a permissionless exit via the forced queue mechanism. It is
important to note that L2 users can still submit transactions through the L2
and receive pre-confirmations, but these cannot be finalized on the L1 until
the forced queue is cleared.

In Alloy, we cannot reason about arbitrary system upgrades, so we instantiate
the described upgradeability mechanism to update the blacklisting policy. The
resulting mechanism is not equivalent to the mechanism described in Section
4.4.

Comparison to blacklisting directly through the forced queue. In Section 4.4,
we implemented a model which guarantees that inputs that were forced prior to
the update of the blacklist policy will be finalized before the new
blacklisting policy is deployed. However, every forced input which appears in
the queue after the new blacklist policy must respect it.

In this section, we describe a mechanism that updates the blacklisting policy
through the generic upgradeability mechanism. In this case, users who observed
the upgrade announcement can force their inputs (even if blacklisted by the
pending upgrade) before the timeout. The time window between the upgrade
announcement and the timeout could be especially useful when users disagree
with the upgrade and would like to take action (e.g., quit the system) before
the upgrade is deployed. At the same time, such a mechanism gives an
opportunity to adjust to the bad actors.

In summary, both blacklisting strategies have their trade-offs. More
specifically, the blacklisting strategy through the forced queue (see Section
4.4) allows the ZK-Rollup to immediately prevent censored transactions to be
added into the forced queue (however, it cannot forbid execution of the
transactions which are already present in the queue). On the other hand
blacklisting strategy through the upgradeability mechanism allows users to
notice the upgrade and quit the ZK-Rollup within the predefined window of time
without receiving a damage.

so the designer of the system can decide which mechanism they would like to
implement in their roll-up.

Data model extensions. To support upgrades, we introduce some new types. The
first is the new abstract type UpgradeAnnouncement, and its concrete subtype
BlacklistUpdateAnnouncement, which includes a blacklist_policy. This type
represents an announcement of an upgrade, detailing the changes that will be
applied, and users can inspect it as it will be submitted to L1. We also
introduce another type, Timeout, associated with an UpgradeAnnouncement,
indicating when the upgrade waiting period expires and it is time to enforce
the upgrade.

⬇

1var abstract sig UpgradeAnnouncement {}

2

3var sig BlacklistUpdateAnnouncement extends UpgradeAnnouncement {

4 var blacklist_policy $\colon$ one ForcedBlacklistPolicy

5}

6

7var sig Timeout {

8 var upgrade $\colon$ one UpgradeAnnouncement

9}

10

11one sig L1 {

12 var ongoing_upgrade $\colon$ lone UpgradeAnnouncement

13 // + previously introduced fields

14}

Processing logic. Handling upgrades requires three new predicates and
amendments to rollup_process and receive_forced. First, upgrade_init ensures
there is no ongoing upgrade (line 2), sets the ongoing upgrade in the L1
contract (line 3), and verifies that this upgrade is not from the past (line
4).

⬇

1pred upgrade_init[f $\colon$ UpgradeAnnouncement] {

2 L1.ongoing_upgrade $=$ none

3 L1.ongoing_upgrade’ $=$ f

4 (f not in Timeout.upgrade)

5}

Next, the upgrade_timeout predicate ensures that the current timeout
corresponds to the ongoing upgrade. The upgrade_deploy predicate then enforces
the ongoing upgrade changes by applying the associated blacklist (if any) and
setting the ongoing upgrade to None, which effectively updates the contracts
and performs any modifications to the L2’s logic.

Furthermore, we update two existing predicates. Specifically, for
rollup_process, we change the logic so if an upgrade is in process, there must
be something in the forced queue to process (otherwise, L2 might delay the
finalization of the upgrade indefinitely and keep operating with a stopped
forced queue). This is enforced with the following line:

⬇

1upgrade_in_progress implies upgrade_forced_queue_processing

Similarly, in receive_forced, we enforce that if an upgrade is in progress,
new forced inputs are accepted only if the timeout for queuing has not yet
occurred.

Upgradeability Properties (UP).

$\triangleright$ UP 1. Consistency of Upgrade Announcement, Timeout, and
Enforcement: If an upgrade is deployed (policy changed), it must be preceded
by a properly announced upgrade and a timeout period. The following Alloy code
validates this sequence, confirming that any changes to the blacklist result
exclusively from an upgrade process that has been announced and timed
correctly. Specifically, the code stipulates that a change in the blacklist
(line 2) must trace back to an Upgrade Announcement (line 4-8) that specifies
the new blacklist settings. It also ensures that this change only takes effect
following a Timeout associated with the announcement (lines 9–10), which
verifies the waiting period was respected before the upgrade was enforced.

⬇

1always (

2 all is $\colon$ set Input | L1.blacklist $=$ is and

3 not L1.blacklist $=$ L1.blacklist’ implies

4 some x $\colon$ UpgradeAnnouncement | L1.ongoing_upgrade $=$ x and

5 once (L1.ongoing_upgrade $=$ none and

6 L1.ongoing_upgrade’ $=$ x and

7 L1.blacklist $=$ is and

8 (no { t $\colon$ Timeout | t.upgrade $=$ x })

9 and ((some t $\colon$ Timeout | t.upgrade $=$ x)

10 releases L1.blacklist $=$ is))

11)

$\triangleright$ UP 2. Finalization of Forced Inputs before the Upgrade: After
an upgrade, it is essential that all forced inputs are finalized to ensure
that no transactions are left pending. The Alloy code below enforces this
requirement by checking that if there is a change in the blacklist (indicative
of an upgrade), then in the past, every forced input that was in the queue
must eventually be finalized. This is achieved by ensuring that each
transaction in the forced queue, at any point before the blacklist change,
eventually becomes part of the finalized state. The code ensures that all
pending transactions are processed before any announced upgrade takes effect.

⬇

1always (

2 (not L1.blacklist $=$ L1.blacklist’) implies

3 historically (

4 all f $\colon$ ForcedInput |

5 f in L1.forced_queue.elems implies

6 eventually (f.tx in

7 L1.finalized_state.elems.block_inputs.elems

8 )

9 )

10)

$\triangleright$ UP 3. Post-Upgrade System Integrity: If the policy changes,
then no ongoing upgrade is happening (the forced queue is unlocked, and the
rollup process is unlocked).

$\triangleright$ UP 4. Consistency of Blacklisting During Upgrades: As long as
the upgrade is ongoing, the L1.blacklist does not change.

Given all of the above properties, we arrive at the following guarantee:

Upgrade Transparency and Guaranteed Action Before Upgrade Enforcement An
upgrade must begin with an announcement being published on L1 and users have a
time window to submit their inputs before the upgrade is deployed; the
mechanism also ensures that all inputs submitted to the forced queue during
the time window are finalized before the upgrade is deployed.

This mechanism ensures that users are not caught off-guard by upgrades and are
guaranteed to be able to act upon upgrade (e.g., exit from L2 rollup) before
the upgrade is enforced (if they react before the timeout).

Figure 3: Counter-example generated by Alloy, illustrating potential issues
with the naive upgradeability mechanism. In this scenario, the blacklisting
policy targets Input_1, leading to an L2 freeze because an input in the
forced_queue cannot be processed. This occurs because the mechanism does not
require processing all transactions from the forced queue prior to executing
an upgrade. Note that despite an extended timeout period, adversarial users
could still flood the forced queue with transactions, potentially leaving
legitimate user transactions unprocessed before the upgrade occurs.

##  5 Design-time Testing with Alloy Models

Building on the implementation details and security properties described in
the previous section, we explore how our Alloy models can be used for design-
time testing of ZK-Rollups. We provide an infeasibility result and highlight a
vulnerability in state-of-the-art upgradeability mechanisms.

Scenario testing. To validate our models, we implement several scenarios that
test their functionality under various conditions, such as handling
simultaneous commitments and proofs, processing in different sequences, and
ensuring that commitments for an outdated state are not processed. These
scenarios help demonstrate the model’s capabilities and expose potential
vulnerabilities. Also, it helps to detect incorrect specifications, e.g.:

⬇

1run {

2 eventually(

3 some x $\colon$ Input |

4 x in L1.blacklist

5 and (x not in all_finalized_inputs)

6 and eventually (x in all_finalized_inputs))

7} for 7

In this scenario for the rollup with upgradeability and blacklisting (Section
4.5), we start with an empty blacklist state and no queued commitments or
proofs. We assert that, eventually, we would like to reach a state where there
is an input `x` which is blacklisted but not finalized. After that we would
like to eventually reach a state when the input `x` is finalized. This
scenario is only possible if the rollup updates its blacklists two times where
the first update blacklists `x` and the second update removes `x` from the
blacklist and at the end `x` gets finalized. When we execute the run command,
the Alloy Analyzer looks for models with up to seven instances of each
signature which would satisfy the predicate. The Alloy Analyzer finds a
satisfying instance that consists of a trace of length eight.

Infeasibility of on-the-spot blacklisting. When processing a blacklisting
policy update transaction (Section 2), transactions that precede it in the
queue must be processed. This means that otherwise censored transactions would
have to be processed. If blacklisting is applied immediately, it can generate
a trace that gets the system stuck, breaking the guarantees of our system. To
maintain the integrity of the forced queue, blacklisting should be enforced
either through the forced queue (Section 4.4) or upgradeability mechanism
(Section 4.5), ensuring correct operation of the forced queue. Moreover, the
described upgradeability mechanism also ensures that all users have a fair
chance to process their transactions before new policies take effect. Notably,
if we allow the query that updates the blacklisting policy “on-the-spot”, then
Alloy immediately generates simple counterexamples to most of the properties
mentioned above. Most importantly, due to the non-deterministic order of the
actions in the system, “on-the-spot” updates can always lead to a situation
where forced queue inputs get blacklisted, which makes the system stuck (i.e.,
no more blocks could be finalized).

Potential vulnerability in state-of-the-art upgradeability policy. The current
state-of-the-art, often described as the safest approach, typically includes
one week before enforcing an
upgrade.131313https://medium.com/l2beat/introducing-stages-a-framework-to-
evaluate-rollups-maturity-d290bb22befe Upgrades based solely on time can lead
to situations where users who wish to exit the L2 before the upgrade are
locked in because their transactions cannot be processed promptly. However,
our solution (Section 4.5) mitigates this issue by ensuring that all
transactions in the forced queue are processed before the upgrade takes
effect, thus maintaining users’ safety in case of malicious upgrades. Here, we
discuss the potential pitfalls of relying solely on a timeout period for
upgrades and then provide a counterexample demonstrating the issues with that
mechanism, as produced by the Alloy Analyzer.

There could be two issues arising from merely enforcing the upgrade after a
set period of time. For the first example, consider the case where we are
using a forced queue and upgradeability as described in Section 4.5. However,
we deploy the upgrade based solely on the timeout (i.e., not taking care of
locking and emptying the forced queue before deploying the upgrade). Figure 3
demonstrates the issue that might arise in that case produced by Alloy.
Specifically, what happens is that first, we start with an empty forced queue,
and then a user adds an input to the queue (Input_1). Next, an announcement
occurs, and then the timeout of that announcement is reached. This enforces
the upgrade, updating the blacklist to include Input_1. The result is that L2
becomes frozen because the head (Input_1) of the queue is blacklisted. Another
problem could occur if the upgrade involves changing the functionality of the
rollup and a user might submit a transaction to be forced before the upgrade
because they disagree with the change and want to exit before the upgrade.
However, because other transactions are in front of it (whether benignly or
maliciously added), their transaction will not be processed. Additionally, the
L2 might censor the user’s transactions, preventing the user from exiting
before the upgrade.

These examples demonstrate severe issues with existing mechanisms. Our model
presented in Section 4 is immune to the described attacks.

##  6 Discussion

Why now. The L2Beat Risk page indicates that the most widely used optimistic
rollups already support mechanisms like the Forced Queue, referred to as
“Sequencer failure” on L2Beat. Additionally, as we demonstrated in Section
4.5, the state-of-the-art upgradeability mechanisms can be exploited by
malicious actors. Most rollups struggle to design an upgradeability mechanism
that is both secure and compatible with other mechanisms. Our work provides a
framework to help design and evaluate such mechanisms, along with a secure
design. This is crucial because for rollups to truly inherit the security and
censorship resistance of the L1 they are based on, they need secure
implementation of the mechanisms discussed in Section 4. We hope that our work
will encourage L2Beat to integrate our security properties into their website,
as it is the de facto source of truth for informing users about the risks of
rollups. Additionally, we have collaborated closely with the Matter Labs team
to help them design secure, verified mechanisms for contracts operating the
zkSync Era rollup.

How we can use Alloy models. Alloy models can provide high-level specification
and guidance for the low-level implementation of the described protocols.
Another promising direction is generating tests from Alloy models to identify
corner cases [24] and validate Solidity contracts against these scenarios. It
is worth mentioning that related tools like TLA+ [25] and Quint [26] offer
closer connections to code and facilitate code extraction.

For more detailed examples and potential extensions of our model, refer to
Appendix B.

Mechanism | Lines of | No. of | Solve time
---|---|---|---
code | Clauses | (sec)
Simple | 295 | 1,203,661 | 9.099
Forced Queue | 529 | 1,996,273 | 136.104
Blacklist | 721 | 2,200,981 | 399.724
Upgradeability | 970 | 2,468,911 | 388.620

Figure 4: Various statistics for each rollup mechanism. The last column
indicating the solving time uses a scope of 5. Figure 5: Log-scale graph of
analysis time for increasing scopes for our most complex model, i.e. the model
for upgradeability.

##  7 Measurements

In this paper, we use Alloy Analyze 6 to verify the invariants and assertions
of various L2 mechanisms. This involved adapting our model for each ZK Rollup
mechanism and then systematically testing them within the Alloy environment.
The scope for our tests was set up to allow us to specify more fine-grained
bounds on each type but does not imply any limitation on the overall number of
system states that can be explored. All experiments were performed on an Intel
Core i7-9750H CPU with 16 GB of RAM.

For each case, we quantified the number of new lines of Alloy code written,
the total number of clauses generated by the analyzer, and the time to solve
these clauses using an SAT solver. Figure 4 shows that the complexity and the
time required to solve the clauses increase with more complex rollup
mechanisms. Figure 5 depicts the running time for different scope values for
our most complex model, demonstrating a significant increase in the SAT solver
time as the scope increases. The observed exponential growth is typical of
SAT-based analyses.

##  8 Related Work

Formal Methods for Web Security. Our work is inspired by the seminal work of
Akhawe et al. [17] on applying formal modeling to analyze the security of web
mechanisms and applications. Specifically, this work provides a formal model
of the web platform to dissect the security of various web mechanism designs
using Alloy. Their analysis included the specification of threat models
tailored for evaluating the security of web platforms. Analogously, we crafted
our analysis around the strongest conceivable adversary (i.e., a malicious
L2), examining rollup designs under this threat model. Moreover, Akhawe et al.
[17] established a set of broadly applicable security goals and analyzed
various security properties for web applications. Similarly, we defined
fundamental security goals tailored for rollup users, defined security
properties, and systematically evaluated different scenarios using Alloy. For
those interested in formal methods for security, the recent survey by Kulik et
al. [27] offers a detailed examination of formal methods accessible to
designers of security-critical systems.

Formal methods in blockchain and ZKPs. There is a growing body of work on
verifying different aspects of blockchain, from smart contacts to consensus
algorithms and ZK proof generation. We mention only some relevant work here.
For smart contract verification, existing research endeavors primarily aim to
either demonstrate the absence of common vulnerabilities or rely on user-
defined specifications to verify correctness. Notable surveys by Murray and
Anisi [28] and Garfatta et al. [29] offer comprehensive overviews of formal
verification methods tailored for Solidity smart contracts. However, it is
important to note that our work diverges from this trajectory, focusing
instead on providing assurances regarding the design of mechanisms implemented
in smart contracts that operate rollups.

On the front of formal verification for Byzantine fault tolerance (BFT) in
blockchain systems, seminal works by Tholoniat and Gramoli [30] and Yoo et al.
[31] have contributed significantly. Regarding ZKPs, recent efforts have
explored the verification of verifiers for ZK-rollups [20]. Additionally,
several initiatives have focused on formally proving the absence of common
bugs in ZK circuits [18]. In contrast to those efforts, we focus on the design
of mechanisms that are complementary to ZKPs.

Rollup Security. Prior works have focused on qualitatively analyzing
optimistic and ZK-Rollups. Gorzny et al. [32] established a wishlist of
properties that an escape hatch mechanism (also known as a forced queue)
should possess to be considered trustworthy. Their paper focuses on
qualitative characteristics that escape hatches should exhibit, such as
executing arbitrary transactions, being supported by default in a rollup, and
efficiency. In contrast, our paper formally defines the security properties of
escape hatches and analyzes various scenarios using Alloy.

In their recent work, Koegl et al. [33] presented nine main attack threats for
rollups, briefly describing potential attacks in both optimistic and ZK-
Rollups, such as censorship attacks, DoS attacks, and client vulnerability
risks. Our work extends some of these potential attacks by formally modeling
ZK-Rollups, presenting a clear and strong adversary, and outlining the
security properties necessary to ensure a secure ZK Rollup design.

Finally, complementing our work, Gorzny and Derka [34] presented a framework
to qualitatively evaluate existing rollups based on different dimensions:
familiarity, finality time, modularity, and maturity. In comparison to the
aforementioned works, we are the first to formally specify the main properties
of ZK-Rollups and analyze various designs using Alloy to provide formal
guarantees of the security of specific ZK rollup designs.

##  9 Conclusion

Rollups are heralded as the foremost solution to blockchain scalability,
collectively securing over $40 billion in value. However, recent incidents
have led to censorship and halting block production on rollups. Despite these
astronomical monetary amounts, the security properties of rollups remain
inadequately understood.

Our work introduces an extensible formal model for ZK-Rollups that facilitates
not only the design and evaluation of rollups’ critical mechanisms but also
enhances the practical understanding of their security properties. Using
Alloy, a language that has been used for modeling complex systems for more
than a decade, we create models that are accessible to developers, security
auditors, and researchers alike, enabling automatic reasoning with rapid
results. By making our models public, we encourage their use for evaluating
concrete implementations. Finally, the comprehensive security properties
described in our work could be showcased on platforms dedicated to rollup
security, like L2Beat. This would give developers and users a clear and
tangible understanding of the security assurances each rollup provides. Our
primary objective is to lay the foundation for the creation and advancement of
secure L2 solutions that are not only informally recognized but also
verifiably proven.

## Acknowledgements

We thank Franck Cassez, Bartek Kiepuszewski, Piotr Szlachciak, Anton Astafiev,
Marco Stronati, Antonio Locascio, Kalman Lajko, and Matej Pavlovic for their
insightful feedback.

## References

  * [1] S. Nakamoto, “Bitcoin: A peer-to-peer electronic cash system,” 2008.
  * [2] G. Wood _et al._ , “Ethereum: A secure decentralised generalised transaction ledger,” _Ethereum project yellow paper_ , vol. 151, no. 2014, 2014.
  * [3] Q. Zhou, H. Huang, Z. Zheng, and J. Bian, “Solutions to scalability of blockchain: A survey,” _Ieee Access_ , 2020.
  * [4] A. Yakovenko, “Solana: A new architecture for a high performance blockchain v0. 8.13,” _Whitepaper_ , 2018.
  * [5] S. Blackshear, A. Chursin, G. Danezis, A. Kichidis, L. Kokoris-Kogias, X. Li, M. Logan, A. Menon, T. Nowacki, A. Sonnino _et al._ , “Sui Lutris: A blockchain combining broadcast and consensus,” _arXiv preprint arXiv:2310.18042_ , 2023.
  * [6] L. T. Thibault, T. Sarry, and A. S. Hafid, “Blockchain scaling using rollups: A comprehensive survey,” _IEEE Access_ , vol. 10, 2022.
  * [7] Barry Whitehat, “Roll up token,” https://github.com/barryWhiteHat/roll_up_token, 2018, accessed: 2024-03-19.
  * [8] S. Goldwasser, S. Micali, and C. Rackoff, “The knowledge complexity of interactive proof-systems,” in _Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing_ , ser. STOC. Association for Computing Machinery, 1985.
  * [9] H. Kalodner, S. Goldfeder, X. Chen, S. M. Weinberg, and E. W. Felten, “Arbitrum: Scalable, private smart contracts,” in _USENIX Security Symposium_ , 2018.
  * [10] D. Sun, W. Ma, L. Nie, and Y. Liu, “Sok: Comprehensive analysis of rug pull causes, datasets, and detection tools in defi,” _arXiv preprint arXiv:2403.16082_ , 2024.
  * [11] G. D. Monte, D. Pennino, and M. Pizzonia, “Scaling blockchains without giving up decentralization and security: A solution to the blockchain scalability trilemma,” in _Proceedings of the Workshop on Cryptocurrencies and Blockchains for Distributed Systems_ , 2020.
  * [12] G. Wang, Z. J. Shi, M. Nixon, and S. Han, “SoK: Sharding on blockchain,” in _Proceedings of the 1st ACM Conference on Advances in Financial Technologies_ , 2019.
  * [13] B. Lashkari and P. Musilek, “A comprehensive review of blockchain consensus mechanisms,” _IEEE access_ , vol. 9, 2021.
  * [14] S. Motepalli, L. Freitas, and B. Livshits, “SoK: Decentralized sequencers for rollups,” _arXiv preprint arXiv:2310.03616_ , 2023.
  * [15] D. Jackson, “Alloy: a lightweight object modelling notation,” _Transactions on software engineering and methodology (TOSEM)_ , vol. 11, no. 2, 2002.
  * [16] ——, _Software Abstractions: logic, language, and analysis_. MIT press, 2012.
  * [17] D. Akhawe, A. Barth, P. E. Lam, J. Mitchell, and D. Song, “Towards a formal foundation of web security,” in _IEEE Computer Security Foundations Symposium_. IEEE, 2010.
  * [18] S. Chaliasos, J. Ernstberger, D. Theodore, D. Wong, M. Jahanara, and B. Livshits, “Sok: What don’t we know? understanding security vulnerabilities in snarks,” _arXiv preprint arXiv:2402.15293_ , 2024.
  * [19] S. Chaliasos, M. A. Charalambous, L. Zhou, R. Galanopoulou, A. Gervais, D. Mitropoulos, and B. Livshits, “Smart contract and DeFi security tools: Do they meet the needs of practitioners?” in _Proceedings of the International Conference on Software Engineering_ , 2024.
  * [20] D. Firsov and B. Livshits, “The ouroboros of zk: Why verifying the verifier unlocks longer-term zk innovation,” Cryptology ePrint Archive, Paper 2024/768, 2024, https://eprint.iacr.org/2024/768. [Online]. Available: https://eprint.iacr.org/2024/768
  * [21] D. Jackson and C. A. Damon, “Elements of style: Analyzing a software design feature with a counterexample detector,” _ACM SIGSOFT Software Engineering Notes_ , vol. 21, no. 3, pp. 239–249, 1996.
  * [22] A. Wahrstätter, J. Ernstberger, A. Yaish, L. Zhou, K. Qin, T. Tsuchiya, S. Steinhorst, D. Svetinovic, N. Christin, M. Barczentewicz _et al._ , “Blockchain censorship,” in _Proceedings of the ACM on Web Conference_ , 2024.
  * [23] Z. Wang, X. Xiong, and W. J. Knottenbelt, “Blockchain transaction censorship: (in) secure and (in)efficient?” in _The International Conference on Mathematical Research for Blockchain Economy_. Springer, 2023.
  * [24] S. A. Khalek, G. Yang, L. Zhang, D. Marinov, and S. Khurshid, “Testera: A tool for testing java programs using alloy specifications,” in _2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)_. IEEE, 2011, pp. 608–611.
  * [25] L. Lamport, “Specifying systems: the tla+ language and tools for hardware and software engineers,” 2002.
  * [26] I. Systems, “Quint: A new specification language for writing and reasoning about distributed systems,” https://github.com/informalsystems/quint, 2024, accessed: 2024-06-05.
  * [27] T. Kulik, B. Dongol, P. G. Larsen, H. D. Macedo, S. Schneider, P. W. Tran-Jørgensen, and J. Woodcock, “A survey of practical formal methods for security,” _Formal aspects of computing_ , vol. 34, no. 1, 2022.
  * [28] Y. Murray and D. A. Anisi, “Survey of formal verification methods for smart contracts on blockchain,” in _2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS)_. IEEE, 2019, pp. 1–6.
  * [29] I. Garfatta, K. Klai, W. Gaaloul, and M. Graiet, “A survey on formal verification for solidity smart contracts,” in _Proceedings of the 2021 Australasian Computer Science Week Multiconference_ , 2021, pp. 1–10.
  * [30] P. Tholoniat and V. Gramoli, “Formal verification of blockchain byzantine fault tolerance,” in _Handbook on Blockchain_. Springer, 2022, pp. 389–412.
  * [31] J. Yoo, Y. Jung, D. Shin, M. Bae, and E. Jee, “Formal modeling and verification of a federated byzantine agreement algorithm for blockchain platforms,” in _2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE)_. IEEE, 2019, pp. 11–21.
  * [32] J. Gorzny, L. Po-An, and M. Derka, “Ideal properties of rollup escape hatches,” in _Proceedings of the International Workshop on Distributed Infrastructure for the Common Good_ , 2022.
  * [33] A. Koegl, Z. Meghji, D. Pellegrino, J. Gorzny, and M. Derka, “Attacks on rollups,” in _Proceedings of the International Workshop on Distributed Infrastructure for the Common Good_ , 2023.
  * [34] J. Gorzny and M. Derka, “A rollup comparison framework,” _arXiv preprint arXiv:2404.16150_ , 2024.
  * [35] K. Fichter, “Why is the optimistic rollup challenge period 7 days?” https://kelvinfichter.com/pages/thoughts/challenge-periods/.
  * [36] Zeeve, https://paragraph.xyz/@zeeve/a-holistic-view-of-solutions-to-reduce-7-day-finality-in-op-rollups.

##  Appendix A Alloy Metamodel for the Forced Queue and Upgradeability Model

Figure 6 illustrates the metamodel used for formalizing the forced queue and
upgradeability model in Alloy. The metamodel depicts various components and
their connections within the system.

Figure 6: The metamodel of our formalization of the forced queue and
upgradeability in Alloy.

##  Appendix B Model Extensions

In this section, we propose some potential extensions that can be built on top
of our model and could further enhance the state of ZK-Rollups, by making our
model more practical, modeling more functionalities, and capturing different
implementation details.

Enforcing Processing from the Forced Queue in Intervals. While our model
requires that every new block processed must include a transaction from the
forced queue if it is not empty, this might be overly strict for practical
implementations due to the asynchronous nature of blockchain systems. A more
practical approach would be to enforce the processing of the head of the
forced queue every 3–5 blocks being finalized. This adjustment still offers
the same guarantees to users regarding eventual processing, but allows for
greater flexibility and efficiency in the system’s operation.

Modeling Optimistic Rollups. Optimistic rollups, which rely on fraud proofs
handled by the L1 for dispute resolution, present a more complex scenario than
our current model. Extending our model to include optimistic rollups would
involve formalizing the fraud proof mechanism.

Analyzing Withdrawal Windows in Optimistic Rollups. Optimistic rollups that
have been deployed generally employ a seven-day withdrawal period. Although
numerous reasons exist for the necessity of this duration [35], newer methods
propose shortening these periods. Nevertheless, the potential security
compromises of these more assertive suggestions [36] still require thorough
examination.

Consideration of State Diffs vs. Transaction Inputs. To capture more granular
changes within blocks, our model could be extended to differentiate between
state diffs and complete transaction inputs. This would allow for a more
detailed understanding of the state transitions within the rollups, aligning
more closely with how changes are batched and processed in practical
implementations. Nevertheless, this should not change the properties described
in our model.

Introducing Data Availability and Expiration. Incorporating data availability
and expiration into our model could significantly enhance its utility. This
involves modeling how data is made available and the potential expiration or
deletion of data, which is critical for maintaining the integrity and
accessibility of the rollup data over time.

Associating Finalized States with Hashes Instead of Actual Blocks. To address
the potential disappearance of data (data availability issues), our model
could be extended to associate finalized states with hashes rather than actual
block contents. This approach would ensure that the system can still verify
the integrity of the data even if the actual data is no longer directly
accessible.

Detailed Modeling of L1 Blocks and Finality. The model could be extended to
include detailed modeling of L1 blocks and their
finality,141414https://ethereum.org/en/roadmap/single-slot-finality/ capturing
how Ethereum’s finality mechanisms, impact L2 operations. Formalizing how L1
reorgs affect L2s would provide critical insights into how to design L2
systems to handle these events safely.

Modeling L2 Operations Beyond Smart Contracts. Expanding our model to include
specifications of L2 operations and components beyond just the smart contracts
on L1 could provide a foundation for designing L2 sequencers and other
critical infrastructure, such as the interactions between L2 sequencers and
provers. This would build upon the provided L1 model, offering a comprehensive
framework for the architectural design of L2 rollups.

In this work, we provide the fundamental missing formalization and implement
it in Alloy to provide guarantees about its correctness. We believe that this
base could be used as a framework to analyze the design of critical mechanisms
of L2 rollups.