Security formal verification engine for OT infrastructures

The goal of this work is to address the need for cybersecurity solutions within the world of operational technology (OT). Specifically, this work describes the development of a part of the DIANA project, a plug and play tool capable of performing automatic scanning, validation and reporting of the status of security within an OT network, in a continuous monitoring cycle. Within the context of DIANA, this thesis focuses on the development of a formal verification engine that takes as input a network description, containing information about host and network configuration, topology, and potential vulnerabilities; and generates possible attack paths and sequences of tasks to be executed in order to test the actual exploitability of the system. The initial scanning phase, and the validation phase, characterized by the execution of planned tasks, are part of the DIANA project but are not included in the scope of this work. The computation of the attack paths is achieved by leveraging and extending MulVAL, a popular open source framework that allows to conduct multi-host and multi-stage vulnerability analysis through the use of attack graphs. The thesis is divided into six chapters being: introduction, background, state of the art, methodology, results and discussions, and conclusions. The first chapter contains an introduction to the DIANA project, it briefly addresses the goals and the need for such a project. The second chapter contains the thesis' background, it provides contextualization about the world of OT and described how cybersecurity relates to this field. Some examples of attacks against OT infrastructures are also given in this chapter. The third chapter discusses the state of the art. It starts by giving a brief theoretical overview of the architectural design of the project. It then proceeds to provide a detailed analysis of the existing literature and afterwards moves on to describe why the MulVAL framework was chosen as the best option for the job compared to others, how it works, and what are the limitations that this work will try to overcome. The fourth chapter discusses the methodology that has been used to build the formal verification engine. It describes the main steps such as how the input model was designed, how MulVAL was extended, how the attack graphs were pruned, and how the validation task models were designed and selected. The fifth chapter presents two test cases run on a test network configuration and showcases and discusses the obtained results. Lastly there is the conclusion chapter, containing final remarks about the project and how it could be expanded going forward. Following the conclusions chapter, an appendix section has been added for supplying some technical resources that are addressed throughout the thesis in order not to disrupt the flow of the reader.