Runtime Verification Audits Tinyman

Runtime Verification is thrilled to announce Tinyman's audit completion. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Tinyman's Audit Scope

Before Tinyman's launch, their team has decided to audit the project's code with Runtime Verification to identify any issues that could cause the system to malfunction or be exploited.

Tinyman's protocol is built with Algorand’s Layer-1 smart contract language TEAL and aims to serve as a decentralized trading platform, similar to the Uniswap protocol, for the Algorand community. The protocol is built using two core smart contracts:

• The Pool Logic Signature Template (a stateless TEAL smart contract template), from which contract accounts representing liquidity pools are created.
• The Validator Application (a stateful TEAL smart contract), which implements the protocol's logic and maintains the state of the system on the blockchain. The contract was created by the core team and is immutable.

Runtime Verification performed an audit on the two contracts just mentioned above and the system's high-level documentation. The focus was reviewing the high-level business logic (protocol design) of Tinyman's system based on the provided documentation and reviewing the low-level implementation of the system in TEAL. In addition, the audit highlighted some informative findings that could improve the performance and efficiency of the implementation and optimize its code size.

Methodology

Runtime Verification team lead Musab Alturki conducted Tinyman's audit and published a detailed report on August 4th, 2021.

The first step consisted of rigorously reasoning about the business logic of the contract and validating security-critical properties to ensure the absence of loopholes in the logic. We also reviewed past public audit reports of Uniswap v1 and v2 and checked if the list of known issues could be applied to Tinyman, and in case they did, to check the code to make sure there is no space for any vulnerability. This step was crucial to conduct as Tinyman's system is based on Uniswap's AMM (Automated Market Maker) design.

The second step consisted of reviewing the contract source code to detect any unexpected (and possibly exploitable) behaviors. We applied an approach that consisted of constructing different high-level representations of the TEAL codebase to systematically check consistency between the logic and the low-level TEAL implementation.

The third step consisted of reviewing the TEAL guidelines published by Algorand to check for known issues and reviewing a list of known Ethereum security vulnerabilities and attack vectors to check whether they apply to TEAL smart contracts and, if they do, to check whether the code is vulnerable to them.

Results

The audit identified and highlighted some critical issues along with a number of informative findings (see the report for details). The Tinyman team properly addressed all the issues and concerns raised during the audit, and incorporated all the necessary changes in the smart contracts.

Finally, in a concluding phase of the audit, we further reviewed the security impact of the changes made based on the issues raised in the first phase and investigated their effects on other parts of the contracts to ensure that no new issues or vulnerabilities were introduced in the process.

We enjoyed working with the Tinyman team and wish them the best of luck with their project.

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.