Runtime Verification audits Swell Network

Runtime Verification is thrilled to announce Swell Network’s audit completion. Swell Network is a next-generation permissionless, non-custodial, liquid staking protocol for Ethereum. Stakers with Swell receive a newly minted swNFT that denotes their staking position and provides access to future rewards, as well as the protocol’s liquid staking derivative token, swETH, which is backed by staked ETH on the Beacon Chain, empowering stakers with more flexibility, liquidity, and yield opportunities.

Design modelling

Runtime Verification was approached by Swell Network at an early stage of development. This engagement at a preliminary phase offered a series of opportunities and insights for Swell, which are commonly overlooked by developers including areas such as security, guidelines, and time consumption. The engagement occurred in advance of key functions being finalized.

In the case of Swell Network, a design modelling was conducted on the unfinished contract to not only identify and verify important security properties as early as possible, but also to gain some clarity on how to develop the remaining protocol functions in a faster and more efficient way while maintaining a higher degree of confidence on the security front. A series of potential corner cases were identified for the functions under development, making their development smoother and faster as well as making future audits shorter and more efficient.

Audit scope

The audit scope focused on the Solidity source code of the three main contracts with some limitations, and a series of utility functions:

• The "SWNFTUpgrade" smart contract implements all the Swell-specific operations. This smart contract is currently under development, and only a limited number of operations were audited, including stake, deposit, withdraw, depositing swETH into a vault and withdrawing swETH out of a vault.
• The "SwETH" smart contract is an ERC-20 derivative token that is fully backed by ETH.
• The "SwDAO" smart contract is the governance token of the Swell Protocol.

All analysis of the above contracts was done assuming the correct implementation of the Vault smart contract, as well as the correct implementation of the remaining functions of SWNFTUpgrade: unstake, swap, and redeem.

The audit only covered Solidity source code contracts and it excluded any deployment and upgrade scripts, off-chain codebase, client-side portions of the codebase and, a series of libraries and smart contracts assumed to be correct.

Methodology

Runtime Verification conducted a manual code review for a period of 3 weeks and a detailed report will be published in the upcoming weeks.

The first step consisted of creating an abstract model of all the operations of the smart contracts, including those operations that were still in development. Having a complete model helped to evaluate if the existing code allowed the implementation of the planned operations under development. A longer period of time than usual was dedicated to the review of the design of the protocol and the creation of the abstract model to account for the missing parts and to ensure, as much as possible, a smooth implementation of the features in the future.

The second step consisted of identifying a series of safety properties and verifying that they held under certain assumptions and behaved as expected. Those assumptions were extracted from the documentation and the code itself with the help of the Swell team, and were used to prove some of the safety properties against the model as the implementation was not fully finished. The SMTChecker tool was also used to prove some of the properties in an automated way.

Before finalizing the audit, the code was checked against common security vulnerabilities to identify as many exploit scenarios as possible.

Results

The audit identified and highlighted some issues along with a number of informative findings. The Swell Network team addressed all the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contracts. Code changes were not part of the scope and only a limited number of very small fixes went through a lightweight best-effort review.

A report will be published in the upcoming weeks with a detailed technical explanation of the findings in our GitHub repository. An announcement will be made on our Twitter account once the report is available to everyone.

About Swell Network

Swell Network DAO is delivering the next-generation Ethereum liquid staking that is permissionless, decentralized, and non-custodial. Swell is built for stakers and node operators. With Swell, stakers will be able to securely and seamlessly liquid-stake their ETH, earning attractive yields in a non-custodial manner and node operators will be able to leverage their financial and technical resources through Swell’s smart contracts.

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.