DR Toby Murray

DR Toby Murray

Positions

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

Overview

OverviewText1

  • 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.   

Publications

Selected publications

Research

Investigator on

Awards

Education and training

  • D.Phil., University of Oxford 2011
  • B. Comp. Sc. (Hons.), Adelaide University 2005

Awards and honors

  • John Crampton Travelling Scholarship (3-year fully funded PhD scholarship to the University of Oxford), University of Adelaide, 2006

Supervision

Available for supervision

  • Y

Supervision Statement

  • My research concerns computer security, and is motivated by the central questions of: 1. why should one computer system be considered more secure than another? 2. how can we build systems that are more secure, and do so more cheaply, than current ad hoc methods? 3. what evidence should we use to judge the security of a system, especially before it has been fielded? My research tends to favour rigorous approaches to answering these questions, although not exclusively. For instance, using machine checked proofs or sound empirical measurement to demonstrate system security, or using verifying compilation of secure programming languages to more easily build verified systems, are examples of rigorous approaches to building secure systems. On the other hand, some aspects of security like human behaviour need to be understood through a different lens but are no less vital. The most important quality I look for in potential research students (whether summer interns, undergraduate thesis students or higher degree research students) is genuine curiosity. Specific experience with formal methods or particular areas of security is not essential; although it may be beneficial for some topics. As you'll see from my home page, my interests in security are very broad, and I'm always willing to dive into a new topic for a motivated student.