During Q1 2024, Informal Systems audited Neutron’s liquidity pool migration which dealt with ~23 million USD in users’ liquidity, exchanging Astroport’s XYK liquidity pools for the PCL pools. Migration edge cases were thoroughly inspected to ensure the highest degree of confidence in the protocol.
We performed model-based testing using Quint, our in-house specification language—this enabled us to automatically create tests that explored many different scenarios for the migration protocol.
The scenarios we generated helped us discover critical bugs in the migration process, helping the development team rethink the overall design and implement a more robust solution. We modeled the steps of the migration process and adapted Neutron’s testing suite to execute the scenarios (sequences of steps) generated by Quint. Our model was lightweight and nimble: it only captured certain aspects of the system that our team determined to be the most appropriate. Yet it still proved useful in exploring scenarios that would be impossible to cover with manually written test cases.
Reasoning about large software systems, with all the implementation details, is impossible. This is why security researchers use models — high-level specifications of programs. Once a model has been built, both automated and manual reasoning are easier. On top of that, these models can function as a precise system specification.
Quint is a specification language developed at Informal. Quint comes equipped with a random and symbolic simulator, as well as the model checker, enabling formal verification of models written in Quint. By modeling a software system using Quint, developers can identify potential issues and inconsistencies early in the development process. This proactive approach allows developers to detect design flaws or logical errors even before writing implementation code.
Besides analyzing models, Quint has another important use-case: generating tests from the model that can be run directly against the implementation. Automatically generating tests from the model has two advantages: 1) generated tests will explore scenarios that we as developers would not think of, or would not bother to implement, and 2) any divergence between the implementation and the model will be spotted immediately by a failing test, thus ensuring the specification will always be up to date. This process is called model-based testing and is one of the most useful tools in our auditing toolbox.
Quint carries the semantics of TLA+, and therefore is able to make use of many years of research on formal verification tooling for it, while addressing many problems developers face with TLA+ itself. To learn more about applications of Quint, check out how to automate bug finding in CosmWasm contracts, or how to develop new protocols with the help of Quint.
Earlier this year, Neutron DAO passed a proposal to migrate liquidity on Astroport, locked during Neutron’s Token Generation Event, from the XYK pool to a PCL pool.
After discussing different approaches, the development team opted for a migration approach that mirrors providing liquidity to the new pool: each locked position would migrate individually, starting from the largest locked position.
Every migration process carries many inherent risks and thus careful planning and rigorous testing is necessary. The Neutron development team aimed to make sure users do not lose value during the migration process and the voting power distribution, derived from the locked assets, is not disturbed. Furthermore, users should obtain their fair share of Astroport rewards — failing to ensure that could damage the reputation of the Neutron chain. Therefore, executing migrations with utmost caution was crucial. With that in mind, the development team created a comprehensive end-to-end testing suite to cover all the aspects of the migration process.
In order to examine the migration implementation, we started by creating a Quint model of the migration specification. Specifically, we focused on modeling paths in the system where users' funds were being handled. That meant modeling these paths:
Claiming rewards from either the XYK or PCL pools
Withdrawing rewards from one of the pools
Migrating from one pool to the other
Based on those paths, our modeled contained 5 possible steps, which describe the evolution of the model:
init
claim_rewards_xyk (w & w/o withdraw)
migrate
advance_block
claim_rewards_pcl (w & w/o withdraw)
The advance_blockaction was performed by the system and, as the name suggests, was used to model the advancing of blocks. This was crucial for earning rewards based on staked assets. Both claim_rewards_* actions were executed by users, with or without withdrawing the rewards. If the rewards were withdrawn, they were sent from Astroport’s contract to the user’s address. The migrate action is permissionless, meaning that any user can initiate a migration for themselves or others. Since users could have their assets either locked or vested, we decided to differentiate between these two types of assets when performing actions.
To begin with, the model needs an initial state. We decided to use the usual suspects, Alice, Bob, and Charlieas the users. Each user had either some assets locked or vested, so we modeled the users as a map, mapping the user’s address to the UserData structure. The UserData structure is shown in the following code snippet, with its associated fields:
type UserData = {
migrated: bool,
xyk_liquidity_withdrawn: bool,
xyk_liquidity_withdrawn_before_migration: bool,
pcl_liquidity_withdrawn: bool,
has_xyk_rewards: bool,
has_pcl_rewards: bool,
only_vesting: bool
}
migration field showcased if the migration was performed for that particular user.
xyk_liquidity_withdrawnfield captures whether the XYK liquidity no longer exists, either due to withdrawal or migration.
pcl_liquidity_withdrawn captures whether the PCL liquidity no longer exists, meaning that after the migration, the user has decided to claim the rewards and withdraw the liquidity.
xyk_liquidity_withdrawn_before_migration field shows if the user withdrew liquidity before the migration happened.
Fields has_xyk_rewards and has_pcl_rewards indicate whether the user has earned some rewards. These fields correspond to the advance_block action, as enough blocks passing will result in rewards to claim.
only_vesting field signifies that the user has only vested assets, meaning no rewards will be available to claim.
To use the Quint model effectively, we had to adapt the existing test suite. The first step was bringing it to the model-defined initial state. We generalized the testing suite to accommodate our defined set of users, set their initial locked or vested asset amounts, and advance the blocks to allow them to earn some rewards.
We decided to explore the scenarios defined by the following two predicates:
fullMigrationHappened,and
allPCLLiquidityWithdrawn.
The first predicate tells Quint to generate a large (parameter-defined) number of different scenarios in which all funds from the XYK pool are withdrawn and transferred to the PCL pool. Similarly, the second predicate is used to request scenarios in which all funds that were migrated to PCL pools are subsequently withdrawn. Quint’s simulator explores the state space to give us different scenarios that satisfy our predicate.
Quint generates traces in a JSON-like format called ITF. Each ITF trace represents a sequence of actions, called steps. After performing all the steps, the relevant predicate is satisfied (e.g., allPCLLiquidityWithdrawn).
To utilize the traces, we had to load them into the testing suite and parse them according to the previously defined test structures. This required developing some glue code: it loads and parses the traces and then executes the function in the testing suite corresponding to the step defined in the trace. Now we had steps of the testing suite reliably mimicking the steps in the Quint model.
We checked for correctness by adding postconditions for the executed actions. Based on the trace, we implemented checks to confirm that the model was in sync with the tested implementation, and straight away we noticed that some of the traces were failing. This prompted us to dig further, and together with the Neutron’s development team, we discovered hidden bugs in the system. (We note here that using steps’ postconditions is a deviation from the standard model-based conformance testing approach: typically, we would compare the model-predicted state with the system’s state. Using postconditions, however, enabled us to work effectively with a much lighter model.
initializeState()
for step in ITF_trace.steps {
match step:
"claim_rewards_xyk" -> {
claimRewardsXyk();
checkClaimRewardsXykPostcondition();
},
"advance_block" -> {
advanceBlock();
checkAdvanceBlockPostcondition();
},
"claim_rewards_pcl" -> {
claimRewardsPCL();
checkClaimRewardsPCLPostcondition();
},
"migrate" -> {
migrate();
checkMigratePostcondition();
},
...
}
In this section, let us examine in a step-by-step manner the process of uncovering one particular bug in the system. This is the most technical part of the post, but bear with us: at the end of it, you will have a pretty good idea of the full bug-discovery process.
The (stripped) test scenario included all three actors and consisted of three actions: Bob migrates Alice, Charlie migrates Bob, and Alice claims rewards with withdrawal from PCL pool. Implicit in that description is that some time passes between the actions.
To understand the problem with this scenario, let us outline the behavior we expected from the system. After Alice’s position was migrated from the XYK pool to the PCL pool, a certain amount of time passed before Bob’s position was migrated to the same pool. During that time, Alice should have earned her PCL rewards.
Assume that initially, when Alice was migrated, there was 0 pending rewards for the contract interacting with the PCL pool. After some time has passed, our model says, the contract should have some pending rewards (and they belong to Alice).
Then, it was Bob’s turn to migrate. We let some more time pass after Bob was migrated, and now some more pending rewards were being generated. The next step showed that one of the key migration properties was broken - after claiming her rewards, Alice got a smaller portion of the rewards than what the model expected, and the test failed. (Indeed, she and Bob got the same amount of rewards.)
Why did that happen? Well, the basic idea in calculating the amount of rewards belonging to each lockup position was as follows: every time there is a claim from the pool, a parameter crucial for future calculations, incentives_rewards_per_share, is increased by the fraction of received_amount over the total_lp_balance_deposited. These parameters represent the received amount of tokens and the total balance of deposited LP tokens. This operation ensures that each lockup that existed between two claims gets assigned its share of rewards.
It turned out that there was a catch. Each time new liquidity is provided to the pool, the pool also implicitly sends pending rewards to the lockdrop contract that works with the PCL pool. However, in that case (unlike when explicitly claiming rewards), the parameter incentives_rewards_per_share did not get updated. Thus, all the rewards corresponding to the time when Alice’s funds were in the PCL pool, but Bob had not yet been migrated, were not assigned to Alice.
If you would like to see the fix to the described bug, check out Neutron’s PR#85.
Our industry leading team of technical experts used Quint to uncover critical vulnerabilities in this protocol. In our experience, manual code review is useful. However, uncovering the really tricky, difficult to find bugs requires a more thorough approach, including tools like Quint.
Are you wondering if your project may benefit from model-based testing or protocol analysis? If you would like to work with us to see how Quint can be used to help your project reach the highest level of confidence possible please get in touch with us at audits@informal.systems.
If you would like to try out Quint yourself, check out the rich set of examples and tutorials on the Quint website.