Dr Toby Murray

  • Room: Level: 08 Room: 17
  • Building: Doug McDonell Building
  • Campus: Parkville

Research interests

    Personal webpage



    Toby is a faculty member of the Department of Computing and Information Systems. His research focuses on how to build highly secure computer systems using rigorous techniques, such as formal software verification and novel programming languages. Before joining the University of Melbourne, he worked at NICTA (now Data61) where he led the team that completed the world's first proof that a general purpose operating system kernel could enforce data confidentiality, for the seL4 kernel; played a leading role in the development of the COGENT programming language for verified systems programming; and collaborated with DST Group to build and verify the security of seL4-based cross domain devices. He holds a D.Phil. in Computer Science from the University of Oxford, awarded in June 2011, and a Bachelor of Computer Science with First Class Honours from the University of Adelaide, awarded in August 2005.

    Recent publications

    1. Rizkallah C, Lim J, Nagashima Y, Sewell T, Chen Z, O Connor L, Murray T, Keller G, Klein G. A framework for the automatic formal verification of refinement from COGENT to C. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2016, Vol. 9807.
    2. Amani S, Hixon A, Chen Z, Rizkallah C, Chubb P, O'Connor L, Beeren J, Nagashima Y, Lim J, Sewell T, Tuong J, Keller G, Murray T, Klein G, Heiser G. COGENT: Verifying High-Assurance File System Implementations. 21st International Conference on Architectural Support for Programming Languages and Operating Systems. Association for Computing Machinery Inc.. 2016, Vol. 50, Issue 2.
    3. Murray T, Sison R, Pierzchalski E, Rizkallah C. Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. 2016 IEEE 29TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2016). IEEE. 2016, Vol. 2016-August.
    4. Matichuk D, Murray T, Wenzel M. Eisbach: A Proof Method Language for Isabelle. 5th International Conference on Interactive Theorem Proving (ITP) held as part of the Federated Logic Conference (FLoC) part of the Vienna Summer of Logic. Springer Verlag. 2016, Vol. 56, Issue 3.
    5. Drossopoulou S, Noble J, Miller MS, Murray T. Permission and authority revisited towards a formalisation. Proceedings of the 18th Workshop on Formal Techniques for Java-Like Programs, FTfJP 2016 - Co-located with ECOOP 2016. 2016.
    6. O'Connor L, Chen Z, Rizkallah C, Amani S, Lim J, Murray T, Nagashima Y, Sewell T, Klein G. Refinement through Restraint: Bringing Down the Cost of Verification. 21st ACM SIGPLAN International Conference on Functional Programming (ICFP). Association for Computing Machinery Inc.. 2016, Vol. 51, Issue 9.
    7. Beaumont M, McCarthy J, Murray T. The cross domain desktop compositor: Using hardware-based video compositing for a multi-level secure user interface. 32nd Annual Computer Security Applications Conference (ACSAC). 2016, Vol. 5-9-December-2016.
    8. Jeffery R, Staples M, Andronick J, Klein G, Murray T. An empirical research agenda for understanding formal methods productivity. Information and Software Technology. Elsevier BV. 2015, Vol. 60.
    9. Matichuk D, Murray T, Andronick J, Jeffery R, Klein G, Staples M. Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. 2015 IEEE ACM 37th IEEE International Conference on Software Engineering. IEEE. 2015, Vol. 1.
    10. Murray T. Short paper: On high-assurance information-flow-secure programming languages. Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, PLAS 2015. 2015.
    11. Amani S, Murray T. Specifying a realistic file system. Electronic Proceedings in Theoretical Computer Science, EPTCS. 2015, Vol. 196.
    12. Matichuk D, Wenzel M, Murray T. An Isabelle proof method language. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2014, Vol. 8558 LNCS.
    13. Klein G, Andronick J, Elphinstone K, Murray T, Sewell T, Kolanski R, Heiser G. Comprehensive Formal Verification of an OS Microkernel. ACM TRANSACTIONS ON COMPUTER SYSTEMS. Association for Computing Machinery Inc.. 2014, Vol. 32, Issue 1.
    14. Keller G, Murray T, Amani S, O'Connor L, Chen Z, Ryzhyk L, Klein G, Heiser G. File systems deserve verification too!. ACM SIGOPS Operating Systems Review. Association for Computing Machinery. 2014, Vol. 48, Issue 1.
    15. Staples M, Jeffery R, Andronick J, Murray T, Klein G, Kolanski R. Productivity for proof engineering. International Symposium on Empirical Software Engineering and Measurement. 2014.

    View a full list of publications on the University of Melbourne’s ‘Find An Expert’ profile