“Using Code4rena early in the development process has allowed us to understand weak points in our code base. Due to the diverse and large set of active wardens competing in Code4rena, you see the code and project through many lenses that you may not have done before.”
Returning to the C4 arena for the second time is Blockswap, a permissionless web3 infrastructure layer for multichain composable ETH. This time around, they’re partnered with both Code4rena and Certora to add a twist to things: a combination of C4’s competitive audit framework, with Certora’s formal verification system. This means that a competitive layer will be added to the construction of abstract representations of Blockswap’s platform, incentivizing Wardens to find scenarios in the code which violate the specifications. For 14 days, Wardens will be participating in the hopes of winning a slice of the $30,000 USDC award pool.
We caught up with Blockswap’s Director of Engineering, Vincent Almeida, to ask him about what prompted their return to Code4rena, why a formal verification approach was chosen, and what’s being looked this time around.
Welcome back! Tell us what prompted you to return to the Arena, a new upgrade? New features?
Previously, we ran a C4 contest against an early preview of the Liquid Staking Derivatives Network (LSD) built on top of Stakehouse protocol. It yielded fantastic results from a standardized manual inspection + Foundry testing perspective. However, when it comes to security, we don’t rest. Part of our regular development practices involves formal verification of the protocols. We build and work with partners such as Certora to achieve that internally and externally, where we decided to formally verify a smart contract from the LSD suite.
After it’s been secured, how do you think the new protocol will affect the industry or the crypto community as a whole?
The idea of the Liquid Staking Derivatives Network (LSD) built on top of Stakehouse protocol is to give anyone the opportunity to start their own liquid staking business in 60 seconds or less. The only requirement is gas for deployment in Ethereum. Being built on top of the Stakehouse Protocol means that despite the fact that there can be 10,000 or more LSD networks on Ethereum, they all benefit from a single liquidity token: dETH. This is truly a new ground-up architecture.
What sets you apart from the competition? What is unique about the protocol and who will be the primary users?
There are 3 main groups of users of the LSD stack:
- Node operators want to own blockspace on the Ethereum consensus layer for 4 ETH. They are free to run any client and hardware they want such as Dappnode.
- Protected stakers want to receive the Stakehouse protocol liquidity token: dETH which accrues slash-free consensus layer yield.
- Fees and MEV stakers want to get democratized access to Ethereum network revenue by contributing at least 0.001 ETH to create a validator
Does your protocol align with the Ethereum roadmap? What are the long-tail benefits for users?
Always. We are long Ethereum decentralization and we shall never surrender is our tagline in this regard. Firstly, we never enforce any specific software on any node runner and we encourage client diversity at all levels. Node running is permissionless and so is staking. Validators at the Stakehouse protocol level are never pooled. This means the protocol and anything built on top of it has anti-centralizing forces baked in — all this without a relayer or oracle.
LSD Networks are an extension of Stakehouse and provide the easiest access for long-tail users. Users receive the benefits of highly orchestrated pooling with 1:1 accounting for staked ETH and their liquid derivatives. This is all done out of the box. Following in the footsteps of Ethereum, we believe that market forces shall drive users to congregate and coordinate in a fair and open manner. Stakehouse operates optimally in a permissionless and decentralized environment. This means it is resilient to centralizing actors. Therefore, Stakehouse protects the common user by ensuring they have access to their assets on both the execution layer and consensus layer. By breaking up the various stakeholders into Protected Stakers, Fees and MEV stakers, and node operators, LSD Networks serve the end user without giving up the freedoms of Ethereum staking.
Since this is an MEV payout contract, it folds into a larger initiative of Blockswap; That is ensuring Ethereum stays neutral and uncensored. We have our Proof of Neutrality product which is a lightweight block proposer builder separator (PBS). Privacy is a right and it’s the responsibility of everyone to uphold a permissionless and inclusive future for web3.
There is a pledge going around for the Ethereum community to join together against centralization. Sign it here.
It’s not your first time sharing your code with C4’s community of anonymous security researchers. What do you think others could learn from undergoing an audit with Code4rena?
Using Code4rena early in the development process has allowed us to understand weak points in our code base. Due to the diverse and large set of active wardens competing in Code4rena, you see the code and project through many lenses that you may not have done before. Additionally, the nature of how the contests are configured means that wardens are incentivized to find more obscure vulnerabilities as prize money associated with low-hanging fruit will likely be split amongst many participants. You get a very interesting adversarial environment that yields great results.
It seems like every other week there’s a new event in the industry that makes crypto projects revisit their approach to security, what do you think is a security non-negotiable that new web3 projects should be thinking about?
While we could highlight many of the approaches taken whilst developing the Stakehouse protocol and Liquid Staking Derivative networks, time and time again formal verification is at the centre of everything. More teams should be thinking about formal verification even in the simplest of projects. Should the specifications be implemented correctly, formal verification allows mathematical modeling of a system that can be run against the specification in order to mathematically prove correctness against all inputs. This makes it stronger than fuzzing and therefore unit tests. However, we still engage in the latter as we still find bugs with more traditional approaches to testing.
Learn more about Blockswap
- Security approach: https://www.blockswap.network/security
- Website: https://www.blockswap.network/
- Twitter: https://twitter.com/Blockswap_team
- Discord: https://discord.gg/s8N9ekQuuj
Blockswap’s $30k formal verification competition in partnership with Certora and Code4rena opens January 19th, 2023, and runs for 14 days. Details here.
C4 Trailblazers puts the spotlight on projects and founders that have returned to the Arena and demonstrated a commitment to security.
