Toby Murray
Interests
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.
Biography
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.Selected Publications
-
Analysing the Information Flow Properties of Object−Capability Patterns
Toby Murray and Gavin Lowe
In Proceedings of the Sixth International Workshop on Formal Aspects of Security and Trust (FAST2009). Vol. 5983 of Lecture Notes in Computer Science. Pages 81−95. 2010.
Details about Analysing the Information Flow Properties of Object−Capability Patterns | BibTeX data for Analysing the Information Flow Properties of Object−Capability Patterns | Download (pdf) of Analysing the Information Flow Properties of Object−Capability Patterns | DOI (10.1007/978-3-642-12459-4_7)
-
Analysing the Security Properties of Object−Capability Patterns
Toby Murray
PhD Thesis University of Oxford. 2010.
Details about Analysing the Security Properties of Object−Capability Patterns | BibTeX data for Analysing the Security Properties of Object−Capability Patterns | Download (pdf) of Analysing the Security Properties of Object−Capability Patterns
-
On Refinement−Closed Security Properties and Nondeterministic Compositions
Toby Murray and Gavin Lowe
In Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems (AVoCS '08). Vol. 250 of Electronic Notes in Theoretical Computer Science. No. 2. Pages 49−68. 2009.
Details about On Refinement−Closed Security Properties and Nondeterministic Compositions | BibTeX data for On Refinement−Closed Security Properties and Nondeterministic Compositions | Download (pdf) of On Refinement−Closed Security Properties and Nondeterministic Compositions | DOI (10.1016/j.entcs.2009.08.017)