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.
Find out more about Toby Murray's experience
Toby Murray's highlights
Toby Murray's selected work
Verifying Expressive Information Flow Security For Weak Memory Concurrent Programs - Murra..
Displaying the 10 most recent projects by Toby Murray.
Internal Research Grant
Displaying the 45 most recent scholarly works by Toby Murray.
Verifying that a compiler preserves concurrent value-dependent information-flow security
R Sison, T Murray
Conference Proceedings | 2019 | Leibniz International Proceedings in Informatics, LIPIcs
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between re..
SECCSL: Security concurrent separation logic
G Ernst, T Murray
Conference Proceedings | 2019 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
© The Author(s) 2019. We present SecCSL, a concurrent separation logic for proving expressive, data-dependent information flow sec..
Empirically Analyzing Ethereum's Gas Mechanism
Renlord Yang, Toby Murray, Paul Rimba, Udaya Parampalli
Conference Proceedings | 2019 | 2019 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW)
Ethereum's Gas mechanism attempts to set transaction fees in accordance with the computational cost of transaction execution: a co..
COVERN: A Logic for Compositional Verification of Information Flow Control
T Murray, R Sison, K Engelhardt
Conference Proceedings | 2018 | 2018 IEEE European Symposium on Security and Privacy (EuroS&P)
© 2018 IEEE. Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive..
Permission and authority revisited towards a formalisation
Conference Proceedings | 2016 | Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs - FTfJP'16
© 2016 ACM. Miller's notions of permissions and authority are foundational to the analysis of object-capability programming. Infor..
A framework for the automatic formal verification of refinement from COGENT to C
C Rizkallah, J Lim, Y Nagashima, T Sewell, Z Chen, L O Connor, T Murray, G Keller, G Klein
Conference Proceedings | 2016 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
© Springer International Publishing Switzerland 2016.Our language Cogent simplifies verification of systems software using a certi..
CoGENT: Verifying High-Assurance File System Implementations.
S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, Y Nagashima, J Lim, T Sewell, J Tuong, G Keller, TC Murray, G Klein, G Heiser
Conference Proceedings | 2016 | Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS '16
Displaying the 3 most recent news articles by Toby Murray.
Honours, Awards and Fellowships
John Crampton Travelling Scholarship (3-year fully funded PhD scholarship to the University of Oxford)
Senior Lecturer In Software Engineering
Computing And Information Systems
Doctor of Philosophy in Computer Science
University of Oxford
Bachelor of Computer Science with First Class Honours