2023-05-16 Audit Report - Duality Dex and Incentives modules

Security Audit Report

Duality: Dex and Incentives modules

Authors: Andrey Kuprianov, Ivan Golubovic, Aleksandar Ljahovic

Table of Contents Audit Overview ............................................................................................................ 1 The Project 1 Scope of this audit 1 Conducted work 1 Conclusions 1 Further Increasing Confidence 2 Audit Dashboard ......................................................................................................... 3 Target Summary 3 Engagement Summary 3 Severity Summary 3 System Overview......................................................................................................... 4 Modules 4 Threat Inspection........................................................................................................ 7 User categories 7 DEX related threats 7 Incentives related threats 8 Findings ..................................................................................................................... 11 Repetetive exponentiation in price computation may lead to DOS 13 A byzantine consumer can cause chain halt via pricing tick 15 Loss of user funds via shares rounding with large ticks 17 Stealing of user funds via negative deposits 19 Wasteful usage of storage creates a potential for DOS attacks 21 Denom collisions can be exploited to steal user funds 23 Stakes querying not handling stakes with multiple coins 27 Tick and Fee inputs are not validated 29 Incomplete validation of MsgDeposit 31 Optimize stakes querying 32 Number of epochs for gauge creation is not validated 34 Invalid Multi Hop Swap routes cause panic 36 Improvements for better efficiency 38 © 2023 Informal Systems Duality: Dex and Incentives modules

Large string for token causes panic 40 Minor code improvements for Incentives module 42 Minor code improvements for the DEX module 43 Appendix: Vulnerability Classification ..................................................................... 44 Impact Score 44 Exploitability Score 44 Severity Score 45 Disclaimer.................................................................................................................. 47 © 2023 Informal Systems Duality: Dex and Incentives modules

Audit Overview The Project Duality is a "concentrated liquidity exchange", which means that for a given trading pair, it relies on many different constant-sum AMM pools to fill orders. This is in contrast to simpler AMM exchanges, which rely on a single constant-product market maker pool to fill orders. The comparative advantage of the constant-sum AMM design is that it allows users who wish to LP to have total control over where they place their liquidity and how much they charge in fees. In its design, Duality combines two approaches to liquidity (thus the name): AMMs (liquidity pools), and Order books (limit orders).

Scope of this audit The audit took place from April 18, 2023 through May 12, 2023 by Informal Systems by the following personnel: • Andrey Kuprianov • Ivan Golubovic • Aleksandar Ljahovic During the audit, we focused on analyzing the x/dex and x/incentives modules; the remainder of the system was largely considered a "black box" during the audit. In particular, it has been explicitly negotiated that the mechanisms of integrating Duality with Cosmos Hub as a Replicated Security consumer chain is outside of the scope of this audit, and needs to be addressed separately.

Conducted work Within the scope of the audit project the following work has been conducted: • Manual code inspection of the DEX and Incentives module. We have carefully inspected the code base of these modules, and documented our understanding in the section “System Overview”; manual code inspection allowed us to discover the majority of the findings in the present report. • Reconstruction of the mathematical protocol employed by the DEX module, and modeling it in the Quint specification language. Due to the limited timeline of the project we’ve been able to complete only around 80% of the model (e.g. limit orders are not yet modeled, or not all error conditions are covered). Despite these limitations, the Quint DEX model allowed us to discover 2 of the 4 critical findings listed in the present report. • Whenever possible, we’ve tried to reproduce the findings using Duality’s integration test suite; the corresponding integration tests are included into the text of the respective findings.

Conclusions In general, we found the codebase to be of very high quality: the code is well-structured and easy to follow, and the test suite includes both unit and integration tests. Despite the high code quality we have discovered 4 Critical and 2 High severity findings, the rest of the findings being Medium, Low, or Informational severity. From our analysis, we would like to point to the following areas of immediate, relatively low effort improvements to the codebase: • Comprehensive validation of system inputs is needed. Around half of the findings we’ve discovered in the course of this audit are due to either missing, or incomplete validation of transaction parameters. • The test infrastructure needs to be made more general and data-driven. The current test suite, while being well thought-though and easy to use, is too limited in order to test all possible scenarios that are important for the system correctness. E.g., only two token types (“TokenA”, “TokenB”) can be supplied to the tests; or a very limited, set of users (“Alice”, “Bob”, “Carol”) can be employed in the tests, and only via calling the appropriately named test functions (e.g. “aliceDeposits” or “assertBobBalances”), etc. These limitations need to be lifted, and the test infrastructure needs to be made data-driven, when the arbitrary

test inputs can be supplied as data, and not as Go code. This should allow to both reduce the amount of code in the test suite, and simultaneously to substantially increase its coverage.

