Runtime Verification audits Pact’s Router smart contract
Runtime Verification is pleased to announce the audit completion of Pact’s Router smart contract. Pact 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
At the beginning of the year, an audit was conducted on Pact's AMM smart contract in charge of a series of functionalities such as swapping and pooling. After its completion, Runtime Verification was further engaged to audit the Router smart contract, which operates on top of the liquidity pool contract previously audited.
The audit scope is limited to the PyTeal source code of the Router smart contract implementing swaps between various liquidity pools, without requiring a dedicated pool to be in place. For example, a user could exchange goBTC for goETH in one transaction, even without an existent goBTC/goETH pool, by using existing pools such as goBTC/ALGO and ALGO/goETH. The optimal route will be calculated off-chain through Pact’s web frontend and will be later executed by the router contract in an atomic transaction group. The router smart contract offers several benefits to users, such as a more predictable slippage and faster transactions without the need to look for the best route manually.
The audit only covered the PyTeal source code contract and it excluded any deployment and upgrade scripts, off-chain codebase and client-side portions of the codebase.
Methodology
Runtime Verification conducted a code review of Pact’s Router smart contract for a period of six weeks, and published a detailed report on May 10th, 2022.
To begin, a manual code review was conducted on the Router smart contract, with an emphasis to check if the source code implemented all operations declared in the Application Binary Interface (ABI). The ABI is a standard created by the Algorand Foundation to declare a list of the contract’s operations to ease external interaction between different applications. Although not mandatory, the Pact team decided to declare their interface according to Algorand's standard, so other people could use Algorand's tools to interact with Pact's router.
Next, the PyTeal source code of the Router was integrated into a Python based simulated environment in order to test the individual contract ABI endpoints. Every privileged and non-privileged endpoint of the Router contract was tested during this process to ensure that any potential vulnerabilities could be identified. The simulator didn’t require any changes to the codebase, allowing for the simulation to mimic as closely as possible the actual blockchain environment. The liquidity pool smart contract was also added to the model together with a series of behavioral patterns representing different users’ interactions with the router to test if the code of both contracts behaved as expected in different scenarios.
Finally, the contract code was tested in various corner scenarios to identify any loopholes, or any areas that may be vulnerable to exploitation.
Results
The audit identified and highlighted some issues along with a number of informative findings. The Pact team addressed all the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contract. Code changes were not part of the scope; however, some of the changes were informally reviewed by the team.
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 decentralized 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.
