Reverse-engineering systems to identify security flaws and understand behaviour

这个博士学位将考虑如何从基于Erlang的底层系统中逆向工程模型，特别强调安全问题。Erlang和安全性Erlang不是为敌对环境设计的，而是为受防火墙保护的内部网络设计的。虽然这个假设对于Erlang的领域仍然有效，但Erlang的使用已经转向提供广泛访问的在线服务，其中更有可能出现安全线程。今天，利用一个安全漏洞，危及一个单一的Erlang节点自动危及所有。如果两个Erlang节点相连，没有什么是一个节点不能在另一个节点上做的。这个博士专注于开发技术（和工具）来检测现有Erlang代码中的安全线程。分布式系统和EFSM。有限状态机推理已非常成功地用于分析测试集和生成测试集的一般系统测试。然而，FSM模型不包含数据，无论是作为操作参数，还是作为在系统状态中存储信息的有限性较低的方式。EFSM包括数据参数和数据寄存器，允许事件包括对影响控制流决策的数据的保护，并在结果和输出的计算中包括数据值。有大量的工作集中在EFSM推断上，然而这些技术通常只是包括所有可用的数据，并且需要过于复杂或过于一般的推断表达式来解释与感兴趣的属性不直接相关的数据。在以前的工作中，已经针对安全属性测试，目的是抽象出尽可能多的数据，以便能够验证感兴趣的安全属性。在这个博士论文中，我们专注于推断分布式系统的EFSM，以产生包括数据流和使用的模型。这将利用该部门开发的推理技术。该博士将开发用于表达安全属性的语言和语法，然后将其应用于从工业案例研究中构建的模型。

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.