2024-12-11 Neutron Dex Model

Security Audit Report

Neutron Dex Model

Authors: Manuel Bravo, Ivan Gavran, Gabriela Moreira

Table of Contents Project Overview ......................................................................................................... 1

Input......................................................................................................................... 2
The Quint Model ...................................................................................................... 3 State 3
Properties of Interest .............................................................................................. 6 State Properties 6 Transition Properties 7
Analysis Results ....................................................................................................... 8 Violated Properties 8 Model Simulation: Size of the Input Space 9 Model Simulation: Shrinking the State Space 10
Conclusion ............................................................................................................. 12 Disclaimer.................................................................................................................. 13 © 2024 Informal Systems Neutron Dex Model

Project Overview In Q4 of 2024, as a part of security partnership with Neutron, Informal Systems set out to write a formal model of Neutron’s Dex in Quint. Working closely with the Dex’s development team, we captured the most important aspects of the Dex, defined the desired properties, and analyzed their validity. While our analysis did uncover some violations of the desired properties, further investigation showed that they do not constitute a security threat to the Dex. In this report we give the basics of the model and we detail the analysis results. The full model will be open-sourced in the near future.

Input As a starting point to building the model, we used the following material: • Public documentation of the Dex module, corresponding to the commit bfb0c31 of the docs repository • System specification, written by the dev team specially for this modelling effort, in which the basic behavior and expected properties of the system are described. This document is dynamic and was developed simultaneously with modelling.

• The implementation of the dex, at commit 01b71f7 and, in the second phase, at release v5.0.0-rc0. While our explicit goal was to avoid relying too much on the implementation details, sometimes it was necessary in order to understand e.g, the rounding of rationals, which was influencing whether the behavior was correct or erroneous.

Input 2 © 2024 Informal Systems Neutron Dex Model
The Quint Model Each Quint model is conceptually a state machine whose evolution is defined by its initial state and the set of transitions from a current to the next state. In this model, we opted for having a single variable called state, that captures all the relevant aspects of the system. Let us first see how the state of the system looks like:

State

