Posted on August 4, 2022 by Melissa Baber
Posted in Audits
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.
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:
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).
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.
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.
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.
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.