About the Project
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 ([Email Address Removed]) for further information.
[1] G. Rosen, "Security Update Facebook, Inc." 2018, [Online; accessed September-2018].
Funding Notes
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.
Continue with Facebook
