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 ProSwap platform engulfs Ethereum network?

Blockchain and BlocBuy

DLTx: A Mission-driven Public Company

The development prospect and prospect of NFT

All about Chains: Layer 1, Layer 2 and Side Chains

Potential Project Analysis: BSC Dinosaur Eggs as a New Gameplay that Integrates DEX and Social

Why Blockchain is a Hammer Looking for a Nail and Where it Might Find it

Why Blockchain is a Hammer Looking for a Nail and Where it Might Find it

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

Hyundai x Meta Kongz

Innovative DAO aggregation platform: VboxDAO’s world’s first main sub-DAO integration

Demystifying StarkNet accounts

ProofID — W3C DID Spec