University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Toby Murray

Personal photo - Toby Murray
Toby Murray
Doctoral Student
Former Member

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 Department of Computer Science

Selected Publications

View all

Manage 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.

Analysing the Security Properties of Object−Capability Patterns

Toby Murray

PhD Thesis University of Oxford. 2010.

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.

Info

Themes

Activities

Supervisor

SHARE THIS: