Runtime Verification Audits xBacked
Runtime Verification is pleased to announce the completion of the xBacked smart contracts audit. xBacked is building a decentralized, permissionless stablecoin on the Algorand blockchain, fully backed by crypto assets.
Audit scope
The audit was limited to the Reach source code of a set of smart contracts controlling the master vault and stability pool functionalities.
The master vault contracts are the main contracts for holding minted stablecoins, as well as information about the protocol users and who have minted stablecoins. With xBacked, users can create a vault to mint stablecoins, and collateralize it with ALGO or other ASA assets. xBacked is an over-collateralized stablecoin, meaning that all open vaults should have more collateral backing them than needed to cover the minted stablecoins against the vault. The audit included two master vault smart contracts, one for holding ALGO as an asset, and the other for holding ASA assets.
The audited stability pool contract allows for minted stablecoins to be staked & used for liquidations. This will generate yield for users participating in the stability pool. Users are able to monitor the market state and liquidate their capital to hedge against losses, or to let them accrue interest if the market rate is profitable.
The audit covered only the Reach 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, and a detailed list of all the audited contracts can be found in the report.
Methodology
Runtime Verification conducted a manual audit review for a period of 8 weeks, and published a detailed report on May 27th, 2022.
The first step in the audit process consisted of creating a high level structural and operational model of the ecosystem in Alloy language. The model was useful in helping to ensure that the system functioned as expected, and to help identify any potentially dangerous loopholes in the implementation of the code. The model was then used to represent the way participants might interact with the system. The goal was to identify any operations that might interfere with or change the system, and to ensure that these operations didn’t result in errors or vulnerabilities in the implementation.
Once problem behaviors were identified in the contract, the logic of the smart-contract in Reach language was reconstructed into a Python model in order to be used in our in-house tstmodel. Since there are no tools to perform fast modeling of smart-contracts in Reach language, our Python model and in-house tools were used to identify arithmetic precision issues, logic errors or potential malicious behaviors.
Next, we conducted a review of the code changes implemented by the xBacked team to address the problem behaviors. The review lasted a period of two weeks, and details of specific code changes can be found in the report.
Finally, the code was subject to a series of known attack vectors to ensure that its integrity held up to such attacks.
Results
The audit identified five high severity findings, one medium severity, and one informative in the first round. Two medium severity findings and one informative were identified during the second round of the audit process. Users interested in a more detailed and technical explanation about the findings can go over the full report in our GitHub repository.
About xBacked
xBacked is building a decentralized stablecoin on Algorand, xUSD. The protocol ensures all xUSD in circulation is over collateralized by on-chain assets held in vaults. These vaults are collateralized debt positions (CDPs), and work similarly to MakerDAO, Liquity, and other over collateralized stablecoins.
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.
