Dr Toby Murray

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

Research interests

  • Computer Security
  • Concurrent Systems
  • Formal Verification
  • Operating Systems
  • Programming Languages
  • Software Engineering

Personal webpage

http://people.eng.unimelb.edu.au/tobym

Biography

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. Heiser, G.; Klein, G.; Murray, T. Can We Prove Time Protection?. Proceedings of the Workshop on Hot Topics in Operating Systems - HotOS '19. ACM Press. 2019, pp. 23-29. DOI: 10.1145/3317550.3321431
  2. Noble, J.; Potanin, A.; Murray, T.; Miller, MS. Abstract and Concrete Data Types vs Object Capabilities. . Springer International Publishing. 2018, pp. 221-240. DOI: 10.1007/978-3-319-98047-8_14
  3. Murray, T.; Van Oorschot, P. BP: Formal Proofs, the Fine Print and Side Effects. 2018 IEEE Cybersecurity Development (SecDev). IEEE. 2018, pp. 1-10. DOI: 10.1109/SecDev.2018.00009
  4. Murray, T.; Sison, R.; Engelhardt, K. COVERN: A Logic for Compositional Verification of Information Flow Control. 2018 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE. 2018, pp. 16-30. DOI: 10.1109/EuroSP.2018.00010
  5. Klein, G.; Andronick, J.; Fernandez, M.; Kuz, I.; Murray, T.; Heiser, G. Formally Verified Software in the Real World. Communications of the ACM. ASSOC COMPUTING MACHINERY. 2018, Vol. 61, Issue 10, pp. 68-77. DOI: 10.1145/3230627
  6. Issa, A.; Murray, T.; Ernst, G. In search of perfect users: Towards understanding the usability of converged multi-level secure user interfaces. Proceedings of the 30th Australian Conference on Computer-Human Interaction - OzCHI '18. ACM Press. 2018, pp. 572-576. DOI: 10.1145/3292147.3292231
  7. Klein, G.; Andronick, J.; Keller, G.; Matichuk, D.; Murray, T.; O'connor, L. Provably trustworthy systems. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. ROYAL SOC. 2017, Vol. 375, Issue 2104. DOI: 10.1098/rsta.2015.0404
  8. Gruetter, S.; Murray, T. Short paper: Towards information flow reasoning about real-world C code. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security - PLAS '17. ACM Press. 2017, Vol. 2017-January, pp. 43-48. DOI: 10.1145/3139337.3139345
  9. Murray, T.; Sabelfeld, A.; Bauer, L. Special issue on verified information flow security. Journal of Computer Security. IOS PRESS. 2017, Vol. 25, Issue 4-5, pp. 319-321. DOI: 10.3233/JCS-0559
  10. 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 International Publishing. 2016, Vol. 9807, pp. 323-340. DOI: 10.1007/978-3-319-43144-4_20
  11. 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, TC.; Klein, G.; Heiser, G. CoGENT: Verifying High-Assurance File System Implementations.. Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS '16. ACM. 2016, Vol. 50, Issue 2, pp. 175-188. DOI: 10.1145/2872362.2872404
  12. 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). IEEE. 2016, Vol. 2016-August, pp. 417-431. DOI: 10.1109/CSF.2016.36
  13. Matichuk, D.; Murray, TC.; Wenzel, M. Eisbach: A Proof Method Language for Isabelle. Journal of Automated Reasoning. Springer Verlag (Germany). 2016, Vol. 56, Issue 3, pp. 261-282. DOI: 10.1007/s10817-015-9360-2
  14. Murray, T. Permission and authority revisited towards a formalisation. Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs - FTfJP'16. Association for Computing Machinery (ACM). 2016. DOI: 10.1145/2955811.2955821
  15. Murray, T.; Stefan, D. PLAS 2016 chairs' welcome. PLAS 2016 - Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, co-located with CCS 2016. 2016, pp. iii-.
  16. Murray, T.; Stefan, D. PLAS'16-ACM SIGPLAN 11th Workshop on Programming Languages and Analysis for Security. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security - CCS'16. ASSOC COMPUTING MACHINERY. 2016, Vol. 24-28-October-2016, pp. 1870-1870. DOI: 10.1145/2976749.2990484
  17. 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. ACM SIGPLAN Notices. ACM. 2016, Vol. 51, Issue 9, pp. 89-102. DOI: 10.1145/2951913.2951940
  18. Beaumont, M.; Mccarthy, J.; Murray, T. The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface. Proceedings of the 32nd Annual Conference on Computer Security Applications - ACSAC '16. ACM. 2016, Vol. 5-9-December-2016, pp. 533-545. DOI: 10.1145/2991079.2991087
  19. Jeffery, R.; Staples, M.; Andronick, J.; Klein, G.; Murray, T. An empirical research agenda for understanding formal methods productivity. Information and Software Technology. Elsevier. 2015, Vol. 60, pp. 102-112. DOI: 10.1016/j.infsof.2014.11.005
  20. 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, pp. 722-732. DOI: 10.1109/ICSE.2015.85

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