Runtime Verification audits Blockswap’s Stakehouse protocol

Runtime Verification is thrilled to announce Blockswap’s Stakehouse protocol audit completion. Stakehouse is a programmable staking layer allowing users to register a consensus layer validator and mint tokens representing the validator’s balance. The user’s initial stake is minted partly as dETH, with more being minted when the validator earns rewards, and partly as SLOT, which represent management rights of the validator and carry risk of being slashed if the validator is penalized.

Audit scope

The audit scope covers the Solidity source code of Blockswap labs - Stakehouse protocol smart contracts. Some of the main functionalities implemented in the contracts consist of:

• Registering a KNOT (a validator in the protocol).

• Reporting an increase in a KNOT's balance in the Beacon Chain due to validator rewards or a decrease due to penalties (and minting or slashing the corresponding tokens).

• Moving a KNOT between indices.

• Withdrawing or depositing dETH into the open index.

• Topping up SLOT that has been slashed by paying ETH.

• Recovering a KNOT's signing key.

• Rage-quitting a KNOT, enabling the staked ETH for withdrawal.

A detailed explanation of the different functionalities just mentioned can be found in Blockswap’s documentation.

Due to limited time and the extensive list of contracts covered, the core contracts were prioritized during the audit process following discussions with the Blockswap team. A detailed list of all the audited contracts can be found in the report.

The audit only covered Solidity source code contracts and it excluded any deployment and upgrade scripts, off-chain codebase and client-side portions of the codebase, as well as the security of the cryptography underlying the Common Interest Protocol used to recover the signing key.

Methodology

Runtime Verification conducted a combination of design review and manual code review for a period of 11 weeks, and published a detailed report on March 27th, 2022.

The first step consisted of using a Solidity-like pseudocode to build a high-level model of key parts of the protocol. This model was used to get a better understanding of the protocol and its behavior based on the documentation and other resources provided by the Blockswap team, and to make it easier to observe how different operations would modify the protocol's state and which properties should hold during the protocol’s operation.

A manual code review was then performed to identify scenarios where the code didn’t function in the way the model expected it to, as well as to look for common security vulnerabilities.

Working together with the Blockswap team, certain aspects of the protocol which were of particular concern were singled out, and a pen-and-paper analysis was carried out to identify issues and potential risks in implementation. Additionally, a series of changes were proposed that could lead to an improvement of the protocol’s performance and security in certain areas.

Finally, various tools were run against the code to analyze certain parts of the protocol, aiming to either identify scenarios where desirable properties of the protocol were violated or develop confidence that these properties were maintained. When it was not practical to run these tools on the code itself, they were run on a modified version of the high-level model.

Results

The audit identified and highlighted some issues along with a number of informative findings. The Blockswap 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; however, the team conducted a lightweight best-effort review of a limited number of changes.

Users interested in a more detailed and technical explanation about the findings can go over the full report in our GitHub repository.

About Blockswap

Blockswap is a permissionless web3 infrastructure layer for multichain composable ETH. This ETH is superfluid, doesn’t require an intermediary, doesn’t require a bridge, is capital efficient, and provides yield singularity with native blockchain cryptographic security. Multichain composable ETH is a new primitive for interoperability between blockchains, L2/rollups, and end users. Blockswap's protocols introduce the new standard of tooling to build multichain and yield capturing protocols.

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.