Toby Murray
|
Toby
Murray
Room Room 311, Wolfson Building, Parks Road, Oxford OX1 3QD |
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.Links
Tools - Small tools I've developed during the course of my work at the ComLab
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). 2009. To appear |
| 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 | BibTeX | Download (pdf) | DOI (10.1016/j.entcs.2009.08.017) |
| Analysing Object-Capability Security Toby Murray In Proceedings of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS'08). 2008. |
Info
|
Themes |
|
|
Activities |
|
|
Supervisor |