Runtime Verification audits EXA Finance’s Baskets smart contract

Runtime Verification is thrilled to announce the completion of EXA Finance’s Baskets smart contract audit. EXA Finance is a peer-to-peer asset exchange marketplace for both fungible and non-fungible tokens built on the Algorand blockchain.

Audit scope

The audit scope is limited to the TEAL source code of two files of a single smart contract implementing the “Baskets” feature, which is part of EXA finance’s core products. The audited contract allows users to handle and trade a group of up to 4 assets using the Basket feature. Users can select from a variety of different exchange models, such as:

• Simple sale: users can choose to sell assets in a simple sale format with assets being sold at a fixed price.
• Shopping cart: users have the option of using a shopping cart function, allowing them to sell a set amount of an asset until the set amount is depleted.
• Simple auction: users can sell assets in an auction format, with the sale going to the highest bidder.
• Reverse/Dutch auction: users can sell assets in a reverse auction format, where the price of the basket goes down gradually to a set minimum until someone buys it.

There is an extra way for users to buy assets called the “explorer functionality”, which is implemented in EXA’s website platform. This functionality allows users to create a direct offer in someone else's profile through the web interface creating a basket that only a fixed buyer, in this case, the one who did the offer, can buy if the other party accepts such an offer.

The audit covered only the TEAL source code contract mentioned in the report and it excluded any deployment and upgrade scripts, off-chain codebase and client-side portions of the codebase.

Methodology

Runtime Verification conducted a manual audit review on EXA Finance’s Baskets smart contract for a period of 7 weeks, and published a detailed report on March 1st, 2022.

The first step consisted of analyzing the documentation provided by EXA Finance and using the available functionalities in the testnet to understand their business model and identify any loopholes in the logic.

Next, the TEAL source code was thoroughly reviewed with the construction of higher-level representations of the TEAL codebase that included automatically generated control-flow graphs and modeled sequences of mathematical operations as equations. The objective was to find any behavior that could cause the code to malfunction, or provide the user with an unexpected result. This approach enabled us to systematically check the consistency between the logic and the low-level TEAL implementation.

Rounds of internal discussions with Algorand experts over the code and platform design were then conducted, aiming to identify any scenarios that were vulnerable to exploitation and to identify improvements for the analyzed contract.

Finally, a review of the TEAL guidelines published by the Algorand Foundation was conducted, together with a review of the code against well-known security threats.

When unexpected outcomes were encountered, they were communicated to the EXA Finance team. If the outcomes were harmful or could lead to an exploit, possible solutions were suggested.

Results

The audit identified and highlighted some issues along with a number of informative findings. The EXA Finance 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 EXA Finance

EXA Finance is a peer-to-peer multi-asset exchange for fungible and non-fungible tokens (NFTs) built by EXA Labs, a French startup based in Paris. The platform leverages the Algorand blockchain to provide best-in-class experiences for users at low cost and with a minuscule carbon footprint.

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.