A Comprehensive Formal Security Analysis of OPC UA

OPC UA is a standardized Industrial Control System (ICS) protocol, deployed in critical infrastructures, that aims to ensure security. The forthcoming version 1.05 includes major changes in the underlying cryptographic design, including a Diffie-Hellmann based key exchange, as opposed to the previous RSA based version. Version 1.05 is supposed to offer stronger security, including Perfect Forward Secrecy (PFS). We perform a formal security analysis of the security protocols specified in OPC UA v1.05 and v1.04, for the RSA-based and the new DH-based mode, using the state-of-the-art symbolic protocol verifier ProVerif. Compared to previous studies, our model is much more comprehensive, including the new protocol version, combination of the different sub-protocols for establishing secure channels, sessions and their management, covering a large range of possible configurations. This results in one of the largest models ever studied in ProVerif raising many challenges related to its verification mainly due to the complexity of the state machine. We discuss how we mitigated this complexity to obtain meaningful analysis results. Our analysis uncovered several new vulnerabilities, that have been reported to and acknowledged by the OPC Foundation. We designed and proposed provably secure fixes, most of which are included in the upcoming version of the standard. We analyze OPC UA using ProVerif. Given the size and the complexity of our model, and the large number of possible configurations, we provide tooling (Section 4.2) that allows to (i) generate ProVerif models for a particular set of configurations, and threat model; (ii) efficiently explore the lattice of configurations and threat models, and automatically find maximal configurations in which a property holds, as well as minimal configurations in which we find attacks (or reach the limits of ProVerif). Moreover, we used many advanced features of ProVerif [7] to fine tune the model and guide the proof search, to be able to conclude in complex configurations (Section 4.3). We believe that this is among the most complex analyses performed with ProVerif, both due to the size of the model as well as the complexity of the state machine, e.g., the model requires a lot of information to be stored in a global state. To the best of our knowledge, it is the largest ProVerif model in terms of LoC and initial clauses (the internal protocol representation on which ProVerif reasons) ever analyzed. Our analysis allowed to discover 8 new vulnerabilities and other weaknesses in OPC UA v1.05 (Section 5), 6 of these also affect v1.04. Each of these have been responsibly disclosed to and acknowledged by the OPC UA Foundation. We proposed provably secure fixes and other mitigations, most of them are now included in the specification. Finally, we draw more general lessons for the future of OPC UA (Section 5.7). Artifacts. All models, results, and instructions to reproduce them are provided in the companion artifact [17] . OPC UA Protocol Overview We start by presenting the OPC UA protocol version 1.05.03 with a high-level overview of the sub-protocols and their interactions. In this work, we cover the security sub-protocols, namely the secure channel and the session sub-protocols. They are specified in the OPC UA standard, mostly in [26, Parts 4, 6, 7] . They involve three kinds of agents: clients (e.g., user workstations), servers (e.g., SCADA), and users (e.g., humans operating user workstations). Each agent is assumed to be enrolled in a Public Key Infrastructure (PKI) and possesses a certificate that describes its identity and role (e.g., a client certificate 𝐶 cert ) with the associated private key (e.g., 𝐶 sk ); users store them on a smart card or may alternatively use a login password pair. The main flow is depicted in Fig. 1 : a client opens a secure communication channel with a server and creates a session inside this channel. A user on this client can then log in, i.e., activate a previously created session, and use this session to send/receive requests to/from the server. We now briefly present those sub-protocols. User: 𝑈 + (𝑈 pwd | (𝑈 cert ,𝑈 sk )) Client: 𝐶 cert , 𝐶 sk Server: 𝑆 cert , 𝑆 sk OpenChannel (RSA | ECC + Enc | Sign | None) 𝑖𝑑 𝑐 , sk 𝑖𝑑 𝑐 , sk ‖CreateSession(𝑖𝑑 𝑠 , 𝑡𝑜𝑘 𝑠 )‖ 𝑖𝑑 𝑐 ,sk (SSec | SNoAA) 𝑖𝑑 𝑐 , sk, 𝑖𝑑 𝑠 𝑖𝑑 𝑐 , sk, 𝑖𝑑 𝑠 ‖ActivateSession(𝑖𝑑 𝑠 , 𝑡𝑜𝑘 𝑠 , U)‖ 𝑖𝑑 𝑐 ,sk