Ockam 的密码学设计审查

2023年10月，Ockam 聘请 Trail of Bits 审查其产品的设计，该产品是一组旨在实现跨各种异构网络的安全通信（即，端到端加密和相互认证的通道）的协议。一个安全的系统始于设计阶段，这为安全的实现和部署奠定了基础，尤其是在密码学中，安全的设计可以避免整个漏洞。

在这篇博文中，我们将深入了解我们对 Ockam 协议的密码学设计审查，重点介绍初始设计的几个积极方面，并描述我们为进一步加强系统安全性而提出的建议。对于任何考虑与我们合作以改进其设计的人来说，这篇博文还从幕后展示了我们的密码学设计审查服务，包括我们如何使用形式化建模来证明协议满足某些安全属性。

以下是 Ockam 的首席技术官 Mrinal Wadhwa 对与 Trail of Bits 合作的评价：

Trail of Bits 为我们的审查带来了卓越的协议设计专业知识、仔细的审查和对细节的关注。与他们的深入和细致的讨论帮助我们进一步增强了对设计选择的信心，改进了我们的文档，并确保我们仔细考虑了客户数据的所有风险。

Ockam 系统和 Ockam Identities 概述

Ockam 是一组协议和托管基础设施，可实现安全通信。用户也可以在他们的场所部署 Ockam，从而无需完全信任 Ockam 的基础设施。我们的审查基于 Ockam 的两个用例：

1. TCP portals：跨越各种网络并穿越 NAT 的安全 TCP 通信
2. Kafka portals：通过 Apache Kafka 进行安全数据流传输

Ockam 的一个关键设计特性是，安全通道是使用 Noise 框架的 XX 模式的实例化来建立的，这种方式与网络层无关（即，通道可以为 TCP 和 Kafka 网络以及其他网络建立）。

Ockam 部署的一个主要组成部分是 Ockam Identities 的概念。Identities 唯一地标识 Ockam 部署中的一个节点。每个节点都有一个自我生成的标识符和一个关联的主密钥对，该密钥对会随时间轮换。每次轮换都使用当前和下一个主密钥进行密码学证明，从而创建一个变更历史。因此，identity 由标识符和关联的签名变更历史定义。具体构造如图 1 所示。

图 1：Ockam Identities

主密钥不直接用于 Noise 协议中的身份验证或会话密钥建立。相反，它们用于证明用于安全通道建立和凭证颁发的 purpose keys。这些凭证的作用类似于传统 PKI 系统中的证书，以实现相互信任并强制执行基于属性的访问控制策略。

手动评估过程

我们对 Ockam 设计规范进行了手动审查，包括安全通道、路由和传输、身份和凭证，重点关注我们在类似通信协议中看到的潜在密码学威胁。手动审查过程发现了五个问题，主要与假设和预期安全保证的文档不足有关。这些发现表明，规范中的信息不足，例如威胁建模，可能导致 Ockam 用户在对协议的理解不完整的情况下做出对安全至关重要的决策。

我们还提出了一些与规范和我们从对实现的粗略审查中发现的实现之间的差异有关的问题。即使实现不在本次审查的范围内，我们经常发现当设计文档不清楚并且可以用不同的方式解释时，它可以作为基本事实。

使用 Verifpal 和 CryptoVerif 进行形式化验证

除了手动审查 Ockam 设计外，我们还使用形式化建模工具来自动验证特定的安全属性。我们的形式化建模工作主要集中在 Ockam Identities 上，它是 Ockam 系统的关键要素。为了实现全面的自动分析，我们使用了协议分析器 Verifpal 和 CryptoVerif。

Verifpal 在符号模型中工作，而 CryptoVerif 在计算模型中工作，这使它们成为一组互补的工具。Verifpal 发现了针对协议的潜在高级别攻击，从而可以在找到安全设计之前对协议进行快速迭代，而 CryptoVerif 提供了更低级别的分析，并且可以更精确地将协议的安全性与实现中使用的各个原语的密码学安全保证联系起来。

使用 Verifpal 方便的建模功能和内置原语，我们为 Ockam Identities 建模了一个（简化的）场景，其中 Alice 向 Bob 证明她拥有与 Bob 当前尝试验证的对等标识符关联的主密钥。我们还模拟了一个场景，其中 Bob 验证了由 Alice 发起的新更改。

