引入不变性开发即服务

理解和严格测试系统不变性是开发健壮智能合约的关键环节。不变性是指无论发生什么情况都应保持真实的协议事实。定义和测试这些不变性可以使开发者防止引入错误，并长期使代码更加健壮。然而，建立内部知识和流程来创建和维护此类不变性十分困难。因此，只有最成熟的团队已将不变性集成到其开发生命周期中。

认识到这一需求，我们很高兴宣布我们的新服务：不变性开发。该服务的客户将获得：

• 作为代码和规范的不变性
• 关于如何将不变性集成到开发生命周期中的指导
• 关于如何编写不变性的培训
• 额外Trail of Bits服务的优先待遇

全面不变性开发

我们的不变性开发服务为您的代码库识别、开发和测试不变性。虽然我们的安全审查通常包含在认为存在错误的领域开发一些不变性，但该服务旨在更广泛地覆盖代码库中的不变性，帮助您在开发生命周期中实现更全面的长期安全方法——而不仅仅是在最后阶段。

该服务特别适合仍在开发中的代码库，因为它们将使您的工程师能够长期编写更安全的合约。

Trail of Bits工程师将主导与您团队的讨论，以识别和理解系统的不同不变性。我们的服务包括以下活动：

不变性识别。基于我们的经验以及与开发者的讨论，我们将识别潜在的不变性。这可能包括必须相对于函数执行保持的函数级不变性（例如，加法是可交换的）或系统级不变性（例如，用户的余额不能大于总供应量）。我们将用英语指定不变性，并识别其前提条件（例如，参数在给定范围内）。

不变性实现。我们将在Solidity中实现部分识别出的不变性。我们将确定最佳测试方法（内部、外部或部分测试），创建相关包装器，并设置模糊测试初始化（合约部署和前提条件）。我们将尽量减少对代码库的干扰，并选择最合适的方法以确保不变性可以长期使用。

不变性测试与集成。我们将在本地和专用云基础设施上运行不变性。我们将基于模糊运行结果完善规范，识别算术边界，并缩小前提条件以反映现实场景。我们将与开发团队合作，将模糊测试集成到CI中（例如，通过GitHub Actions）进行短期模糊测试活动，并提供在本地或云中运行长期模糊测试活动的建议。

培训与指导。通过此服务，我们的工程师旨在提升您团队的技能，我们将使他们能够编写自己的不变性，并使模糊测试成为您开发过程的重要组成部分。我们将提供关于如何维护提供的不变性以及编写新不变性的指导和建议。此外，我们的专家将提供量身定制的设计建议，以优化代码库进行模糊测试。最后，我们将邀请开发者与我们的工程师共同编写不变性以获得即时反馈。

此外，通过我们不变性服务的客户将获得额外Trail of Bits服务的优先待遇。例如，我们的工程师将利用在不变性开发过程中获得的知识，减少安全审查所需的工作量和成本。

Trail of Bits在提供此服务方面具有独特优势。我们的工程师编写不变性已超过五年（例如，参见Balancer、Primitive和Liquity报告）。我们是多个模糊测试工具的作者（Echidna、Medusa、test-fuzz），并且我们是众多关于模糊测试的教育材料的作者（+150个预定义不变性、如何像专业人士一样进行模糊测试（会议研讨会）、10小时模糊测试研讨会、模糊测试教程）。

增强您的安全性

基于不变性的开发将成为智能合约开发者的标准。我们的新服务将使您能够：

• 在保护代码库方面变得主动而非被动。不变性防止引入错误并解决其根本原因。
• 识别和开发最具影响力的不变性。理解哪些不变性将对安全产生影响需要专门的专业知识，我们的团队将提供这一点。
• 教育团队关于不变性驱动的开发。这将重新调整开发生命周期以预防错误，并使开发者能够将不变性推理集成到其开发过程中。

联系我们，利用我们的经验保护您的代码库。