A Comprehensive Formal Security Analysis of OPC UA

A Comprehensive Formal Security Analysis of OPC UA

Speakers: Vincent Diemunsch, Engineer, French Cyber Security Agency; Lukayashi, Researcher, INRIA; Steve Kramer, Researcher, INRIA

Conference: USENIX Security

YouTube: https://www.youtube.com/watch?v=_PyngibbWC8

Overview

This talk presents a rigorous formal security analysis of OPC Unified Architecture (OPC UA), a critical industrial control system (ICS) protocol. Delivered by Vincent Diemunsch from the French Cyber Security Agency, in collaboration with Lukayashi and Steve Kramer from INRIA, the research delves into the protocol's built-in security mechanisms. OPC UA is widely deployed in safety-critical infrastructures such as nuclear power plants, power grids, air traffic control, and oil and gas installations, making its security paramount.

The core objective of this work was to ascertain the robustness of OPC UA's message authentication and confidentiality properties, particularly when faced with an active attacker on the industrial network who may have compromised long-term cryptographic keys. Given the protocol's complexity, encompassing features like secure channel key renewal, session reactivation, and channel switching, a comprehensive formal verification was deemed essential to identify potential vulnerabilities that could undermine its integrity and confidentiality in highly sensitive environments.

The findings from this extensive analysis include the discovery of five new attacks and three weaknesses within OPC UA version 1.4/1.5. These vulnerabilities were responsibly disclosed to the OPC Foundation, leading to their acknowledgment and subsequent remediation in the latest specifications. This research not only contributes to the security of critical infrastructure but also introduces a novel methodology for applying formal verification tools like ProVerif to highly complex, real-world protocols.

Background

▶ Watch: Introduction to OPC UA and its critical role (0:00)

OPC UA (IEC 62,541 version 1.4) is a data exchange standard for industrial automation, designed to enable secure and reliable communication between diverse devices, from client workstations in control rooms to SCADA servers and programmable logic controllers (PLCs). Its inherent security features, including built-in cryptography and Public Key Infrastructure (PKI) reliance, often lead government cybersecurity agencies to recommend it for critical infrastructure.

Prior to this work, existing security analyses of OPC UA were either informal or partial. The German BSI (Bundesamt für Sicherheit in der Informationstechnik) released a security analysis in 2022, but it was not a formal verification. Two earlier formal analyses of OPC UA version 1.3 focused on specific, isolated aspects of the protocol. One, using the ProVerif tool, examined only the establishment of secure channel symmetric keys in RSA cryptography. The other, utilizing the Tamarind tool, proved flow integrity properties of secure channels but notably excluded key establishment processes. These prior efforts, while valuable, did not encompass the full complexity of OPC UA, specifically lacking analysis of user sessions, the newer elliptic curve cryptography (ECC), or the intricate state machine transitions like channel renewal and session handover. This gap highlighted the need for a comprehensive, version 1.4/1.5 analysis that considered the protocol's full feature set and potential long-term key compromises.

Key Findings

▶ Watch: Challenges of OPC UA protocol state machine complexity (3:05)

The research yielded significant contributions to the understanding and improvement of OPC UA security. The primary findings include:

• Comprehensive Formal Model: Development of a formal model for OPC UA version 1.4/1.5, incorporating user sessions and supporting both RSA and the newer elliptic curve cryptography (ECC). This model is noted as "one of the largest ProVerif models ever studied," comprising 8,600 lines of applied pi calculus and generating approximately 2,300 initial horn clauses.
• Automated Proofs and Novel Methodology: Implementation of automated proofs of security properties using ProVerif. Due to the protocol's complexity, a novel proof methodology was devised. This involved identifying and breaking resolution loops with added constraints and providing necessary information through over 100 lemmas, which were subsequently proven separately. This methodology ensured the termination and soundness of the verification process.
• Discovery of New Vulnerabilities: Identification of five new attacks and three weaknesses in OPC UA. These vulnerabilities were responsibly disclosed to the OPC Foundation through detailed vulnerability reports, tickets, and direct meetings with their security group.
• Protocol Remediation: The OPC Foundation acknowledged the disclosed vulnerabilities and has since implemented fixes in the latest release version of the OPC UA specifications.
• Partial Security Proofs: The research successfully proved security properties for many configurations unaffected by the discovered attacks, including injective agreement between client and server upon user requests and responses, and perfect forward secrecy of secure channel keys in elliptic curve cryptography. However, the full proof of the new security fixes proposed by the OPC Foundation for all configurations remains an ongoing task.

Technical Deep Dive

▶ Watch: Introduction to ProVerif and its inherent limitations (5:00)

The OPC UA protocol's architecture is built around a client-server model where agents, including users, clients, and servers, possess certificates issued from a PKI and their corresponding private keys. The communication sequence begins with a secure channel establishment. The client initiates this by opening a secure channel with the server, whose primary purpose is to guarantee message integrity and optionally confidentiality against an active network attacker. Within this "open channel" sub-protocol, symmetric keys (SK) are derived for the secure channel, identified by a unique channel ID (IDC). These SKs are crucial for generating message authentication codes (MACs) and for encryption.

