本文介绍了Symbiotic协议在即将上线主网前与Certora合作进行的安全审计，发现并解决了多个关键问题，包括更严格的访问控制和更好的存取款处理。此外，文章详细介绍了财务验证的过程和获得的安全增强措施，为即将到来的主网发布做好了充分准备。
在主网发布协议是一个 高风险里程碑，尤其是引入像 restaking 和 slashing 这样的创新机制。Symbiotic 与 Certora 合作，确保通过彻底的审计获得强大的安全性，发现问题并通过形式验证验证协议的核心属性。
在我们的审计过程中，我们发现了一些关键问题，包括 slashing 操作中的一个问题，并通过形式验证验证了关键安全属性。这些发现导致了像更严格的 访问控制、改善存款和取款的处理、以及增加 对潜在DoS攻击的保护 等修复。
在本文中，我们将深入探讨我们识别出的问题、实施的解决方案，以及我们的合作如何帮助 Symbiotic 为即将到来的主网发布做好准备。
确保 Symbiotic 的主网准备就绪
Symbiotic 是一个共享安全协议，作为一个薄协调层，使网络构建者能够以无许可的方式控制和调整他们自己的 (re)staking 实现。
考虑到主网部署的高风险，该团队聘请 Certora 识别潜在问题、验证安全属性，并增强协议对新兴威胁的防范。
Certora 结合手动代码审查和形式验证，提供全面的洞见，确保每个协议组件在所有场景下都按预期运行。
对 Symbiotic 安全性的关键贡献
1. 解决问题
在审计过程中，Certora 发现了 slashing 操作中的一个问题，其中执行顺序问题可能会阻止特定的 slashes。为了解决这个问题：
- 实施了更严格的访问控制。
- 将 slashing 职责委托给一个可信的网络。
这些修复确保恶意行为者无法干扰 slashing 操作，显著增强了协议的弹性。
2. 核心属性的形式验证
Certora 利用其 Prover 工具对 Symbiotic 的关键属性进行数学验证，包括：
- 准确处理存款和取款。
- 质押和 slashing 状态转换的完整性。
- 遵守网络和质押限制。
这种 形式验证 确保协议遵循其设计意图，消除了通过传统测试可能未被发现的漏洞。
3. 缓解中等和低严重风险
还缓解了其他问题，例如在 slashing 过程中可能出现的 DoS 风险和 gas griefing。采取的措施包括：
- 防止恶意循环的重入保护。
- 更新文档以增强开发者可用性。
- 加固策略以减少未来攻击面。
这些改进不仅加强了安全性，还提高了协议的可靠性和可用性。
结果
Certora 与 Symbiotic 的合作带来了显著的安全增强。通过解决问题并提供形式保障，该协议现在已为其主网发布做好充分准备，为用户和开发者提供一个安全可靠的平台。
“Certora 对安全的严格方法使我们能够解决问题，并自信地准备主网。他们的见解对我们的成功至关重要。” Symbiotic 团队
探索完整审计报告
深入了解我们的发现和 Symbiotic 的安全增强详情。
→ 阅读完整报告
