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.
