PhD studentship on Automated Black-box Verification of Networking Systems at University College London

Applications are invited for a PhD studentship at University College London,
under the supervision of Prof. Alexandra Silva and Dr. Matteo Sammartino.

The start date is flexible and can be negotiated. It should be in September 2018 at the latest.


The studentship is funded by the UK Research Institute in Verified Trustworthy
Software Systems, and will be conducted within the Programming Principles, Logic
and Verification (PPLV) group (http://pplv.cs.ucl.ac.uk/).

Computer Science at UCL was ranked among the top 20 in the world and fifth in the UK.
The PPLV group provides an exciting research environment, with outstanding connections
with cutting-edge industry.



Potential applicants are encouraged to contact Prof. Silva (alexandra.silva@ucl.ac.uk) and
Dr. Sammartino (m.sammartino@ucl.ac.uk) for further information and expressions of interest.


Applications should be made via the UCL evision website:

https://evision.ucl.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app&code1=RRDCOMSING01&code2=0025



Here is a short description of the project.


Title: Automated Black-box Verification of Networking Systems


Our society is increasingly reliant on complex networking systems, consisting of several
components that operate in a distributed/concurrent fashion, exchange data that may be
highly sensitive, and are implemented with a mix of open and closed-source code.
Examples are Software Defined Networks, cloud computing systems, Internet of Things
and others.

As the complexity of these systems increases, there is a pressing need of methods and
tools to automatically verify security and privacy properties. High quality models – able
to express all the behaviours of interest – are of paramount importance to this aim.
However, it is often the case that the task of building a model is performed by humans
and in a short span of time – if it is performed at all – and as such can be error-prone and
inaccurate.

The goal of the proposed PhD project is to develop techniques and tools to automate the
modelling and verification of networking software systems. The novel idea is to rely on the
model learning paradigm, originally proposed in artificial intelligence, to automatically build
an automaton model of a running system in a black-box fashion -- purely via interactions with
the running system.