Following secure channel establishment, the client proceeds to create a session on the server. The "create session" sub-protocol transits within the established secure channel (IDC) and is therefore protected by the symmetric keys (SK), ensuring its integrity. The server responds by providing a new session authentication token, which the client subsequently uses to identify the session in all future requests. The final step involves the user activating the session by logging in. This involves the client sending an "active session" request through the secure channel, identifying the session with the token, and crucially, including a signature of the user computed with the user's private key. Once activated, all subsequent requests sent via that secure channel with the specific session authentication token are associated with that authenticated user.

The complexity of OPC UA's state machine arises from several dynamic features:

1. Secure Channel Key Renewal: Secure channels periodically renew their symmetric keys, a process that effectively involves "reopening" the channel.
2. Session Reactivation: Sessions can be reactivated by different users, a common requirement for operational handover during shift changes.
3. Secure Channel Switching: A session can switch from one secure channel to another, enhancing reliability by mitigating the loss of an existing channel.

To formally analyze this intricate protocol, the researchers utilized ProVerif, a cryptographic protocol verifier developed at INRIA, which operates within the symbolic model. In this model, the protocol is specified as parallel processes using applied pi calculus. Messages are represented as terms constructed with functions and atoms. For instance, a nonce might be encrypted with a server's public key and transmitted alongside a client's certificate, signed by the client's private key. The attacker model adheres to the Dolev-Yao model, meaning an attacker can intercept, analyze, and forge messages based on known terms, but cannot break cryptographic primitives (e.g., cannot derive a private key from its hash). ProVerif uses idealized cryptography, where encryption and decryption operations are perfectly modeled.

Despite being a state-of-the-art verifier, ProVerif has inherent limitations. The general verification problem is undecidable, meaning the tool might not terminate or might conclude inconclusively. This challenge was particularly acute for OPC UA, resulting in "one of the largest ProVerif models ever studied." The unfolded process generated by the solver after parsing amounted to 8,600 lines of code in applied pi calculus, with about 2,300 initial horn clauses—figures significantly higher than, for example, the TLS 1.3 model presented at CCS 2022.

To manage this complexity, the team initially adopted a modular approach. The model's various parts were activated via a configuration mechanism. This allowed selection of:

• Cryptography: RSA or elliptic curves.
• Channel security mode: Message integrity only, or both integrity and confidentiality.
• Supported user credentials: Login/password or certificates.
• Level of session security.
• Attacker capabilities: No key compromises or only long-term key compromises.
• Simplifications: Disabling demanding features like channel reopening and channel switching.

This modularity resulted in 756 distinct possible configurations. An iterative approach using Python scripts was employed to explore these configurations, organizing them into a lattice of configurations based on a partial order. A proof on a weaker configuration holds for all inferior ones, while an attack on a configuration applies to all superior ones. However, even with highly parallelized exploration and iterative time delays, non-termination remained a significant issue due to the protocol's complex state machine.

This necessitated a new proof methodology:

1. Identify Main Loops: Pinpoint the recurring loops that cause non-termination during resolution.
2. Break Loops with Hints: Introduce proof hints that redefine ProVerif's selection function, guiding the proof search to break these loops. Initially, this often led to inconclusive results because ProVerif could not trace the origin of certain terms.
3. Iteratively Add Lemmas: Introduce over 100 lemmas to provide the necessary information for ProVerif to conclude. These lemmas were initially assumed as "axioms" during the main query resolution.
4. Prove Lemmas Separately: Each lemma was then proven as a separate query under the same configuration but with different proof hints. This multi-stage process preserved the soundness of the results; if ProVerif concluded a query was true, it genuinely meant no attack existed. This innovative methodology was crucial for achieving termination and obtaining conclusive results for many configurations.

Demo / Proof of Concept

▶ Watch: Novel proof methodology to overcome ProVerif limitations (7:20)

While the talk did not feature a live, interactive demonstration, it effectively illustrated one of the most striking attacks discovered: a session hijack by reopening a secure channel in sign mode. This example serves as a clear proof of concept for the identified vulnerabilities.

The threat model for this attack assumes an active attacker on the network who has compromised the client's long-term certificate, specifically possessing its associated private key.

The attack unfolds as follows:

