Mobile menu icon
Skip to navigation | Skip to main content | Skip to footer
Mobile menu icon Search iconSearch
Search type

Department of Computer Science


Exploiting Software Vulnerabilities at Large Scale

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

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?