Skip to main content

Toby Murray

Toby Murray
Senior Researcher; Lecturer, University of Melbourne

Research Interests

Toby's research interests broadly concern the application of formal methods to enable the cost-effective development of secure software and systems.

Contact Details

Phone: +61 2 8306 0567
Email:Toby.Murray@nicta.com.au
Web:http://people.eng.unimelb.edu.au/tobym
Twitter:@tobycmurray

More contact information is available at the Contact page.

Photo of Toby Murray

Publication List


Toby's current research focuses, among other things, on frameworks for verifying the security of microkernel-based systems in the context of the seL4 kernel, and on how to dramatically reduce the cost of producing verified systems code, like file systems, by leveraging domain-specific languages applying code-proof co-generation.

Projects

Current

Past

Toby is leading the Information Flow work for the seL4 microkernel, and is involved in the Trustworthy File Systems project, both of which are part of the Trustworthy Systems activity of SSRG.

Collaborations

Toby is currently leading a collaboration with the Defence Science and Technology Organisation to build and verify a secure cross domain solution device on seL4.

Toby is also collaborating with researchers from the University of Adelaide, Saarland University and WPI on techniques for timing channel mitigation, an activity closely related to SSRG's Timing Channels work.

Toby is also collaborating with researchers from Imperial College, Victoria University Wellington and Google on techniques for formally reasoning about the security of capability-based software, an activity that combines the expertise gained during his PhD and since at NICTA.

Toby previously led NICTA's work on a SBIR-funded collaboration with Galois Inc to build and verify a separation kernel platform on seL4.

Career Summary

Before joining NICTA, Toby studied at the University of Oxford under the supervision of Gavin Lowe, where he completed a D.Phil. (PhD) in Computer Science. His thesis examined the application of the CSP process algebra in order to formally reason about the security properties of object-capability patterns (i.e. to prove that reusable security-enforcing capability-based software abstractions actually enforce the security properties that they claim to).

Before studying at Oxford, Toby worked for the Defence Science and Technology Organisation (DSTO) where he researched and worked on security architectures for pervasive computing platforms. In particular, his work focused on the use of the object-capability model as such an architecture for DSTO's Annex pervasive computing project.

Qualifications

Toby holds a D.Phil. (PhD) in Computer Science from the University of Oxford, and a Bachelor of Computer Science with First Class Honours from the University of Adelaide.

Affiliations

Toby is a Conjoint Senior Lecturer at the School of Computer Science and Engineering at USNW.

Grants

AOARD Grant #144093 "Verified OS Interface Code Synthesis" (2014-2016)

Program Committees and Editorial Boards

Publications

Best Papers

Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011


NICTA Papers

2016

Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016
Abstract PDF Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah
Compositional verification and refinement of concurrent value-dependent noninterference
IEEE Computer Security Foundations Symposium, Lisbon, Portugal, June, 2016
Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016
Abstract PDF Daniel Matichuk, Toby Murray and Makarius Wenzel
Eisbach: A proof method language for isabelle
Journal of Automated Reasoning, Volume 56, Number 3, pp. 261-282, March, 2016

2015

Abstract PDF Sidney Amani and Toby Murray
Specifying a realistic file system
Workshop on Models for Formal Analysis of Real Systems, pp. 1-9, Suva, Fiji, November, 2015
Abstract PDF Toby Murray
On high-assurance information-flow-secure programming languages
ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 43-48, Prague, Czech Republic, July, 2015
Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
Empirical study towards a leading indicator for cost of formal software verification
International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015
Abstract PDF Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray
An empirical research agenda for understanding formal methods productivity
Information and Software Technology, Volume 60, pp. 102-112, January, 2015

2014

Abstract PDF David Cock, Qian Ge, Toby Murray and Gernot Heiser
The last mile: An empirical study of some timing channels on seL4
ACM Conference on Computer and Communications Security, pp. 570-581, Scottsdale, AZ, USA, November, 2014
Abstract PDF Liam O'Connor-Davis, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014
Abstract PDF Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski
Productivity for proof engineering
Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014
Abstract PDF Daniel Matichuk, Makarius Wenzel and Toby Murray
An Isabelle proof method language
International Conference on Interactive Theorem Proving, pp. 390-405, Vienna, Austria, July, 2014
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

2013

Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser
File systems deserve verification too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract PDF Toby Murray and Thomas Sewell
Above and beyond: seL4 noninterference and binary verification
Abstract, 2013 High Confidence Software and Systems Conference, Annapolis, MD, May, 2013.
Abstract PDF Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass
Formal specifications better than function points for code sizing
International Conference on Software Engineering, pp. 1257-1260, San Francisco, USA, May, 2013
Abstract PDF Toby Murray
On the limits of refinement-testing for model-checking CSP
Formal Aspects of Computing, Volume 25, Number 2, pp. 219-256, February, 2013

2012

Abstract PDF Daniel Matichuk and Toby Murray
Extensible specifications for automatic re-use of specifications and proofs
10th International Conference on Software Engineering and Formal Methods, pp. 8, Thessaloniki, Greece, December, 2012
Abstract PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126-142, Kyoto, Japan, December, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105
Technical Report, NICTA, October, 2012
Abstract
Slides
PDF Sidney Amani, Leonid Ryzhyk and Toby Murray
Towards a fully verified file system
Poster presentation at EuroSys Doctoral Workshop, Bern, Switzerland, April, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE: Security and Privacy, Volume 10, Number 2, pp. 67-70, March, 2012

2011

Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report option 1 – AOARD 104105
Technical Report, NICTA, November, 2011
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011

Non-NICTA Papers

2010

Abstract PDF Toby Murray
Analysing the security properties of object-capability patterns
PhD Thesis, University of Oxford, 2010
Abstract PDF Toby Murray and Gavin Lowe
Analysing the information flow properties of object-capability patterns
International Workshop on Formal Aspect of Security and Trust (FAST), pp. 81–95, Eindhoven, The Netherlands, 2010

2009

Abstract PDF Toby Murray and Gavin Lowe
On refinement-closed security properties and nondeterministic compositions
Proceedings of the 8th International Workshop on Automated Verification of Critical Systems, pp. 49–68, Glasgow, UK, 2009

2008

Abstract PDF Toby Murray and Duncan Grove
Non-delegatable authorities in capability systems
Journal of Computer Security, Volume 16, Number 6, pp. 743–759, 2008

2007

Abstract PDF Duncan Grove, Toby Murray, Chris Owen, Chris North, Jeremy Jones, M.R. Beaumont and B.D. Hopkins
An overview of the Annex system
Miami Beach, Florida, 2007

Research Theses Supervised

2016

Abstract PDF Sidney Amani
A methodology for trustworthy file systems
PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016