Ockam加密设计审查 - Trail of Bits博客

Joop van de Pol, Marc Ilunga, Jim Miller, Fredrik Dahlgren
2024年3月5日
审计, 密码学, 设计审查

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

在本博客文章中，我们深入探讨了对Ockam协议的加密设计审查，重点介绍了初始设计的几个积极方面，并描述了我们为进一步加强系统安全性提出的建议。对于任何考虑与我们合作改进设计的读者，本文还提供了我们加密设计审查服务的一般幕后视角，包括我们如何使用形式化建模来证明协议满足特定安全属性。

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

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

Ockam系统及Ockam身份概述

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

• TCP门户：跨各种网络并穿越NAT的安全TCP通信
• Kafka门户：通过Apache Kafka的安全数据流

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

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

图1：Ockam身份

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

手动评估过程

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

我们还提出了一些与规范和实现之间差异相关的问题，这些差异是我们从对实现的粗略审查中发现的。尽管实现不在本次审查范围内，但我们经常发现，在设计文档不清晰且可以以不同方式解释的情况下，实现可以作为基本事实。

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

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

Verifpal在符号模型中工作，而CryptoVerif在计算模型中工作，使它们成为互补的工具集。Verifpal发现针对协议的潜在高级攻击，支持快速迭代协议直到找到安全设计，而CryptoVerif提供更底层的分析，并可以更精确地将协议的安全性与实现中使用的各个原语的加密安全保证联系起来。

利用Verifpal方便的建模能力和内置原语，我们为Ockam身份建模了一个（简化的）场景，其中Alice向Bob证明她拥有与Bob当前正在验证的对等标识符关联的主密钥。我们还建模了一个Bob验证Alice发起的新变更的场景。

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

Ockam身份的当前实现可以用两种签名方案中的任何一种实例化，ECDSA或Ed25519，它们具有不同的安全属性。CryptoVerif强调，ECDSA和Ed25519不一定提供相同的安全保证，具体取决于协议的期望。然而，文档中未明确提及这一点。

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

有时，协议需要比签名方案属性通常期望的更强属性（参见Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures）。因此，从设计角度来看，期望对协议构建块的预期属性有充分理解并明确说明。

我们加强Ockam的建议

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

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

通常，我们建议Ockam明确记录关于加密协议的假设以及Ockam系统每个组件的预期安全保证。这样做将确保协议的未来开发建立在充分理解和明确的假设之上。应记录的良好假设和预期安全保证示例包括我们使用CryptoVerif识别的ECDSA与EdDSA的理论问题，以及使用较低安全边界的原语不会显著影响安全性。

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

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

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

安全是一个持续的过程

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

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

该项目还表明，安全是一个持续的过程，在设计阶段早期纳入安全考虑为实施可以安全依赖奠定了坚实基础。但始终需要不断努力改进系统的安全状况，同时充分应对新威胁。评估设计和实施是确保系统安全的两个最关键步骤。

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

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容
Ockam系统及Ockam身份概述
手动评估过程
使用Verifpal和CryptoVerif进行形式化验证
我们加强Ockam的建议
安全是一个持续的过程
近期文章
Trail of Bits的Buttercup在AIxCC挑战赛中获得第二名
Buttercup现已开源！
AIxCC决赛：记录表
攻击者的提示注入工程：利用GitHub Copilot
发现NVIDIA Triton中的内存损坏（作为新员工）
© 2025 Trail of Bits.
使用Hugo和Mainroad主题生成。