Runtime Verification audits QuipuSwap’s token-to-token distributed exchange

Runtime Verification is thrilled to announce the audit completion of QuipuSwap’s token-to-token distributed exchange (TTDex). QuipuSwap is an automated market-maker (decentralized exchange) built on the Tezos blockchain.

Audit scope

The audit scope was limited to the token-to-token distributed exchange smart contract code. The contract can execute multi-token routes with fewer contract calls allowing lower fees and improved performance compared to other exchange models.

The code was written in Ligo, a high-level language for Tezos smart contracts aimed at helping developers write shorter and simpler code which eases the workload for security experts conducting audits.

After the initial audit period, all changes the QuipuSwap team made to address findings were re-reviewed.

As mentioned, the audit only covered Ligo source code; off-chain components of the system, client-side portions of the codebase, and deployment/upgrade scripts were excluded from the scope and not reviewed.

Methodology

Runtime Verification conducted a manual audit on QuipuSwap’s token-to-token distributed exchange smart contract for a period of five weeks and published a detailed report on November 5th, 2021.

The first step consisted of reasoning about the business logic of the contract. This helped both teams identify a list of properties to be validated and rule out possible loopholes in the business logic and inconsistencies between the logic and the implementation. The property validation was carried out in two different phases, first by considering each entrypoint independently, then by considering sequences of entrypoint calls.

The first phase consisted of analyzing each entrypoint independently to identify any bugs in the code (and if a bug was found, find a feasible attack scenario). Once the first phase was completed, the second phase was carried out and aimed to check if properties were held after subjecting entrypoints to multiple contract calls in sequence (the code should continue to behave as expected even with chains of calls).

Lastly, the code was checked against a series of already known security issues and attack vectors to rule out additional potential exploits.

Results

The audit identified and highlighted some issues along with a number of informative findings. The QuipuSwap team addressed all the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contract.

Users interested in a more detailed and technical explanation about the findings can go over the full report in our GitHub repository.

About QuipuSwap

QuipuSwap is a Tezos DEX with on-chain governance for baking rewards developed by the Madfish team. It was launched in April 2021 and allowed anyone to add any Tezos based tokens to DEX. At the moment, QuipuSwap has more than 300 trading pairs and 7+ million liquidity. The team plans to release token-to-token and stable pools soon.

About Runtime Verification

Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.

--

--

--

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

How to Mine/Stake MCL (Marmara) Coin?

Reading Gems of 2018 (so far…) 💎 📖

WHEN THE BLOCKCHAIN DOES THE LAUNDRY

iEx.ec — A blockchain revolution of the Cloud computing business

Crash Course: Blockchain

[Press_Release] Wemade and Rock Square Signed an MOU For WEMIX Platform On-boarding

The Case for an Institutional DeFi dApp

Augur: product review

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Runtime Verification

Runtime Verification

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

More from Medium

Axelar is a universal interoperability platform that connects all blockchains through a…

The cross-chain communication problem and the role of Axelar Network in the global blockchain…

Penguin Finance — How to use the section “Bond”. [EN]

Axelar is a universal interoperability platform that connects all blockchains through a…