Runtime Verification Audits Tinyman AMM V2
Runtime Verification is pleased to announce the completion of the Tinyman AMM V2 security audit. Tinyman is a constant-product automated market maker built on Algorand, offering advanced decentralized trading services, such as flash loans and flash swaps.
Audit Scope
Following the completion of the version one audit and its release in October 2021, Runtime Verification was further engaged to audit the new V2 of the Tinyman AMM protocol prior to its release.
The V2 release sports a more efficient codebase by taking advantage of recent updates to the AVM (Algorand Virtual Machine) and will provide users with several additional features, including flash swaps, flash loans, and configurable pool fees.
The audit scope included the entirety of the on-chain smart contracts implementing Tinyman AMM V2 core functionalities.
The audit scope is limited to the contracts’ Tealish source code and the generated TEAL code. Tests and testing scripts are outside of the scope of this audit. A detailed list of all the contracts audited can be found in the report.
Methodology
Runtime Verification conducted a combined design review and manual code review for a period of 5 weeks, and delivered a detailed report on November 23, 2022.
The first stage of the audit process consisted of a thorough review of the protocol's documentation and the implementation of the codebase. During this phase, rounds of discussion with the Tinyman team allowed for a better understanding of the audit's priorities.
and, if they do, to check whether the code is vulnerable to them.
Next, the code underwent a thorough manual review, including the following steps:
The first step in the manual code review consisted of reviewing the lifecycle of a pool, determining which operations the approval contract allows, in which state, and who is authorized to initiate these operations. During this step, special attention was given to the consequences of rekeying the pool to the Approval contract.
Next, the various checks implemented by the contracts were reviewed to ensure that interactions with the application and the pools conformed to the defined interface. To make this review more systematic and comprehensive, two different approaches were devised and followed: a manual approach that lists all transaction fields in all transactions and their intended restrictions, and an automatic approach that included the use of a mathematical model of these transactions and their restrictions which automatically checked for violations. This step helped identify or confirm missing input validation checks.
The next step included analyzing the implementation of the protocol’s mathematical formulas as statements and arithmetic expressions, including arithmetic overflow, underflow, and division-by-zero errors, and the effects of rounding down with integer division and square-root operations.
As the contracts are written in Tealish, what followed was a review of the TEAL code generated by the Tealish transpiler (source-to-source compiler) to validate the translation from the Tealish contracts to the corresponding TEAL contracts. This was important to avoid having to trust the Tealish transpiler codebase and to ensure that the generated TEAL is accurate.
Throughout the code review, several important properties and invariants were identified that the contracts must maintain. These properties should hold in the contract’s state before and after the execution of a contract call. These properties were analyzed against the implementation, using a paper-and-pencil style of reasoning which produced informal but detailed arguments of why the implementation satisfies these properties.
Finally, a number of patches and fixes to the codebase were reviewed in preparation for the audit report.
Results
The audit identified and highlighted some issues along with some informative findings. Runtime Verification worked with the Tinyman team to review fixes to these issues and their implementation in the smart contracts.
As in previous versions of Tinyman AMM contracts, the V2 AMM contracts implement a permissionless protocol where pools operate autonomously. No account has authority over any pool or its tokens (and so pools cannot be cleared or closed out) beyond protocol fees and pool donations, which are currently managed by a set of authorized accounts. Furthermore, the contracts are immutable, so they cannot be deleted or updated.
Readers interested in a more detailed and technical explanation of the findings can go over the full report in our GitHub repository.
About Tinyman
Tinyman is a re-imagined decentralized trading protocol which utilizes the fast and secure framework of the Algorand blockchain, creating an open and safe marketplace for traders, liquidity providers, and developers.
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.