Research projects
Find a postgraduate research project in your area of interest by exploring the research projects that we offer in the Department of Computer Science.
We have a broad range of research projects for which we are seeking doctoral students. Browse the list of projects on this page or follow the links below to find information on doctoral training opportunities, or applying for a postgraduate research programme.
Alternatively, if you would like to propose your own project then please include a research project proposal and the name of a possible supervisor with your application.
Available projects
Exploiting Software Vulnerabilities at Large Scale
Primary supervisor
Additional supervisors
- Giles Reger
Contact admissions office
Other projects with the same supervisor
- Application Level Verification of Solidity Smart Contracts
- Finding Vulnerabilities in IoT Software using Fuzzing, Symbolic Execution and Abstract Interpretation
- Designing Safe & Explainable Neural Models in NLP
- Verification Based Model Extraction Attack and Defence for Deep Neural Networks
- Using Program Synthesis for Program Repair in IoT Security
- Automated Repair of Deep Neural Networks
- Automatic Detection and Repair of Software Vulnerabilities in Unmanned Aerial Vehicles
- Combining Concolic Testing with Machine Learning to Find Software Vulnerabilities in the Internet of Things
- Verifying Cyber-attacks in CUDA Deep Neural Networks for Self-Driving Cars
- Hybrid Fuzzing Concurrent Software using Model Checking and Machine Learning
Funding
- Directly Funded Project (European/UK Students Only)
This research project has funding attached. Funding for this project is available to citizens of a number of European countries (including the UK). In most cases this will include all EU nationals. However full funding may not be available to all applicants and you should read the full department and project details for further information.
Project description
Currently, our software verification community faces a pressing problem to ensure security of Internet services that hold sensitive information from millions of users. Even minor defects can lead to huge impacts for companies and costumers; for instance, in September 2018, attackers exploited three Facebook vulnerabilities and stole access tokens from as many as 50 million users, in order to take over their accounts [1]. In this context, software verification plays an important role in ensuring the overall product reliability. Even though formal verification techniques have been dramatically evolved in the past 15 years, our main challenge remains scalability. Runtime verification (RV) and (path-based) symbolic execution (SE) have been successfully applied to verify real-world embedded software (and discover subtle errors), including single- and multi-threaded programs written in programming languages such as C/C++ and Java. RV involves executing a given system and analysing its behaviour to determine whether that particular execution satisfies or violates certain properties. By contrast, path-based SE is a completely static method that systematically and symbolically explores the program state space in a depth-first, random state or path selection fashion. An advantage of RV is that it is exact as it deals concretely with the actual system, conversely SE techniques must approximate certain aspects (e.g. external libraries). Due to a focus on single runs, RV scales up relatively well, however it gives limited confidence in the overall correctness of the system, whilst path-based SE gives more confidence in the verification results, but it suffers from the path- explosion problem, thus limiting scalability.
This project will explore the combination of Runtime Verification and Symbolic Execution with the aim of producing a method that combines the scalability of RV with the coverage of SE. It is likely that the developed method will leverage existing tools such as KLEE, Map2Check, MarQ, Frama-C and CProver.
The candidate should have a solid foundation in core computer science topics such as compilers, language theory, and logic, and strong programming skills (preferably in C++). The project will be under the supervisors of Dr Lucas Cordeiro (an expert in symbolic execution) and Dr Giles Reger (an expert in runtime verification)
Applications can be made via the standard process (see http://www.cs.manchester.ac.uk/study/postgraduate-research/programmes/phd/apply/) although we recommend checking your suitability before applying. The deadline for applications is 10th November 2018.
Please contact Dr Lucas Cordeiro (lucas.cordeiro@manchester.ac.uk) for further information.
[1] G. Rosen, "Security Update Facebook, Inc." 2018, [Online; accessed September-2018].
Person specification
For information
- Candidates must hold a minimum of an upper Second Class UK Honours degree or international equivalent in a relevant science or engineering discipline.
- Candidates must meet the School's minimum English Language requirement.
- Candidates will be expected to comply with the University's policies and practices of equality, diversity and inclusion.
Essential
Applicants will be required to evidence the following skills and qualifications.
- You must be capable of performing at a very high level.
- You must have a self-driven interest in uncovering and solving unknown problems and be able to work hard and creatively without constant supervision.
Desirable
Applicants will be required to evidence the following skills and qualifications.
- You will have good time management.
- You will possess determination (which is often more important than qualifications) although you'll need a good amount of both.
General
Applicants will be required to address the following.
- Comment on your transcript/predicted degree marks, outlining both strong and weak points.
- Discuss your final year Undergraduate project work - and if appropriate your MSc project work.
- How well does your previous study prepare you for undertaking Postgraduate Research?
- Why do you believe you are suitable for doing Postgraduate Research?