Advertised: 01 April, 2019
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.
There are many approaches we might take. One promising one would be based on the Owicki-Gries method. It involve combining two ingredients:
In a recent paper, we have developed a technique called Decoupled Functional Correctness that allows one to take a traditional concurrent program verification method like Owicki-Gries and repurpose it to reason precisely about very expressive forms of information flow security.
At the same time, other researchers have been actively investigating how to adapt traditional concurrent program verification methods to reason soundly about programs in weak memory consistency models. Amongst other things, this has led to the development of a sound Owicki-Gries proof method for weak memory concurrency.
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.
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.
Please see the Position Description linked from the official Advertisement Page.
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.
The position is initially funded for up to two years, with possible extension beyond 24 months dependent on performance and funding.
Applications close on 30 April 2019, 11:55PM Australian Eastern Standard Time (AEST) (1:55PM GMT/UTC), and should be made on-line:
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/