QuipuSwap‘s token-to-token smart contracts were audited by the Runtime Verification team, which uses runtime verification-based methods to perform security audits on virtual machines and smart contracts on public blockchains.
New token-to-token swaps contracts created on the Tezos smart-contract language Ligo have been tested for code correctness and security. The report became available to the community.
Methodology
Initially, the business logic of the contract was defined and analyzed. This allowed us and the Runtime Verification team to focus on the main features of the functionality and eliminate all loopholes and inconsistencies between the original idea and implementation.
Contract validation included reviewing each entrypoint for errors and potential attack scenarios. At the second stage, the behavior and state of the contract were analyzed during chains of calls and sequential execution.
The audit did not cover off-chain components, client-side portions of the codebase, and deployment/upgrade scripts.
Conclusions
All proposals from Runtime Verification to improve and fix contracts have been accepted by MadFish and re-verified by auditors. You can view the full audit report with technical details in the GitHub repository.
About Runtime Verification
Runtime Verification startup uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. Runtime Verification deals with software testing for blockchain technology companies in order to improve the safety, reliability, and correctness of software systems.