[TYPES/announce] PhD studentship on Automated Black-box Verification of Networking Systems at University College London

[Sammartino, Matteo]

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 at ucl.ac.uk) and
Dr. Sammartino (m.sammartino at 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.