Security analysis of systems using emerging 5G technologies (5GTech-Sec)

5GTech-Sec will undertake the formal security and privacy analysis of 5G-systems against 5G-specific security and privacy risks e.g. threats stemming from reconfigurable networks, the arbitrary number of connections to a small cell etc. In other words, this a project to develop formal models, verification mechanisms and tools that are suited for the verification of 5G systems.
Start date
Ongoing
Duration
3.5 years
Application deadline
Ongoing
Funding information

This research project has funding attached. Funding for this project is available to UK citizens only, and includes a £22,000 per annum, tax-free stipend.

Applications accepted all year round.

About

The 5G systems will be arbitrarily large, and they will introduce new designs, elements, paradigms compared to their 4G counterparts. What is more, one core aspect that is set to change in 5G vs 4G is the way in which privacy is provisioned. Some formal security analysis of security and privacy of 5G specifications have already started. Continuing on this trend but also complementary to it, in this work, we will look at developing threat-models, verification methodologies and tools that are bespoke to 5G systems and their arbitrary sizes and lend themselves particularly well to analysing privacy properties.

We can summarise the 5GTech-Sec quests here as follows:

  1. What are the main threat-and security-models suited to 5G systems, accounting for 5G-specific architectures and designs, including the introduction of small cells (including pico-cells, femto-cells and the general infrastructure for heterogeneous networks)?
  2. How do the different 5G architectures (e.g., flat vs. hierarchical), different communication-primitives (e.g. broadcast vs. focused beams) and the changing topologies induced by the positioning of 5G’s small cells (jointly) influence the formal analysis of 5G systems w.r.t. security and privacy properties? How do the arbitrary numbers of pseudo-arbitrarily positioned small cells and how do focused beams influence 5G attacks and their analysis, when applicable?

Main research challenge

5GTech-Sec envisages tackling the advancement of new automated-verification theories and tools, based on non-classical logics, for the analysis of privacy and security in arbitrarily-large/unbounded-size 5G systems, where the 5G-specific designs, such as the topologies in which the SCs are placed, are considered within new 5G-suited threat-models and analyses.

Indeed, this project focuses on the theory and practice of formal verification of 5G systems privacy through model checking using non-classical logics.

The team

The research in 5GTech-Sec is supported by the UK Government and it is in partnership with BT.

The student will join a team of researchers at Surrey University’s Centre for Cyber Security (SCCS), supervised by Dr Ioana Boureanu, in collaboration with Prof. Zhili Sun at the 5GIC (5G Innovation Centre). The SCCS’ research interests include verification and provable security applicable to different secure systems, ranging from established cryptographic protocols to emerging ones, like those in the sphere of 5G. The 5GIC research interests include mobile networks, and particularly the 5G, from infrastructure to design to security thereof.

Eligibility criteria

Required

  • Bachelor degree in Computer Science (UK equivalent 1st classification)
  • Interest in verification techniques (e.g. formal methods/analysis, logics) and/or in security and privacy
  • Programming experience (any language)
  • Analytical skills: knowledge of foundations of computer science (e.g., discrete mathematics); ability to think independently
  • Strong verbal and written communication skills, both in plain English (see http://www.plainenglish.co.uk), and scientific language for publication in relevant journals and presentation at conferences.

Desirable

  • Masters degree (UK equivalent of Merit classification or above)
  • Experience in Boolean logic, and first order logic, or other specific logics
  • Experience in formal verification (model checking, theorem proving or SMT solving)
  • Experience of implementation and/or experimentation with verification tools
  • Knowledge of cryptography and/or information security and/or networks
  • Proficiency in C++ and/or Java
  • Experience with a functional programming language (e.g., Haskell, Ocaml).

 

The research in 5GTech-Sec is supported by the UK Government and it is in partnership with BT.

The student will join a team of researchers at Surrey University’s Centre for Cyber Security (SCCS), supervised by Dr Ioana Boureanu, in collaboration with Prof. Zhili Sun at the 5GIC (5G Innovation Centre). The SCCS’ research interests include verification and provable security applicable to different secure systems, ranging from established cryptographic protocols to emerging ones, like those in the sphere of 5G. The 5GIC research interests include mobile networks, and particularly the 5G, from infrastructure to design to security thereof.

How to apply

You can apply for this studentship by applying for the Computer Science PhD. You must mention this studentship in your application to be considered.

Computer Science PhD

Contact details

Ioana Boureanu (Carlson)
09 BB 02
Telephone: +44 (0)1483 683425
E-mail: i.boureanu@surrey.ac.uk

Studentships at Surrey

We have a wide range of studentship opportunities available.