A single exploitable software vulnerability could enable hackers to steal thousands of users’ credentials (e.g., Heartbleed in 2014) or carry out millions of ransomware attacks (e.g., WannaCry 2017). The cybercrime risk will continue to increase, and by 2025, it will cost the world $10.5 trillion annually. Increasing concern is about solutions for catching security vulnerabilities to tackle this cost.

This project aims to study a solution for uncovering vulnerabilities using formal verification. Its overarching goal is to advance logical reasoning on software codebase by developing novel logical foundations and analysis techniques that leverage and extend existing incorrectness logic. The work will involve the development of novel mathematical logic and algorithms that formally prove the presence of security vulnerability in software. It will also involve the iterative development of robust software prototypes and their experimental evaluation. In particular, the work will include developing under-approximating logic, proof systems, and automated reasoning algorithms for analysing software source code, focusing on solving long-standing computer science problems like finding bugs in object-oriented programs with infinite executions (e.g., loop statements and recursive procedures). It will also consist of novel software systems to find bugs automatically in real-world codebases. Such software will leverage bi-abduction techniques for automation, scalability, and cyclic proof to reason about infinite executions.

The Ph.D. will provide training in programming principles, logic, and formal verification. Candidates should have a Bachalor’s degree in computer science or mathematics. Ideal candidates should have a Master’s degree with a solid technical background and interest in programming languages and logical methods in computer science.