Modern software is insecure for at least two reasons. Firstly, it is buggy and bugs invite exploits. Secondly, it runs with too much authority. This makes exploits dangerous, because an exploit can use the authority of the program it has exploited to cause unwanted effects.
I'm interested in solving these problems by applying formal verification to software systems that adhere to the Principle Of Least Authority (POLA). The object-capability model is one such system on which my work is currently focused. Perhaps the best source of information on the object-capability model is Part I of Mark Miller's PhD dissertation. Examples of real-world object-capability systems include programming languages such as E, Cajita and Joe-E, and operating systems such as CapROS (formerly EROS) and seL4. Plash also implements an object-capability system to bring POLA to the Unix desktop.
My work is currently concerned with model-checking object-capability patterns, which are reusable, composable security-enforcing abstractions that can be deployed in object-capability systems to enforce security policies. Previous work in this area includes Fred Spiessens' Scoll project, from which I've drawn much inspiration.
Toby Murray holds a Bachelor of Computer Science (Hons.) from the University of Adelaide. Before coming to Oxford, he worked on Research and Development in Computer Security for the Defence Science and Technology Organisation (DSTO), an organisation of the Australian Government devoted to Defence R&D. While working at DSTO, his research focused on Security Architectures for Pervasive Computing Environments and, in particular, the use of the Object-Capability Model as such an architecture.
