[Main Page]

Research position in Program Verification and Security

Advertised: May 1st, 2017

I'm currently recruiting a researcher (a postdoc or a graduate with suitable experience), to work on the application of concurrent separation logic for verifying information flow security of seL4-based, security-critical embedded systems. Verified information flow security has seen something of a renaissance over the past 5 years, with success stories such as seL4 [IEEE Symposium on Security and Privacy ("Oakland" S&P) 2013 pdf] or the more recent mCertiKOS; but concurrency remains an open challenge and one that this project aims to address for the first time.

This research will:

  1. design and mechanise logics for verifying the information flow security of concurrent programs, and
  2. apply those logics to verify software running on seL4-based, user-facing critical embedded devices [Annual Computer Security Applications Conference (ACSAC) 2016 pdf], previously deployed on Defence networks to process and protect classified information.

Ideal applicants will have prior experience with an interactive theorem prover like Isabelle or Coq, and either knowledge of verification techniques for shared memory concurrent programs (e.g. rely guarantee, concurrent separation logic, etc.) or information flow security (noninterference, declassification, etc.).

The successful applicant will be based at the School of Computing and Information Systems, University of Melbourne and work in collaboration with project partners at Data61's Trustworthy Systems Group in Sydney and the Defence Science and Technology Group in Adelaide.

The position is currently funded for one year, with possible extension beyond 12 months contingent on additional funding.

Applicants are encouraged to contact me in the first instance.

Enquiries about the position should be directed to:
      Toby Murray