Some PhD research areas I am interested in
Generally, I am interested in supervising PhD research in all aspects of programming languages. More specifically, the interaction of programming languages and computer security is an exciting new research area. We have strength here in both programming language and computer security research.
While the list is not meant to be exhaustive, here are some possible subjects for PhD research that I would be happy to supervise, so that you could use them as a starting point for writing your PhD research proposal when applying for a PhD with me.
If you are interested in one of these topics, please see the page on applying for a PhD with me.
Cloud Computing and security
Cloud computing, particularly software as a service and platform as a service, raises problems about the interaction between the platform provider (such as Amazon) and service hosted there. Possible PhD topics include:
- Reasoning about nodes and virtual machines in the cloud, particularly using modal logics
- Applying game theory to analyzing the incentives of economic actors in the cloud, such as platform providers, business hosted in the cloud, and customers.
Multicore, many-core and GPGPU programming via abstract machines
CPUs now have increasingly many cores. Modern Graphics Processors (GPUs) have hundreds of cores and more. In principle they can be used for general purpose computation (GPGPU). While such architectures are potentially powerful, programming them is much harder than for sequential ones. This project develops abstract machines as a programming model for such architectures.
Safe systems-level programming
C is still the language of choice for programming operating systems and other code that needs to be efficient and manage system resources. However, C code is often afflicted with buffer overflows and other memory corruption vulnerabilities. Some experimental programming languages (such as Vault and Cyclone) aim to give the same power as C while being much safer (eliminating buffer overflows, for instance). A PhD thesis could build on the lessons learnt from those languages to defend against more classes of attacks.
Concurrent programming and security
Some of the most subtle security flaws arise due to race conditions in concurrent access to some critical resoure. The time-of-check-time-of-use (TOCTOU for short) vulnerability class is a classic example. Race conditions and other concurrency problems are likely to become more prevalent in distributed computing and the spread of multi-core processors. A PhD could use types and logics for concurrency to address these problems.
Abstract machines
Abstract machines give a concise desription of many programming language features. They can be used to prove the correctness of more high-level formalisms, such as showing soundess of Hoare logics. Some of the basics of abstract machines are covered in the Principles of Programming module I have taught in Semester 2, 2011.
Type and effect systems
I have done some work on type and effect systems for control (continuations); it would be interesting to see whether these results fit into a broader picture of computational effects in general, using mathematical tools like modal and classical logics.