Reverse-engineering systems to identify security flaws and understand behaviour

This PhD will consider how to reverse engineer models from underlying Erlang-based systems, with a particular emphasis on security questions. Erlang and security. Erlang is not conceived for a hostile environment, but rather for a firewall protected internal network. While this assumption is still valid for the domain where Erlang was conceived, the use of Erlang has been shifting to provide widely accessible online services, where security threads are more likely to occur. Today, exploiting a security vulnerability that compromises a single Erlang node automatically compromises them all. If two Erlang nodes are connected, there is nothing one node cannot do on the other one. This PhD focuses on developing techniques (and tools) to detect security threads in existing Erlang code. Distributed systems and EFSM. FSM inference has been used very successfully for both analysing test sets and for generating test sets for general system testing. However, FSM models do not contain data, either as parameters of operation, or as a less finite way to store information in the system state. EFSMs include data parameters and data registers that allow for events to include guards over the data that influence control flow decisions, and to include data values in the computation of results and outputs. There is a body of work focusing on EFSM inference, however these techniques often simply include all of the available data and require overly complex or overly general inferred expressions to account for data that is not directly relevant to the properties of interest. In previous work that has been directed at security property testing, the aim has been to abstract away as much data as need in order to be able to verify security properties of interest. In this PhD we focus on inferring EFSMs for distributed systems in order to produce models that include the flow and use of data. This will make use of the inference techniques developed in the department. This PhD will develop language and practises for expressing security properties and then will apply these to models built from industrial case studies.