Further Increasing Confidence Based on the modeling efforts in Quint for the DEX module, we can safely recommend to the Duality developers to continue this route. A formal model can serve both as a concise documentation of the system behavior, as well as a means of uncovering protocol level bugs in the mechanism design, which would be very difficult to find otherwise. As immediate next steps we recommend the following: • Allocate the time to finalize the DEX Quint model. The goal here is to obtain the complete specification of the DEX protocol, as well as to formulate and validate the set of formal properties the system should satisfy. E.g., with the current model we’ve come very close to formally describing and validating the following (informal) English language property: a. In any system state, when a liquidity provider deposits an amount of tokens to a liquidity pool; b. Followed by any number of system actions; c. When the liquidity provider withdraws all the shares obtained in step a), they obtain the amounts of tokens that are not smaller than the originally deposited token amounts, taking into account the exchange rate of the liquidity pool in question. • Formally model the Incentives module, formulate and validate its properties. From our analysis we can say that formal modeling of this module in Quint should bring substantial benefits in understanding and validating the underlying protocols, as it includes non-trivial distribution logic involving the time axis. • Implement the infrastructure for model-based testing (MBT) of DEX and Incentives modules, and integrate it into the project CI: when the aforementioned generalization of the test suite is performed, and the tests are data-driven, then performing MBT on the base of Quint models should dramatically increase the test coverage, via the systematic exploration of all possible scenarios of system evolution.

Audit Dashboard Target Summary • Type: Specification and Implementation • Platform: Golang • Artifacts: • Duality DEX module at v0.2.0 • Duality Incentives module at v 0.2.0

Engagement Summary • Dates: 18.04.2023 to 12.05.2023 • Method: Manual code review, protocol analysis, formal modeling • Employees Engaged: 3

Severity Summary Finding Severity #

Critical 4

High 2

Medium 2

Low 5

Informational 3

Total 16

System Overview Duality’s mission is to give liquidity providers superpowers by creating sustainable and powerful financial markets. Duality is introducing a novel mechanism design which combines the advantages of AMMs and order books. Duality can reach order-book levels of capital efficiency (zero price impact on trades, swaps, and limit orders) while still maintaining the computational efficiency and liveness properties of AMMs. At the core of the AMM lays an incredibly simple swap mechanic: liquidity pools that allow traders to buy or sell tokens at a constant price. While two liquidity providers on Duality may prefer completely different liquidity distributions, they will still use the same underlying pools. The only difference is the amount deposited in each pool.

Modules

DEX module The DEX (Decentralized Exchange) module holds the core functionality for token swaps, limit orders, and liquidity provisioning

Data structures (KV Stores):

Messages:

Deposit Enables tokens to be deposited in different pools for the same pair of denoms. Based on the amount of deposited funds, shares tokens are calculated and sent to the receiver, while the deposited funds are transferred to the dex module. Also, data structures (pool, tick, pair) are checked, initialized and updated in this message.
Withdrawal Enables the withdrawal of funds for the same pair of denoms from different pools, by specifying ticks and fees. Also, for each pool, it is possible to specify the number of shares tokens that you want to withdraw. The calculation determines the amount of certain tokens that corresponds to the given amount of share tokens. If everything goes as expected, shares tokens are withdrawn from the caller's account and burned, and the calculated amount of tokens are sent to the receiver's account.

Swap Allows the user to exchange a certain amount of a token with a certain amount of another token. It is iterated by the Liquidities corresponding to the tokens participating in the swap. In each iteration, a swap is performed over the current liquidity, and as a result, the amount of in/out tokens used from that liquidity for the swap is returned. The iteration ends either when the amount of input tokens reaches the specified maximum or when all iterations are finished. The Liquidity interface has two implementations: PoolLiquidity and LimitOrderTranche Input tokens are sent from the caller's account to the dex module, and output tokens are sent from the dex module to the receiver's account.
MultiHopSwap Allows specifying multiple possible routes to swap tokenA for tokenB: OSMO -> ATOM -> ETH OSMO -> ATOM -> USDC -> ETH OSMO -> USDC -> ETH For each of the routes, the best price for the swap between two tokens is calculated, until the end is reached. There is an option to specify whether to calculate the best route or swap according to the first one from the collection. Input tokens are sent from the caller's account to the dex module, and the calculated output tokens are sent from the dex module to the receiver's account.
PlaceLimitOrder Enables adding a limit order for a certain pair of denoms, the amount of input token, tick and order type.
WithdrawFilledLimitOrder Calculates and sends filled liqudity from module to user for a limit order based on amount wished to receive.
CancelLimitOrder Removing a specified number of shares from a limit order and returning the respective amount in terms of the reserve to the user

Incentives module Incentive module represents Duality’s take on rewards program. The intention is to reward users providing liquidity for trading. In Duality’s terms this means providing liquidity on particular positions where the position is defined by token pair and chosen tick range. From high level perspective, the module is organized around two main types: gauges and stakes. The following diagram explains the structure of the types and basic operations:

As it is shown above, basic operations include four messages:

