In October 2023, Ockam hired Trail of Bits to review the design of its product, a set of protocols that aims to enable secure communication (i.e., end-to-end encrypted and mutually authenticated channels) across various heterogeneous networks. A secure system starts at the design phase, which lays the foundation for secure implementation and deployment, particularly in cryptography, where a secure design can prevent entire vulnerabilities.
2023 年 10 月，Ockam 聘请 Trail of Bits 审查其产品的设计，该产品是一组协议，旨在实现跨各种异构网络的安全通信（即端到端加密和相互验证的通道）。安全系统从设计阶段开始，这为安全实施和部署奠定了基础，特别是在密码学领域，安全设计可以防止整个漏洞。
In this blog post, we give some insight into our cryptographic design review of Ockam’s protocols, highlight several positive aspects of the initial design, and describe the recommendations we made to further strengthen the system’s security. For anyone considering working with us to improve their design, this blog post also gives a general behind-the-scenes look at our cryptographic design review offerings, including how we use formal modeling to prove that a protocol satisfies certain security properties.
在这篇博文中，我们深入了解了奥卡姆协议的密码设计审查，强调了初始设计的几个积极方面，并描述了我们为进一步加强系统安全性而提出的建议。对于任何考虑与我们合作改进其设计的人，这篇博文还对我们的加密设计审查产品进行了一般性的幕后观察，包括我们如何使用形式化建模来证明协议满足某些安全属性。
Here is what Ockam’s CTO, Mrinal Wadhwa, had to say about working with Trail of Bits:
以下是 Ockam 的首席技术官 Mrinal Wadhwa 对于与 Trail of Bits 合作的评价：
Trail of Bits brought tremendous protocol design expertise, careful scrutiny, and attention to detail to our review. In depth and nuanced discussions with them helped us further bolster our confidence in our design choices, improve our documentation, and ensure that we’ve carefully considered all risks to our customers’ data.
Trail of Bits 为我们的审核带来了丰富的协议设计专业知识、仔细的审查和对细节的关注。与他们进行深入细致的讨论帮助我们进一步增强了对设计选择的信心，改进了我们的文档，并确保我们仔细考虑了客户数据的所有风险。
Overview of the Ockam system and Ockam Identities
奥卡姆系统和奥卡姆恒等式概述
Ockam is a set of protocols and managed infrastructure enabling secure communication. Users may also deploy Ockam on their premises, removing the need to trust Ockam’s infrastructure completely. Our review was based on two use cases of Ockam:
Ockam 是一组协议和托管基础设施，可实现安全通信。用户还可以在自己的场所部署 Ockam，从而无需完全信任 Ockam 的基础设施。我们的评论基于 Ockam 的两个用例：
- TCP portals: secure TCP communication spanning various networks and traversing NATs
TCP 门户：跨各种网络并穿越 NAT 的安全 TCP 通信 - Kafka portals: secure data streaming through Apache Kafka
Kafka 门户：通过 Apache Kafka 保护数据流
A key design feature of Ockam is that secure channels are established using an instantiation of the Noise framework’s XX pattern in a way that is agnostic to the networking layer (i.e., the channels can be established for both TCP and Kafka networking, as well as others).
Ockam 的一个关键设计特征是，使用噪声框架的 XX 模式的实例化来建立安全通道，其方式与网络层无关（即，可以为 TCP 和 Kafka 建立通道）网络，以及其他）。
A major component of an Ockam deployment is the concept of Ockam Identities. Identities uniquely identify a node in an Ockam deployment. Each node has a self-generated identifier and an associated primary key pair that is rotated over time. Each rotation is cryptographically attested to with the current and next primary keys, thereby creating a change history. An identity is therefore defined by an identifier and the associated signed change history. The concrete constructions are shown in figure 1.
Ockam 部署的一个主要组成部分是 Ockam 恒等式的概念。身份唯一标识 Ockam 部署中的节点。每个节点都有一个自行生成的标识符和一个随时间轮换的关联主键对。每次轮换都使用当前和下一个主密钥进行加密证明，从而创建更改历史记录。因此，身份是由标识符和关联的签名更改历史记录定义的。具体构造如图1所示。
Figure 1: Ockam Identities
图 1：奥卡姆恒等式
Primary keys are not used directly for authentication or session key establishment in the Noise protocol. Rather, they are used to attest to purpose keys used for secure channel establishment and credential issuance. These credentials play a role akin to certificates in traditional PKI systems to enable mutual trust and enforce attribute-based access control policies.
主密钥不直接用于噪声协议中的身份验证或会话密钥建立。相反，它们用于证明用于安全通道建立和凭证颁发的目的密钥。这些凭证的作用类似于传统 PKI 系统中的证书，以实现相互信任并强制执行基于属性的访问控制策略。
The manual assessment process
人工评估流程
We conducted a manual review of the Ockam design specification, including the secure channels, routing and transports, identities, and credentials, focusing on potential cryptographic threats that we see in similar communication protocols. The manual review process identified five issues, mostly related to the insufficient documentation for assumptions and the expected security guarantees. These findings indicate that insufficient information in the specifications, such as threat modeling, may lead Ockam users to make security-critical decisions based on an incomplete understanding of the protocol.
我们对 Ockam 设计规范进行了手动审查，包括安全通道、路由和传输、身份和凭证，重点关注我们在类似通信协议中看到的潜在加密威胁。手动审查过程发现了五个问题，主要与假设和预期安全保证的文件不足有关。这些发现表明，规范中的信息不足（例如威胁建模）可能会导致 Ockam 用户基于对协议的不完整理解而做出安全关键决策。
We also raised a few issues related to discrepancies between the specifications and the implementation that we identified from a cursory review of the implementation. Even though the implementation was not in scope for this review, we often find that it serves as a ground truth in cases when the design documentation is unclear and can be interpreted in different ways.
我们还提出了一些与规范和实施之间的差异有关的问题，这些问题是我们通过对实施的粗略审查发现的。尽管实现不在本次审查的范围内，但我们经常发现，在设计文档不清楚并且可以以不同方式解释的情况下，它可以作为基本事实。
Formal verification with Verifpal and CryptoVerif
使用 Verifpal 和 CryptoVerif 进行形式验证
In addition to reviewing the Ockam design manually, we used formal modeling tools to verify specific security properties automatically. Our formal modeling efforts primarily focused on Ockam Identities, a critical element of the Ockam system. To achieve comprehensive automated analysis, we used the protocol analyzers Verifpal and CryptoVerif.
除了手动审查 Ockam 设计之外，我们还使用正式建模工具自动验证特定的安全属性。我们的正式建模工作主要集中在奥卡姆恒等式上，这是奥卡姆系统的关键要素。为了实现全面的自动化分析，我们使用了协议分析器 Verifpal 和 CryptoVerif。
Verifpal works in the symbolic model, whereas CryptoVerif works in the computational model, making them a complementary set of tools. Verifpal finds potential high-level attacks against protocols, enabling quick iterations on a protocol until a secure design is found, while CryptoVerif provides more low-level analysis and can more precisely relate the security of the protocol to the cryptographic security guarantees of the individual primitives used in the implementation.
Verifpal 在符号模型中工作，而 CryptoVerif 在计算模型中工作，使它们成为一组互补的工具。 Verifpal 发现针对协议的潜在高级攻击，从而能够快速迭代协议，直到找到安全设计，而 CryptoVerif 提供更底层的分析，并且可以更精确地将协议的安全性与各个原语的加密安全保证联系起来在实施中使用。
Using Verifpal’s convenient modeling capabilities and built-in primitives, we modeled a (simplified) scenario for Ockam Identities where Alice proves to Bob that she owns the primary key associated with the peer identifier Bob is currently trying to verify. We also modeled a scenario where Bob verifies a new change initiated by Alice.
使用 Verifpal 方便的建模功能和内置原语，我们为 Ockam 恒等式建模了一个（简化的）场景，其中 Alice 向 Bob 证明她拥有与 Bob 当前尝试验证的对等标识符关联的主密钥。我们还模拟了一个场景，其中 Bob 验证 Alice 发起的新更改。
Modeling the protocol using Verifpal shows that the design of Ockam Identities achieves the expected security guarantees. For a given identifier, only the primary key holder may produce a valid initial change block that binds the public key to the identifier. Any subsequent changes are guaranteed to be generated by an entity holding the previous and current primary keys. Despite the ease of modeling, proving security guarantees with Verifpal requires a few tricks to prevent the tool from identifying trivial or invalid attacks. We discuss these considerations in our comprehensive report.
使用 Verifpal 对协议进行建模表明 Ockam 恒等式的设计实现了预期的安全保证。对于给定的标识符，只有主密钥持有者可以生成将公钥绑定到标识符的有效初始更改块。任何后续更改都保证由持有先前和当前主键的实体生成。尽管建模很容易，但使用 Verifpal 证明安全保证需要一些技巧来防止该工具识别微不足道或无效的攻击。我们在综合报告中讨论了这些考虑因素。
The current implementation of Ockam Identities can be instantiated with either of two signature schemes, ECDSA or Ed25519, which have different security properties. CryptoVerif highlighted that ECDSA and Ed25519 will not necessarily provide the same security guarantees, depending on what is expected from the protocol. However, this is not explicitly mentioned in the documentation.
Ockam 恒等式的当前实现可以使用两种签名方案（ECDSA 或 Ed25519）中的任意一种进行实例化，这两种签名方案具有不同的安全属性。 CryptoVerif 强调，ECDSA 和 Ed25519 不一定提供相同的安全保证，具体取决于协议的预期。但是，文档中没有明确提及这一点。
Ed25519 is the preferred scheme, but ECDSA is also accepted because it is currently supported by the majority of cloud hardware security modules (HSMs). For the current design of Ockam Identities, ECDSA and Ed25519 theoretically offer the same guarantees. However, future changes to Ockam Identities may require other security guarantees that are provided only by Ed25519.
Ed25519 是首选方案，但 ECDSA 也被接受，因为它目前受到大多数云硬件安全模块 (HSM) 的支持。对于奥卡姆恒等式的当前设计，ECDSA 和 Ed25519 理论上提供相同的保证。然而，未来对奥卡姆恒等式的更改可能需要仅由 Ed25519 提供的其他安全保证。
Occasionally, protocols require stronger properties than what is usually expected from the signature schemes’ properties (see Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures). Therefore, from a design perspective, it is desirable that properties expected from a protocol’s building blocks be well understood and explicitly stated.
有时，协议需要比签名方案属性通常预期更强的属性（请参阅看似合法：对使用签名的协议的微妙攻击的自动分析）。因此，从设计的角度来看，希望协议构建块所期望的属性能够得到很好的理解和明确的说明。
Our recommendations for strengthening Ockam
我们对加强奥卡姆的建议
Our review did not uncover any issues in the in-scope use cases that would pose an immediate risk to the confidentiality and integrity of data handled by Ockam. But we made several recommendations to strengthen the security of Ockam’s protocols. Our recommendations aim at enabling defense in depth, future-proofing the protocols, improving threat modeling, expanding documentation, and clearly defining the security guarantees of Ockam’s protocols. For example, one of our recommendations describes important considerations for protecting against “store now, decrypt later” attacks from future quantum computers.
我们的审查没有发现范围内用例中的任何问题，这些问题会对 Ockam 处理的数据的机密性和完整性构成直接风险。但我们提出了几项建议来加强奥卡姆协议的安全性。我们的建议旨在实现深度防御、面向未来的协议、改进威胁建模、扩展文档以及明确定义 Ockam 协议的安全保证。例如，我们的一项建议描述了防止未来量子计算机“立即存储，稍后解密”攻击的重要考虑因素。
We also worked with the Ockam team to flesh out information missing from the specification, such as documenting the exact meaning of certain primary key fields and creating a formal threat model. This information is important to allow Ockam users to make sound decisions when deploying Ockam’s protocols.
我们还与 Ockam 团队合作，充实规范中缺失的信息，例如记录某些主要关键字段的确切含义并创建正式的威胁模型。这些信息对于让 Ockam 用户在部署 Ockam 协议时做出明智的决策非常重要。
Generally, we recommended that Ockam explicitly document the assumptions made about cryptographic protocols and the expected security guarantees of each component of the Ockam system. Doing so will ensure that future development of the protocols builds upon well-understood and explicit assumptions. Good examples of assumptions and expected security guarantees that should be documented are the theoretical issue around ECDSA vs. EdDSA that we identified with CryptoVerif and how using primitives with lower security margins will not significantly impact security.
一般来说，我们建议 Ockam 明确记录有关加密协议的假设以及 Ockam 系统每个组件的预期安全保证。这样做将确保协议的未来开发建立在易于理解和明确的假设之上。应该记录的假设和预期安全保证的好例子是我们通过 CryptoVerif 确定的围绕 ECDSA 与 EdDSA 的理论问题，以及使用安全裕度较低的原语如何不会显着影响安全性。
Ockam’s CTO responded to the above recommendations with the following statement:
Ockam的CTO针对上述建议做出了如下回应：
We believe that easy to understand and open documentation of Ockam’s protocols and implementation is essential to continuously improve the security and privacy offered by our products. Trail of Bits’ thorough third-party review of our protocol documentation and formal modeling of our protocols has helped make our documentation much more approachable for continuous scrutiny and improvement by our open source community.
我们相信，易于理解且开放的 Ockam 协议和实施文档对于不断提高我们产品提供的安全性和隐私性至关重要。 Trail of Bits 对我们的协议文档和协议的正式建模进行了彻底的第三方审查，这有助于使我们的文档更容易接受开源社区的持续审查和改进。
Lastly, we strongly recommended an (internal or external) assessment of the Ockam protocols implementation, as a secure design does not imply a secure implementation. Issues in the deployment of a protocol may arise from discrepancies between the design and the implementation, or from specific implementation choices that violate the assumptions in the design.
最后，我们强烈建议对 Ockam 协议实施进行（内部或外部）评估，因为安全设计并不意味着安全实施。协议部署中的问题可能源于设计和实现之间的差异，或者源于违反设计假设的特定实现选择。
Security is an ongoing process
安全是一个持续的过程
At the start of the assessment, we observed that the Ockam design follows best practices, such as using robust primitives that are well accepted in the industry (e.g., the Noise XX protocol with AES-GCM and ChachaPoly1305 as AEADs and with Ed25519 and ECDSA for signatures). Furthermore, the design reflects that Ockam considered many aspects of the system’s security and reliability, including, for instance, various relevant threat models and the root of trust for identities. Moreover, by open-sourcing its implementation and publishing the assessment result, the Ockam team creates a transparent environment and invites further scrutiny from the community.
在评估开始时，我们观察到 Ockam 设计遵循最佳实践，例如使用业界广泛接受的稳健原语（例如，使用 AES-GCM 和 ChachaPoly1305 作为 AEAD 的 Noise XX 协议，以及使用 Ed25519 和 ECDSA 作为 AEAD）。签名）。此外，该设计反映出奥卡姆考虑了系统安全性和可靠性的许多方面，包括各种相关威胁模型和身份信任根等。此外，通过开源其实施并公布评估结果，Ockam团队创造了一个透明的环境，并邀请社区进一步审查。
Our review identified some areas for improvement, and we provided recommendations to strengthen the security of the product, which already stands on a good foundation. You can find more detailed information about the assessment, our findings, and our recommendations in the comprehensive report.
我们的审查确定了一些需要改进的领域，并提供了加强产品安全性的建议，这已经奠定了良好的基础。您可以在综合报告中找到有关评估、我们的调查结果和建议的更多详细信息。
This project also demonstrates that security is an ongoing process, and including security considerations early in the design phase establishes a strong footing that the implementation can safely rely on. But it is always necessary to continuously work on improving the system’s security posture while responding adequately to newer threats. Assessing the design and the implementation are two of the most crucial steps in ensuring a system’s security.
该项目还表明，安全性是一个持续的过程，在设计阶段的早期就考虑安全性，为实施奠定了可以安全依赖的坚实基础。但始终有必要不断努力改善系统的安全状况，同时充分应对新的威胁。评估设计和实施是确保系统安全的两个最关键的步骤。
Please contact us if you want to work with our cryptography team to help improve your design—we’d love to work with you!
如果您想与我们的密码学团队合作来帮助改进您的设计，请联系我们 – 我们很乐意与您合作！
原文始发于Marc Ilunga, Jim Miller, Fredrik Dahlgren, and Joop van de Pol：Cryptographic design review of Ockam
相关文章