1. Initial Secure Channel and Session Setup: A legitimate client opens a secure channel with the server in "sign mode," meaning it guarantees message integrity but not confidentiality. The client then creates a session, which is subsequently activated by the legitimate user. During this process, the session authentication token is transmitted, and because the channel lacks confidentiality, this token becomes publicly known to the attacker.
2. Attacker Initiates Channel Renewal: The attacker, having compromised the client's certificate and private key, is able to initiate the renewal of the secure channel's symmetric keys. Crucially, the server does not require proof of knowledge of the previous symmetric keys during this renewal process. This design flaw allows the attacker to successfully establish a new set of symmetric keys for the secure channel, effectively impersonating the client for the channel renewal.
3. Session Hijack: At this point, the attacker possesses control over the renewed secure channel and knows the publicly available session authentication token. The attacker can then send any request to the server through this channel, simply by including the known session authentication token.
4. Impact: The server receives the request, believing it originates from the legitimate user on the client machine, even though it was sent by the attacker. This constitutes a major authentication violation, as the attacker has successfully hijacked the active user session.

The root causes of this attack are two critical design flaws:

1. Lack of Binding During Channel Renewal: There is no cryptographic binding between the channel keys before and after a renewal. This allows an attacker to impersonate the client during the renewal process, even if they never knew the original symmetric keys used when the session was created or activated.
2. Absence of Session Ownership Proof: The protocol lacks a mechanism for the client to prove ownership of the session beyond merely presenting the session authentication token. Since the secure channel was configured without confidentiality, the session authentication token was public. This allowed the attacker to use the token to send requests, leading the server to mistakenly attribute them to the legitimate user.

This detailed attack trace, along with others, was provided to the OPC Foundation, highlighting the practical security impact and underlying design flaws, which were largely attributed to a "lack of binding between sessions and secure channel" and "lack of authentication secrets."

Defensive Implications

▶ Watch: Modular approach and 756 configurations for analysis (9:00)

The detailed formal analysis of OPC UA, coupled with the responsible disclosure of five new attacks and three weaknesses, carries significant defensive implications for organizations utilizing or implementing this critical ICS protocol. The most immediate and crucial recommendation is to prioritize updating to the latest versions of the OPC UA specifications and their corresponding implementations. The OPC Foundation has acknowledged the reported vulnerabilities and has implemented fixes in the latest releases, specifically addressing the design flaws identified by this research.

Defenders should pay particular attention to the secure channel configuration. The demonstrated session hijack attack highlights the severe consequences of operating secure channels in "sign mode" (integrity only) without confidentiality. While integrity protection is vital, the lack of encryption for the session authentication token allowed the attacker to easily obtain it and subsequently hijack the session. Therefore, where possible, OPC UA deployments should enforce confidentiality for all secure channels, especially those involving session establishment and activation, to protect sensitive tokens and prevent their public exposure.

Furthermore, the root causes of many attacks pointed to a "lack of binding between sessions and secure channel" and a "lack of authentication secrets" during key renewal processes. Implementers of OPC UA products must ensure their solutions strictly adhere to the updated specifications, which are expected to introduce stronger cryptographic bindings between session and channel states and require more robust authentication during key and channel renewals. This includes verifying that servers properly validate proof of knowledge of previous keys or session ownership before accepting channel renewals or processing session-associated requests.

Finally, while this research focused on long-term key compromises, it underscores the broader importance of robust key management practices within ICS environments. Protecting client certificates and private keys from compromise is fundamental, as even with protocol fixes, a compromised long-term key significantly elevates an attacker's capabilities. Regular security audits, penetration testing, and adherence to security best practices for credential management remain essential layers of defense against sophisticated adversaries targeting critical infrastructure.

Key Takeaways

• OPC UA Complexity Demands Formal Analysis: OPC UA, a critical protocol for industrial control systems, possesses a highly complex state machine with features like channel renewal and session switching, necessitating rigorous formal security analysis beyond traditional methods.
• Novel Methodology for Large-Scale Verification: The research developed and applied an innovative ProVerif methodology, involving loop breaking with hints and extensive lemma proving, to successfully analyze one of the largest and most complex protocol models ever studied with the tool.
• Discovery of Critical Vulnerabilities: Five new attacks and three weaknesses were identified in OPC UA version 1.4/1.5, including a significant session hijack vulnerability, and responsibly disclosed to the OPC Foundation.
• Protocol Remediation Underway: The OPC Foundation acknowledged the vulnerabilities and has implemented fixes in the latest specifications, addressing issues related to insufficient binding between sessions and secure channels, and lack of authentication during key renewal.
• Importance of Confidentiality and Updates: Defenders using OPC UA should prioritize updating to the latest, patched versions of the protocol specifications and implementations, and enforce confidentiality for secure channels to protect session tokens and other sensitive information.
• Partial Proofs Achieved, More Work Ahead: While security properties were proven for many configurations, the full formal verification of the OPC Foundation's proposed fixes for all configurations remains an ongoing effort.

About the Speaker(s)

Vincent Diemunsch is an engineer who conducted this formal security analysis while working for the French Cyber Security Agency. His work focuses on the security of critical industrial control system protocols.

Lukayashi and Steve Kramer are researchers at INRIA, the French National Institute for Research in Digital Science and Technology. They collaborated with Vincent Diemunsch on this project, contributing their expertise in formal verification and cryptographic protocol analysis.