Runtime Verification audits Blockswap’s Stakehouse code changes

Runtime Verification is pleased to announce the completion of Blockswap’s Stakehouse second smart contract audit. 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 carries the risk of being slashed if the validator is penalized.

Audit scope

Following the initial audit of the Stakehouse protocol, Blockswap Labs further engaged Runtime Verification to audit changes made to the code. Based on the advice from their first round audit, a few large upgrades were made to the code. Following security best practices, these upgrades were presented to Runtime Verification for a review. The audit scope is limited to the Solidity source code of several major changes to the smart contracts including:

• Changes related to the balance reporting mechanism. In the previous audit, multiple issues related to the balance reporting mechanism in both the Stakehouse and the deposit router were identified. This is mainly due to the complicated nature of the off-chain deposit router needing to consolidate information from both the Beacon Chain and the Execution Layer (current Ethereum Mainnet) during the process. During this engagement, the bulk of our time spent with these contracts focused on major fixes to the balance reporting.
• Special exit fee. This is a new feature added to the contracts following the first round audit. Its purpose is to track penalties that go beyond 4ETH.

In addition to these changes to the contracts, various smaller changes made in response to issues identified in the previous audit were included in the scope to ensure that the highlighted issues were addressed properly.

The audit only covered Solidity source code contracts and it excluded any deployment and upgrade scripts, off-chain codebases and client-side portions of the codebase. A cursory review of the deposit router was conducted as well (an off-chain component).

Methodology

Runtime Verification conducted a manual code review for a period of 3 weeks, and delivered a detailed report on June 6th, 2022.

The first step in the audit process consisted of creating a high level model of the contracts subject to the audit. Separate models were developed for the general Stakehouse protocol and the balance reporting mechanism. Since each model focused on different aspects, separating the two made it easier to reason about them. For the balance reporting mechanism, creating a high level model was especially important due to the complex interactions between the Execution Layer and the Beacon Chain. The difficulty is in ensuring that when the deposit router combines information from both chains, they are still in sync. Otherwise an attacker may be able to exploit the router.

The previous audit primarily focused on coming up with scenarios that would break the balance reporting mechanism in some way. However, as the complexity increases, trying to find scenarios becomes more difficult, and it is impossible to ensure that potentially dangerous scenarios are not missed.

Instead, the high level model was used to define precisely what the correct behavior should be. A set of requirements was derived that, if they are enforced, ensure correctness.

Afterwards, a pen and paper proof sketch of these requirements was created to ensure that they really do ensure correctness when enforced.

Finally, the implementation was examined to ensure that it enforces all the necessary requirements.

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. Although code change reviews were not part of the audit scope, a best effort review was conducted on some minor code 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 Network 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.