CreateGauge for constructing the gauge itself and adding coins to it. The operations includes storing gauge to appropriate KV store, it’s indexing and emitting of event. After the gauge is created, the response is returned.
AddToGauge is designed to handle increasing of coin amount in the gauge. It includes validation of gauge’s activity (coins cannot be added to finished gauges) as well as event emitting and response when the message is processed.
Stake message is created to support creating of new stake or adding stakes to already created ones. The most important parts of this operation include owner validation and denom calculation. It is not allowed to stake multiple tokens. Event emitting and response also included.
Unstake comprises of iterating through unstaking array and finding and executing eligible unstakes. Eligibility depends on coin amount, owner and time of unstaking action. It also includes event emitting and response. Apart from four messages described above, probably the most important action is the reward distribution. It is executed in Distribute function inside keeper. It strongly depends on epochs (time period for rewards distribution), as it can be executed only upon active gauges which are determined by comparing gauge time and running block time. All eligible gauges are looped with their respective stakes. To perform the reward distribution, coins must be extracted from stake, and rewards have to be properly calculated. The concept used to calculate the reward is the pricing_tick. It is designed to support fair distribution and stop reward increase in cases of users staking greater amounts on specific positions. The distribution event is triggered when all the rewards are delivered to addresses that “deserved” their reward.

Threat Inspection User categories • Duality stakeholders: Duality owners, or whoever has an economic upside from the Duality itself • Liquidity providers (LPs): Users who provide their tokens, and thus give liquidity for trades. Their main incentive is to get upside from trades via fees • Traders: Users who perform trades on Duality. Their incentive is to extract value via trading tokens at different exchanges at varying valuations.

DEX related threats

Threat: Traders' tokens are lost while swapping The DEX module has certain super-powers (e.g. transferring tokens from a user account via Bank module’s SendCoinsFromAccountToModule ). If not used carefully, this may have disastrous consequences for users.

• Impacted users: • Traders • Possible impacts: • Loss of funds • Possible ways of exploitation: • Submitting a transaction with specially crafted inputs (e.g. such that the coins with the wrong denoms are used) • Audit actions: examine all places where superpowers (Bank module methods) are used: • from where these methods are used • How their inputs are formed • Whether those inputs can be maliciously crafted to perform an exploit.

Threat: Traders get unfair swap price The main incentive for traders to participate in Duality is to trade their tokens at the expected prices. We should make sure that the core Duality swapping logic is correct • Impacted users: • Traders • Liquidity providers • Possible impacts: • Traders receive an unfair amount of swapped tokens • receiving less means traders lose their funds • receiving more means the system is exploitable, and liquidity providers lose their funds. • Possible ways of exploitation: • Discovering a flaw in the economic mechanism and submitting a crafted transaction to exploit it • Audit actions: validate Duality core swap protocols • reconstruct the protocol from code, and model them in Quint • formulate desirable properties of the protocol (invariants) • (partially) validate invariants via Quint simulation • (for the future): validate reconstructed protocols with the mechanism design expert

Threat: Liquidity providers get unfair shares When LPs submit their funds into liquidity pools, they receive shares instead. We should make sure that the shares they receive are fair wrt. all parameters. • Impacted users: • Liquidity providers • Possible impacts: • LPs submitting funds receive an unfair amount of shares • receiving less means they lose their funds • receiving more means the system is exploitable, and other liquidity providers lose their funds. • Possible ways of exploitation: • Discovering a flaw in the economic mechanism and submitting a crafted transaction to exploit it • Audit actions: validate Duality core LP protocols • reconstruct the protocols from code, and model them in Quint • formulate desirable properties of the protocols (invariants) • (partially) validate invariants via Quint simulation • (for the future): validate reconstructed protocols with the mechanism design expert

Threat: Out-of-thin-air token generation due to swap rounding Calculations when doing swapping are non-trivial, with multiplication and truncation, and multiple cases. (see e.g. Pool::Swap0To1()). Rounding errors may lead to generation of residual tokens; however small, this may lead to depleting the reserves. • Impacted users: • Duality stakeholders • Liquidity providers • Possible impacts: • Loss of funds • Possible ways of exploitation: • Submitting multiple transactions with specially crafted inputs (e.g. very large values) • Audit actions: precisely understand the logic there, and how it will behave: • under various combinations of conditions • when some of the inputs/state variables are very small or very large • whether the rounding errors can be exploited in user’s favor.

Incentives related threats • Miscalculation that can be abused to lead to unfair allocation of rewards. Miscalculation in terms of amount can harm both users and chain holders. Apart from amount, the denomination (also a result of some sort of calculation) should always be correct in order not to reward arbitrary tokens. • Routing tokens to incorrect user. Since the number of users that are involved in staking is presumably arbitrary, it should be inspected that rewards distribution is correctly routed and that rewards always end up on accounts that really did the staking and “deserved” the reward. • Abuse the time concept of rewarding mechanism - stop or delay reward distribution. The rewards are distributed using epochs module which is responsible for creating particular time periods in which the distribution is happening. The mechanism should be resistant to any abuse that some rewards are not distributed until the end of period. • Malicious validators with significant portion of power trying to control incentives mechanism. This threat is in some cases known as 66% attack and it implies there are validators with voting power exceeding 66% and that their intentions are malicious in any way. In this particular case, the goal would be

to misuse incentives program (create any of the previous threats maybe) or to take control of it in a way that no other validators can be rewarded. •

Excerpt (19996 of 79049 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation