Launching a protocol on the mainnet is a high-stake milestone, especially when introducing innovative mechanisms like restaking and slashing. Symbiotic partnered with Certora to ensure robust security for a thorough audit, discovering issues and validating the protocol’s core properties through formal verification. 

During our audit, we uncovered key issues, including an issue in slashing operations, and validated critical security properties using formal verification. These findings led to fixes like stricter access controls, improved handling of deposits and withdrawals, and added protections against potential DoS attacks.

In this article, we’ll dive deeper into the issues we identified, the solutions implemented, and how our collaboration helped prepare Symbiotic for its upcoming mainnet launch.

Ensuring Symbiotic’s Mainnet Readiness

Symbiotic is a shared security protocol that serves as a thin coordination layer, empowering network builders to control and adapt their own (re)staking implementation in a permissionless manner. 

Recognizing the high stakes of mainnet deployment, the team engaged Certora to identify potential issues, validate security properties, and fortify the protocol against emerging threats. 

Certora combined manual code reviews with formal verification to deliver comprehensive insights, ensuring every protocol component operates as intended across all scenarios.

Key Contributions to Symbiotic’s Security

1. Resolving Issues

During the audit, Certora identified an issue in slashing operations, where execution order issues could prevent specific slashes. To address this:

• Stricter access controls were implemented.
• Slashing responsibilities were delegated to a trusted network.

These fixes ensure malicious actors cannot interfere with slashing operations, significantly enhancing protocol resilience.

2. Formal Verification of Core Properties

Certora utilized its Prover tool to mathematically validate Symbiotic’s critical properties, including:

• Accurate handling of deposits and withdrawals.
• The integrity of staking and slashing state transitions.
• Compliance with network and staking limits.

This formal verification guarantees that the protocol adheres to its intended design, eliminating vulnerabilities that might go unnoticed through traditional testing.

3. Mitigating Medium and Low Severity Risks

Additional issues, such as potential DoS risks and gas griefing during slashing, were mitigated. Measures included:

• Reentrancy guards to prevent exploitative loops.
• Updated documentation to enhance developer usability.
• Hardening strategies to reduce future attack surfaces.

These improvements not only strengthened security but also enhanced the protocol’s reliability and usability.

Results

Certora’s collaboration with Symbiotic resulted in significant security enhancements. By addressing issues and providing formal assurance, the protocol is now well-prepared for its mainnet launch, offering users and developers a secure, dependable platform.

“Certora’s rigorous approach to security allowed us to address issues and prepare confidently for mainnet. Their insights were invaluable to our success.”

Symbiotic Team

Explore the Full Audit Report

Dive into the details of our findings and Symbiotic’s security enhancements.

→ Read the Full Report