With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review
Lido is a DeFi protocol that offers liquid staking solutions where users can stake ETH and receive liquid staked tokens (stETH) which can be used across the DeFi ecosystem. Runtime Verification engineers specialize in formal verification and symbolic execution of smart contracts applying their expertise to provide high assurance that systems perform as specified. In April 2024, Runtime Verification completed a design review of Lido's dual governance mechanism. This mechanism is the first of its kind, representing a monumental upgrade to the Lido governance model. This collaboration aimed to ensure that the new system, scheduled for testnet release in Q3 2024 and mainnet in Q4 2024, functions as intended and maintains the integrity and security of Lido’s $33 billion in total value locked (as of this writing).
The Need for Dual Governance
The introduction of dual governance in Lido is driven by the need to balance power between stETH and LDO token holders and address limitations posed by Ethereum’s validator exit queue. In traditional finance, users are constrained in how they can exit the system by their centralized counterparties. For example, a user cannot get money out of their bank without visiting a branch or an ATM, relying on bank's centralized infrastructure. The non-custodial nature of DeFi gives users the unique power to exit independently of any centralized entity.
In the case of Lido, the dual governance upgrade aims to create checks and balances between protocol users (stETH holders) and token holders (LDO holders). If enough stETH holders signal their opposition to a DAO proposal, the DAO functionality is temporarily frozen, preventing proposal execution until a resolution is reached. This mechanism gives users veto power over DAO proposals, or to be more precise, it gives users the power to pause proposals from taking effect until they withdraw their ETH stake from the protocol.
How Dual Governance Works
Dual Governance V1 gives stETH holders a direct path to signal their opposition to LDO token holders actions by using their stETH to veto on-chain. As more stETH holders join the veto, the DAO functionality (outside of treasury spending) is frozen, preventing all proposals from passing. At this point, LDO holders have two options:
- Cancel Pending Proposals: The decision can be reached that the proposal should not go through. If this happens, the DAO returns to its regular state.
- Escalate the Proposal: If the proposal is escalated when there is significant stETH holder opposition, a rage quit is triggered. In this case, the DAO remains paused until all stETH holders who voted to veto the proposal have a chance to withdraw their ETH. Once all stETH vetoers have been made whole, the DAO reverts to its regular state.
This system ensures that stETH holders have a significant say in governance decisions, adding a layer of security and trust to the protocol.
Scope of Engagement and Methodology
Our engagement with Lido focused on a thorough design review of Lido's dual governance system. We encourage every protocol to start with such a review, as the majority of critical vulnerabilities that we've detected so far were on the system design level. The design review can help catch and mitigate those early. We started by studying the specifications and documentation. This system involves several contracts: DualGovernance.sol, Executor.sol, Escrow.sol, EmergencyProtectedTimelock.sol, and Configuration.sol. These contracts collectively manage proposal submission, execution, and opposition signaling.
The advantage of having Runtime Verification perform a design review is our quantitative approach and formal verification expertise. In addition to helping our partners write clear, easy to understand specifications, we write mathematical proofs that can be used to prove the correctness of the code under review. These proofs can be automated using symbolic execution - tested for the entire possible input space - to ensure that the system can never reach a state outside of the bounds defined by the specification. This approach provides our partners with the highest assurance level that their implementation adheres to the specification.
In the Lido review Runtime Verification built a simplified model of the system and abstracted the implementation details in order to capture high-level behavior. We identified critical security properties and wrote formal proofs to ensure these properties held true according to the specifications. In the next stage of this engagement (June 2024), we will symbolically execute these proofs and prove the system can never reach a state outside of the bounds defined in the specification. This process is computationally intensive, but it can be outsourced by using KaaS (K as a Service), leveraging our highly customized servers to handle the load - an option the Lido team is taking advantage of.
The beauty of this approach is that it allows Runtime Verification formal engineers to work alongside the smart contract developers at Lido before the smart contracts are finalized and help them make implementation decisions that focus on the security of the code being developed. Once our teams agree on the specification, code changes trigger KaaS to execute the proofs again without the need of any further review by formal engineers. Even after the engagement, the Lido team can change the code and re-run the proof with no involvement from Runtime Verification. We believe that enabling protocols to take this process in-house is a significant improvement in how smart contract developers think about security in the future.
Addressing Potential Attacks
There are two opposing ways in which a malicious actor might attack the protocol:
- Delay the Proposal Execution: similar to Denial of Service, an adversary slows or freezes the execution of DAO proposals.
- Trigger Early Execution: this attack triggers proposal execution before stakers can exit the protocol.
Dual Governance protocol parameters such as VetoSignalingMinActiveDuration (), VetoSignalingDeactivationMaxDuration (), DynamicTimelockMaxDuration, and VoteCooldownDuration can affect the delay on proposal execution in various ways. These parameters are quantified internally by the dual governance contracts.
The Ragequit process will affect the range uniquely because it depends on a mechanism external to the Dual Governance protocol. This makes sense because various stakers may require different durations to unwind their DeFi positions and reclaim their ETH. In other words, the time from when the rage quit state is entered until the last withdrawal request is claimed, cannot be determined based on the internal state of Dual Governance.
Understanding these parameters and their interactions allows us to bound the time between proposal submission and execution.
Two Key Proofs
As a result of our design review, we developed proofs of two critical properties: Maximum Time Lock and Staker Reaction Time.
Maximum Time Lock
This proof ensures that the protocol transitions from the Veto Signaling state to the Veto Cooldown state within a defined time frame, considering maximum Ragequit support and other variables.
Suppose that at time 𝑡 𝑎𝑐𝑡 𝑆 the Dual Governance protocol enters the Veto Signaling state. If a rage quit isn't triggered, and assuming that state transitions are activated as soon as they become enabled, the protocol will transition to the Veto Cooldown state at a time 𝑡 𝑎𝑐𝑡 𝐶 > 𝑡 𝑎𝑐𝑡 𝑆 such that:
𝑡 𝑎𝑐𝑡 𝐶 ≤ 𝑡 𝑎𝑐𝑡 𝑆 + 𝑇 𝑙𝑜𝑐𝑘 ( 𝑅 𝑚𝑎𝑥 ) + 𝑇 𝑚𝑖𝑛 𝑆 𝑎 + 𝑇 𝑚𝑎𝑥 𝑆 𝐷 + 2
where 𝑅 𝑚𝑎𝑥 is the maximum rage quit support between 𝑡 𝑎𝑐𝑡 𝑆 and 𝑡 𝑎𝑐𝑡 𝐶, and 𝑇 𝑙𝑜𝑐𝑘 ( 𝑅 𝑚𝑎𝑥 ) is the dynamic timelock for this amount of rage quit support. The proof involves analyzing the transition conditions between states and ensuring that the maximum duration is respected under all possible conditions.
Staker Reaction Time
This proof guarantees that stakers can extend the Timelock for proposal execution if they amass enough Ragequit support before the ProposalExecutionMinTimelock expires. This prevents the execution of proposals too quickly, allowing stakers time to react.
Suppose that a proposal is submitted at time 𝑡 𝑝𝑟𝑜𝑝 , and let 𝑡 1 and 𝑡 2 be such that:
𝑡 𝑝𝑟𝑜𝑝 ≤ 𝑡 1 ≤ 𝑡 𝑝𝑟𝑜𝑝 + 𝑇 𝑚𝑖𝑛 ≤ 𝑡 2
where 𝑇 𝑚𝑖𝑛 is ProposalExecutionMinTimelock. If between 𝑡 1 and 𝑡 2, the rage quit support is never lower than some value 𝑅 𝑚𝑖𝑛 such that
𝑡 2 ≤ 𝑡 𝑝𝑟𝑜𝑝 + 𝑇 𝑙𝑜𝑐𝑘 ( 𝑅 𝑚𝑖𝑛 )
then the proposal cannot be executed at any time less than or equal to 𝑡 2. In other words, if the stakers amass at least rage quit support before passes, they can extend the timelock for as long as rage quit support is maintained, up to ().
The proof involves detailed mathematical reasoning about the state transitions and the conditions under which stakers can maintain sufficient support to delay proposal execution.
The Power of Formal Verification
The Dual Governance upgrade is a new paradigm in on-chain governance and an impressive undertaking for Lido. The decentralized nature of Ethereum creates an adversarial environment, so ensuring that the change to the governance machinery of a $33B protocol is done securely is an unnerving undertaking. We are proud that Lido trusted our approach and hope to prove with the highest assurance level possible that the dual governance will serve both LDO and stETH holders as designed for years to come.
Our engineers are Runtime Verification believe that a thorough design review and formal verification of smart contracts will be the future of smart contract security. Currently, protocols rely too heavily on manual code reviews and audit contests. It is difficult to quantify the efficacy of a manual code review (typical audits), and some auditing firms already greatly underbid and under-deliver on their audit engagements. Audit contests, on the other hand, run for a limited time and it is unlikely that they provide a complete coverage of the entire codebase due to how incentives are aligned. Formal verification can achieve an objective standard in the future, giving users an unparalleled confidence in the security of the smart contracts they are interacting with.
Are you interested in seeing formal verification in action?
Kontrol is an open-source, free-to-use tool developed and maintained by Runtime Verification. You can install the tool by following the documentation. You can clone the Dual Governance repository, and see our proofs in action - or write your own. You can also run Kontrol on any existing project that has a foundry test suite, as Kontrol is able to hook onto those tests and execute them as formal verification proofs.
If you need help, join our Kontrol Telegram, or reach out to us.