type State = { tranches: TrancheKey -> Tranche, tranchesShares: TrancheShares, pools: PoolId -> Pool, poolShares: PoolShares, // balances of all the users in the system coins: Coins, blockNumber: BlockTime, // helper state variables, to be used in invariants bookkeeping: TrackedValue }

Fields tranches and tranchesShares contain the information on the state of the tranches and users' ownership in them. The same for pools is achieved by pools and poolShares . The field coins keeps track of the state of users' funds, and blockNumber tracks the blocks. Finally, bookkeeping contains helper variables, that will be used for inspecting desired properties (e.g., total value deposited by a user).

Each field has a type. As an example, pools is a mapping from PoolId into Pool type, which are defined by

type PoolId = { tokenPair: (Token, Token), // Pool's tick is the token0 sell tick, that is: 1 Token0 = price(tick)* 1 Token1 tick: TickIndex, fee: Fee }

type Pool = { reserves: (int, int), shares: int }

Each pool contains the information about its reserves (a pair of two integers) and total existing shares (an integer). Check the other types in types.qnt.

Model Evolution: Initial State The initial state is very simple, with nothing in pools or tranches, and with some coins amount assigned to each user:

The Quint Model 3 © 2024 Informal Systems Neutron Dex Model

pure val initState: State = { tranches: Map(), coins: tuples(CREATORS, TOKENS).mapBy(_ => INITIAL_CREATOR_BALANCE), tranchesShares: Map(), blockNumber: 0, poolShares: Map(), pools: Map(), bookkeeping: emptyTrackedValue }

action init = { state' = initState, }

Model Evolution: Transition Possible transitions are defined by the action predicate step :

action step: bool = any { placeLimitOrderAct, cancelLimitOrderAct, withdrawLimitOrderAct, withdrawPoolAct, depositAct, singlehopSwapAct, advanceTimeAct, }

In short, any of the seven listed things may happen: a user can place a new limit order, or withdraw or cancel from an existing one; a user can deposit into a pool or withdraw from an existing one; a user can swap using available liquidity; or a time may progress.

As an illustration, let's look at the withdrawPoolAction (called directly by withdrawPoolAct ):

action withdrawPoolAction(processResult: (Result, Message) => bool): bool = all {

// a cross-product of creators and pools in which they have >0 share val relevantCreatorsAndPools = tuples(CREATORS, state.pools.keys()).filter(((c, p)) => state.poolShares.get(c).getOrElse(p, 0) > 0) all { require(relevantCreatorsAndPools != Set()),

nondet creatorAndPool = relevantCreatorsAndPools.oneOf() val creator = creatorAndPool._1 val poolKey = creatorAndPool._2 nondet withdrawAll = oneOf(Set(true, false)) val userShares = state.poolShares.get(creator).get(poolKey) nondet partialWithdrawAmount = oneOf(1.to(userShares)) val amountToWithdraw = if (withdrawAll) userShares else partialWithdrawAmount val msg = { creator: creator,

The Quint Model 4 © 2024 Informal Systems Neutron Dex Model

tokenPair: poolKey.tokenPair, sharesAmount: amountToWithdraw, tick: poolKey.tick, fee: poolKey.fee } val result = withdrawPool(state, msg) state' = res.state } }

The action non-deterministically defines which exact message should be sent. Let's examine it part-by-part.

The line require(relevantCreatorsAndPools != Set()) requires that there are some users with non- zero shares in pools, from which they could withdraw. If there are none, this action may not be executed (and is removed from a set of actions to choose from in the step ).

The creatorAndPool is a non-deterministic ( nondet ) value obtained by choosing oneOf the elements from those users and corresponding pools.

The nondet variable withdrawAll is a slight optimization: we want to bias the action to occasionally withdraw all the shares (as we privilege this choice over choices with all possible share values). Thus, if withdrawAll is true, we will withdraw all existing shares, and otherwise a nondet value partialWithdrawAmount .

The message msg is formed with all the choices, and executed on the current state . Finally, the state variable is updated with the result of the execution. ( state' means "the variable state after the transition".)

Transitions Business Logic While the action defines the choices on what to execute, the whole business logic is contained in the function withdrawPool (and similar), which can be found in dex.qnt.

They all share the same signature, transforming the pair (State, Message) into (the next) State . In that regard, all these functions are pure: there is no non-determinism and no accessing the state variable: all of this is done in the transition actions described above.

Modeling Choices and Simplifications In the model, we made the following simplifying choices:

We did not model a multi-hop swap. Instead, we achieve it by consecutive applications of a single-hop swap.
We did not add the feature of the user limiting the maximum amount to receive from the placed limit order message. This is a nice UX feature, but is not security-critical.
In the model, users always specify price ticks instead of direct prices (this choice has to do with technical limitations of Quint, the lack of the logarithm function).
The Quint Model 5 © 2024 Informal Systems Neutron Dex Model
Properties of Interest In this section we describe properties we encoded in the model and checked their validity. They can be divided into state properties (expressed through predicates on a single state) and transition properties (expressed through predicates on two subsequent states).

State Properties

[DEPOSIT-PROFITS] For a user who has deposited to the pool p and who has withdrawn all their shares from p , the following holds:

• If there were swaps through p , the user has withdrawn more value than deposited

• If there were no swaps through p , the user has withdrawn the same value as deposited

• The user withdrew no less value than deposited. Note: In case the autoswap fee needed to be paid, the initial deposited value is considered the one after subtracting the deposit fee.

The Quint encoding of the property can be seen in baseDexEvolution.qnt::poolProfitInv and looks like this:

val poolProfitInv: bool = state.bookkeeping.pools.deposits.keys().forall(((creator, poolId)) => // If the user has withdrawn all their shares state.poolShares.get(creator).get(poolId) == 0 implies val totalDeposited = state.bookkeeping.pools.depositValues.getOrElse((creator, poolId), 0) val withdrawn = state.bookkeeping.pools.withdrawals.getOrElse((creator, poolId), (0, 0)) val swaps = state.bookkeeping.pools.swaps.getOrElse((creator, poolId), Set()) val totalWithdrawn = computeDepositValue(withdrawn, poolId.tick).truncate() val tol = TOLERANCE * computeUnitTolerance(poolId.tick) // If there were swaps, the user withdrew more value than deposited if (swaps != Set()) totalWithdrawn + tol >= totalDeposited // Otherwise, the user withdrew no less value than deposited else abs(totalWithdrawn - totalDeposited) <= tol )

This predicate requires that forall deposits, in case the user has withdraws all their shares, it implies a relation between totalWithdrawn and totalDeposited , depending on whether or not there were swaps.

[NO-LOSS-ON-PLACED-TRANCHE] A user who has placed a limit order (the remaining maker part, post-swap) cannot lose value with respect to the specified sellingPrice .

Once the user has withdrawn all their shares, be it through a (sequence of) withdrawal or a cancellation-induced withdrawal, the user is at no loss (with respect to the price set by sellTick specified by the user). See the predicate at baseDexEvolution.qnt::noLossOnExhaustedTranches .

Properties of Interest 6 © 2024 Informal Systems Neutron Dex Model

We also checked for a sequence of other properties that can be viewed as sanity checks, whose violation would imply that there are potential problems to explore: 3. [RESERVES-IMPLY-SHARES] If a pool has some positive amount of reserves, it also has a positive amount of shares. 4. [COINS-CONSTANT] The total amount of coins in the system (tranches, pools, users' coins) is invariant. 5. [NONEGATIVE-AMOUNTS] All amounts of pool shares and reserves, tranches shares and reserves, and user coins are non-negative.

Transition Properties Transition properties describe the relation between a state before and a state after a transition happened, and their signature is (State, Message, State): bool .

All transitions are inspected for the state changes as described in the specification. Furthermore, there are specific properties to be expected after transitions.

[SWAP-TRANSITION] When a user swaps using a SinglehopSwapMsg message:

• Their limit price is honored. • The value of existing pools either increases corresponding to the fee, or remains the same (if the pool did not take part in the swap). • The value of all tranches remains the same.

[LIMIT-ORDER-TRANSITION] When a user swaps using a PlaceLimitOrderMsg message:

• Their limit price is honored. • The value of existing pools either increases or remains the same. • The value of all tranches remains the same, except for the tranches corresponding to the tick, which may increase in value due to the maker part of the limit order message. 9. [DEPOSIT-TRANSITION] When a user deposits to a pool: • The value of existing pools either increases (for the pool to which the user deposits) or remains the same. • If the deposit is provided in a different ratio than the existing ratio of the pool, a fee for the swap (to reach the existing ratio) is paid. • [POOL-RATIO-CONSTANT] If the autoswap option is set to false, the ratio in the pool does not change when performing (non-initial) deposits. • [SHARES-FOR-DEPOSITS] If a user successfully deposits positive amount of coins (at least one in the pair), they will get in return a positive amount of shares. 10. [CANCEL-TRANSITION] When a user cancels a tranche: • No shares of other users are affected. • The user received the pro-rata shares of any unused maker denom and of all the swap proceeds. 11. [TRANCHE-WITHDRAW-TRANSITION] When a user withdraws from a tranche: • The user gets the pro-rata portion of all the swap proceeds not yet claimed (since the last withdrawal) 12. [POOL-WITHDRAW-TRANSITION] When a user withdraws from a pool: • The user gets the specified portion of the value they provided, increased by their part of the profits from all the swaps occurring since the last withdrawal.

Analysis Results After developing the model, we have used it to analyze the properties of the system. Any violation to the property from the model called for closer inspection. Some violations pointed to discrepancies between the model and the input, some to discrepancies between the model&input and the implementation, and some to actual violations of the properties in the implementation.

Violated Properties Below, we list the properties for which the simulation found violations and discuss the relevant context and consequences.

[DEPOSIT-PROFITS]: The reason for why this property was violated has to do with rounding when withdrawing. Repeated rounding may make it happen so that the loss grows with the number of steps (transactions).

An example run is given in violationRuns.qnt::noLossViolationRoundingRun .

Note that here we are talking about differences in dozens of micro-tokens. Thus, this violation is considered acceptable by the dev team. In order to disregard rounding errors, we have phrased a similar property that included tolerance for rounding errors: 1.a [NO-LOSS-TOLERANCE] Assuming that we allow for the tolerance proportional to the number of swaps and the value of a pair of unit tokens (to counter off-by-one errors), the user withdraws no less value from the pool than deposited. However, even this property does not hold. The problem occurs when the total value of reserves becomes much larger than the total number of shares. When withdrawing all their shares from the pool, the user receives userShares * (totalPoolValue / totalPoolShares) . Assuming an off-by-one error in userShares , the max possible error is 0.99 * (totalPoolValue / totalPoolShares) .

One way in which totalPoolValue and totalPoolShares can substantially diverge in a few steps is the following:

a. Bob deposits (smallAmount, 0) in the pool with a very large fee.

b. Alice deposits (0, largeAmount) with (default) autoswap enabled to the same pool.

This translates into calculating shares as if Alice has first converted the whole largeAmount . Thus, Alice receives very few shares, and the total amount of shares is much smaller than the pool value (because the majority of the value is provided by the autoswap fee). c. Alice withdraws all of her shares, and receives a much smaller value than what she deposited (accounting for the fee paid for the swap). d. Bob withdraws all of his shares, and receives, beside his deposited part and the Alice's fee paid, also the rest of Alice's funds.

An example run is given in violationRuns.qnt::noLossViolationAutoswapRun .

A potential attack is a user front-running any extremely large deposit (bigger than the pool's size) by changing the pool's ratio so as to be able to take advantage of the described behavior. Alternatively, and much more lucrative, is a user front-running any initial deposit to a new pool. NOTE: This particular violation seems to be stemming from the assumption that every pool's value will be significantly larger than the deposit value. Indeed, the calculation for the autoswap fee starts with the goal of

bringing deposit amounts to match the ratio of the pool, where sometimes it would be easier to do it the other way round. Discussing this issue with the dev team, they informed us they were aware of the issue and were planning to address it by runtime monitoring, especially in the initial phase of pool creation. 2. [POOL-RATIO-CONSTANT] Repeated rounding can change the ratio of the pool significantly (even without autoswap disabled).

In the violationRuns.qnt::autoswapIssueRun , we give an example in which the ratio starts at 0.0136 and is then changed into 0.0055 within 4 steps. We discussed the issue with the development team and concluded that this violation does not constitute an attack surface, since no free-swap is possible with it. 3. [NO-LOSS-ON-PLACED-TRANCHE] The violation again has to do with the rounding problem when calculating the value to withdraw. This leads to situations in which it is possible for a tranche to have some funds in it, without anybody having shares in the tranche to ever withdraw from it. While the kinds of errors are off-by-one in terms of a token, depending on the price of the maker and the taker, they can be large in terms of the value of the pool.

For an example, see the violationRuns.qnt::noLossOnTranchesViolationRun run.

For an equivalent property [NO-LOSS-ON-PLACED-TRANCHE], which tolerates rounding errors multiplied by number of steps, we found no violation. Moreover, many other properties we checked had violations on their respective versions without tolerance, and we experimented and reasoned about rounding in order to be able to set up tolerances that were enough to make properties hold under different numbers of steps. This was the main struggle of property checking in this project, as many of our long-running experiments would result in violations which, upon debugging, turned out to be yet another not-accounted-for rounding problem. However, the fact that simulation always found violations on the properties that didn't have tolerance is a strong indication that it's coverage is sufficient for these properties. In the next section, we discuss what kind of confidence we can get about the overall functioning of the system based on these simulation results.

Model Simulation: Size of the Input Space Once a model is developed, there are two main ways in going about checking the properties of it. The first one is by doing bounded model checking---a way to inspect all possible behaviors up to a certain length. With Quint, model checking can be done either using a symbolic model checker Apalache, which encodes the whole model as a logical formula and uses a solver to solve it; or using an enumeration-based model checker TLC, which explores all possible states of the model evolution in a breadth-first manner. Unfortunately, the model of the DEX, which captures different actions and exact computations in them, could not be meaningfully checked either with Apalache or with TLC. On top of that exponential growth of the state space, the computation involves

Excerpt (19990 of 31095 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation