By Marc Ilunga, Jim Miller, Fredrik Dahlgren, and Joop van de Pol

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.

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:

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.

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:

1. TCP portals: secure TCP communication spanning various networks and traversing NATs
2. Kafka portals: secure data streaming through 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).

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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’s CTO responded to the above recommendations with the following statement:

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.

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.

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.

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!

*** This is a Security Bloggers Network syndicated blog from Trail of Bits Blog authored by Trail of Bits. Read the original post at: https://blog.trailofbits.com/2024/03/05/cryptographic-design-review-of-ockam/