Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Research (postdoc or graduate) position in Pro...


view this post on Zulip Email Gateway (Aug 22 2022 at 15:27):

From: Toby Murray <toby.murray@unimelb.edu.au>
Dear all

[Please spread the word to folks you believe may be interested.
Apologies if you receive multiple copies of this message.]

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 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, 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 University of Melbourne
and work in collaboration with project partners at Data61's
Trustworthy Systems group in Sydney (http://ts.data61.csiro.au/) and
the Defence Science and Technology Group in Adelaide.

The position is currently funded for one year, beginning around
July--September 2017, with possible extension beyond 12 months
contingent on additional funding.

Applications close on the 28th of May, Australian Eastern Standard
Time (AEST, GMT +10 hours), and should be made on-line:

http://jobs.unimelb.edu.au/caw/en/job/890645/research-assistant-research-fellow-in-program-verification-security

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/

Thanks heaps

Toby


Last updated: Nov 21 2024 at 12:39 UTC