[Main Page]

Research Position in Verified Confidentiality for Weak Memory Concurrency

Advertised: 01 April, 2019

Overview

I'm currently recruiting a researcher (either a postdoc or a graduate with suitable experience), to work on taking program verification methods for weak memory concurrency and adapting them to assist reasoning about information flow security for weak memory. That is, to adapt methods for reasoning about functional correctness on weak memory models to instead assist reasoning about confidentiality on these same memory models. The methods you develop will be applied to verify the security of seL4-based software for critical embedded devices, in collaboration with the seL4 team and other project partners.

Technical Approaches

Owicki-Gries

There are many approaches we might take. One promising one would be based on the Owicki-Gries method. It involve combining two ingredients:

By combining these two pieces, we have the opportunity to develop the first compositional techniques for reasoning precisely about expressive forms of information flow security on weak memory models.

Concurrent Separation Logic

Another approach we might investigate would be based on concurrent separation logic.

We expect that the ideas used to construct the latter separation logics for weak memory can be applied to our separation logic for information flow security, to allow it to reason over weak memory models. Doing so would yield compositional proof methods that can handle programs with pointers, arrays, dynamic allocation, etc., that are also amenable to automated verification.

Required Experience, Selection Criteria, Salary

Please see the Position Description linked from the official Advertisement Page.

Location

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

Duration

The position is initially funded for up to two years, with possible extension beyond 24 months dependent on performance and funding.

How to Apply

Applications close on 30 April 2019, 11:55PM Australian Eastern Standard Time (AEST) (1:55PM GMT/UTC), and should be made on-line:

Further Information

Applicants are encouraged to contact me in the first instance.

Enquiries about the position should be directed to:
      Toby Murray
      toby.murray@unimelb.edu.au
      http://people.eng.unimelb.edu.au/tobym/