Runtime Verification audits Pact
Runtime Verification is thrilled to announce Pact's audit completion. 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
Pact engaged Runtime Verification to review the protocol’s architecture and code to identify any possible issues before launching their project publicly. A week before finishing the audit, Pact launched their tesnet to collect feedback about the platform user experience and any possible bugs on the UI/UX level. The completion of this audit, together with the testnet deployment, are necessary steps to prepare for the mainnet launch.
The audit scope is limited to one smart contract, written in PyTeal, in charge of the swapping, pooling and associated functionalities. Libraries used to develop the smart contract were also informally reviewed during the audit together with the documentation.
Off-chain components of the system and patches to fix or improve findings were not audited. However, an exception was made for finding A1, where an informal review of the implemented fix was made.
Methodology
Runtime Verification conducted an audit on Pact's smart contract for a period of six weeks and published a detailed report on January 31st, 2022.
The audit process combined tool-assisted modelling of the protocol and a manual review of the documentation and code to find as many attack scenarios as possible during the six weeks.
One of Pact's core features is the implementation of a Constant Product Market Maker with fees (CPMM). We decided to make a high-level model of Pact’s CPMM protocol to ensure that we had the correct idea of intended behavior for Pact's CPMM, and that the system design itself had no known pitfalls. The most suitable solution was to build a high-level model of the smart contract using K-framework while focusing on the protocol properties described in Pact's documentation.
A manual code review of the system implementation was also carried out to identify attack scenarios arising from code errors or Algorand and Teal specific considerations. During the manual code review, the objective was to find issues related to the code of the smart contract built on the Algorand blockchain. The manual code review complements the high-level model of the smart contract to help find issues in the PyTeal implementation in addition to the system design.
Results
The audit identified and highlighted some issues along with a number of informative findings. Pact team addressed all the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contract. The audited contract's source code is high quality, and the team assisted us at all times with any questions related to the code and its functionality.
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.