Runtime Verification audits Pact’s Stableswap AMM smart contract
Runtime Verification is pleased to announce the completion of Pact’s Stableswap AMM smart contract audit. Stableswap is an automated market maker (AMM) built on the Algorand blockchain, offering liquidity to swap ALGO and Algorand Standard Assets (ASA) with low transaction fees.
Audit scope
The audit scope is limited to the PyTeal source code of the Stableswap smart contract and auxiliary files. Pacts Stableswap contract allows for trading stablecoins such as USDT, USDC, or others pegged to USD.
As part of the larger Pact protocol, the Stableswap contract allows for swapping of the above-referenced assets and interacts with the Router smart contract and other asset pools to create seemingly limitless swapping potential.
Since previous audits included Pact’s CPMM with a similar API, this engagement primarily focused on mathematical operations and confirming that changes made to the previous implementation didn't introduce anything harmful to the code.
The audit only covered PyTeal source code contracts and excluded any deployment and upgrade scripts, off-chain codebase, and client-side portions of the codebase.
Interested readers can find a detailed list of all the contracts, libraries, and interfaces audited in the report.
Methodology
Runtime Verification conducted a manual code review of Pact's Stableswap smart contract for a period of 4 weeks and delivered a detailed report on June 6th, 2022.
The first step in the audit process consisted of a manual code review of the Stableswap contract, including a thorough analysis of the mathematical operations used. This stage created the foundation for the rest of the audit: the auditors gained an in-depth understanding of the contract's inner structure and obtained an executable model of the contract.
The next step consisted of integrating the PyTeal source code into PyTeal-Eval, an in-house tool which allowed our auditors to perform a more thorough analysis directly in Python. Tools such as these enable an accurate simulation of the source code behavior.
Next, the code was subject to pattern-based fuzzing of admin and user functions using our in-house TSTModel to check as many scenarios and corner cases as possible and limit the possibility of exploitation.
Finally, since the primary focus of this audit was on the mathematical implementation, additional testing was done using PyTeal-Eval, which also allowed rigorous inspection of the contracts’ behaviors. Any suspicious results were further tested with our in-house TSTGenerator.
Results
The audit identified and highlighted some issues along with a number of informative findings. Three major fixes were audited during the first two weeks of the engagement, and the Pact team addressed all other 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 Pact
Pact is a decentralised automated market maker (AMM) built on the Algorand protocol, with plans to offer deep liquidity and low transaction fees. It allows users to make economical and secure transactions without requiring trust in any intermediary. The web app allows users to interact with Algorand blockchain smart-contracts, facilitating easy swaps between Algo and any other Alogrand Standard Asset (ASA).
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.