使用 Verifpal 建模协议表明，Ockam Identities 的设计实现了预期的安全保证。对于给定的标识符，只有主密钥持有者可以生成有效的初始更改块，该更改块将公钥绑定到标识符。保证任何后续更改都由持有先前和当前主密钥的实体生成。尽管建模很容易，但使用 Verifpal 证明安全保证需要一些技巧，以防止该工具识别出琐碎或无效的攻击。我们在我们的综合报告中讨论了这些注意事项。

Ockam Identities 的当前实现可以使用两种签名方案中的任何一种来实例化，ECDSA 或 Ed25519，它们具有不同的安全属性。CryptoVerif 强调，根据协议的预期，ECDSA 和 Ed25519 不一定提供相同的安全保证。但是，文档中没有明确提及这一点。

Ed25519 是首选方案，但 ECDSA 也被接受，因为它目前受到大多数云硬件安全模块 (HSM) 的支持。对于 Ockam Identities 的当前设计，ECDSA 和 Ed25519 在理论上提供相同的保证。但是，Ockam Identities 的未来更改可能需要仅由 Ed25519 提供的其他安全保证。

有时，协议需要比通常预期的签名方案属性更强的属性（请参阅 似乎合法：对使用签名的协议的细微攻击的自动分析）。因此，从设计的角度来看，最好能够很好地理解并明确说明协议构建块中期望的属性。

我们加强 Ockam 的建议

我们的审查未发现范围内用例中的任何问题，这些问题会对 Ockam 处理的数据的机密性和完整性构成直接风险。但是，我们提出了一些建议，以加强 Ockam 协议的安全性。我们的建议旨在实现深度防御、面向未来的协议、改进威胁建模、扩展文档并明确定义 Ockam 协议的安全保证。例如，我们的一项建议描述了保护未来量子计算机免受“现在存储，以后解密”攻击的重要注意事项。

我们还与 Ockam 团队合作，充实规范中缺失的信息，例如记录某些主密钥字段的确切含义并创建正式的威胁模型。这些信息对于 Ockam 用户在部署 Ockam 协议时做出合理的决策非常重要。

总的来说，我们建议 Ockam 明确记录有关密码协议的假设以及 Ockam 系统每个组件的预期安全保证。这样做将确保协议的未来开发建立在充分理解和明确的假设之上。应该记录的假设和预期安全保证的良好例子是 ECDSA 与 EdDSA 之间的理论问题（我们使用 CryptoVerif 识别出）以及使用具有较低安全裕度的原语不会显着影响安全性。

Ockam 的首席技术官对上述建议的回应如下：

我们认为，易于理解和开放的 Ockam 协议和实现文档对于不断提高我们产品提供的安全性和隐私至关重要。Trail of Bits 对我们的协议文档进行的彻底的第三方审查以及对我们的协议进行的形式化建模，有助于使我们的文档更容易被我们的开源社区持续审查和改进。

最后，我们强烈建议对 Ockam 协议实现进行（内部或外部）评估，因为安全的设计并不意味着安全的实现。协议部署中的问题可能源于设计和实现之间的差异，或者源于违反设计中假设的特定实现选择。

安全是一个持续的过程

在评估开始时，我们观察到 Ockam 设计遵循最佳实践，例如使用业界广泛接受的强大的原语（例如，带有 AES-GCM 和 ChachaPoly1305 作为 AEAD 以及带有 Ed25519 和 ECDSA 用于签名的 Noise XX 协议）。此外，该设计反映出 Ockam 考虑了系统安全性和可靠性的许多方面，包括例如各种相关的威胁模型和身份的信任根。此外，通过开源其实现并发布评估结果，Ockam 团队创建了一个透明的环境，并邀请社区进一步审查。

我们的审查确定了一些需要改进的领域，并提供了加强产品安全性的建议，该产品已经建立在良好的基础之上。你可以在综合报告中找到有关评估、我们的发现和我们的建议的更多详细信息。

该项目还表明，安全是一个持续的过程，在设计阶段尽早考虑安全因素可以建立一个坚实的基础，实现可以安全地依赖它。但是，始终有必要不断努力提高系统的安全态势，同时充分应对新的威胁。评估设计和实现是确保系统安全性的两个最关键的步骤。

如果你想与我们的密码学团队合作以帮助改进你的设计，请联系我们 - 我们很乐意与你合作！

• 原文链接： blog.trailofbits.com/202...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～