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. He is now an Associate Professor at the University of Melbourne.
Contact Details
| Phone: | +61 2 9490 5867 |
|---|---|
| Email: | tobym@trustworthy.systems |
| Web: | http:/ |
| Twitter: | @tobycmurray |
More contact information is available at the Contact page.
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
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 group of Data61.
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 TS'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 and CSIRO.
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 Senior Lecturer at the University of Melbourne.
Grants
AOARD Grant #144093 “Verified OS Interface Code Synthesis” (2014-2016)
Program Committees and Editorial Boards
- SSV 2015 (PC co-chair)
- CRTS 2015
- PLAS 2015
- POPL 2015 (External Review Committee)
- SSV 2014
- CPP 2013
- SSV 2012
- DCDP 2010
Publications
- Google Scholar profile
- Best Papers
- TS Group Papers (2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011)
- Research Theses Supervised
Best Papers
|
 |
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 |
|
|
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 |
|
|
|
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 |
Trustworthy Systems Group Papers
2023
|
|
|
Rob Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser Formalising the prevention of microarchitectural timing channels by operating systems International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023 |
|
|
|
Scott Buckley, Rob Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser Proving the absence of microarchitectural timing channels arXiv preprint arXiv:2310.17046, 2023 |
2021
|
|
|
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell and Gabriele Keller Cogent: Uniqueness types and certifying compilation Journal of Functional Programming, Volume 31, 2021 |
|
|
|
Rob Sison and Toby Murray Verified secure compilation for mixed-sensitivity concurrent programs Journal of Functional Programming, Volume 31, pp. e18, 2021 |
2020
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein Towards provable timing-channel prevention ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020 |
2019
|
|
|
Rob Sison and Toby Murray Verifying that a compiler preserves concurrent value-dependent information-flow security International Conference on Interactive Theorem Proving, pp. 27:1–27:19, Portland, USA, September, 2019 |
|
|
|
Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019 |
2018
|
|
|
Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018 |
|
|
|
Toby Murray, Rob Sison and Kai Engelhardt COVERN: A logic for compositional verification of information flow control European Conference on Security and Privacy (EuroS&P), London, United Kingdom, April, 2018 |
2017
|
|
|
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor Provably trustworthy systems Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017 |
2016
|
|
|
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 |
|
|
|
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 |
|
|
|
Toby Murray, Rob Sison, Ed Pierzchalski and Christine Rizkallah Compositional verification and refinement of concurrent value-dependent noninterference IEEE Computer Security Foundations Symposium, pp. 417–431, Lisbon, Portugal, June, 2016 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
Liam O'Connor, 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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, 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. |
|
|
|
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 |
|
|
|
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. |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Sidney Amani, Leonid Ryzhyk and Toby Murray Towards a fully verified file system Poster presentation at EuroSys Doctoral Workshop, Bern, Switzerland, April, 2012 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012 |
2011
|
|
|
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 |
|
|
|
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 |
|
|
|
Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011 |
Research Theses Supervised
2018
|
|
|
Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, July, 2018 |
2016
|
|
|
Sidney Amani A methodology for trustworthy file systems PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016 |