We are seeking a highly motivated researcher with a research background in formal methods and security. You will contribute to the development of methods for reasoning about timing channels in verified operating system kernels, applied to the seL4 kernel.
The University of Melbourne is consistently ranked among the leading universities in the world, we are globally engaged; comprehensive; research-intensive; and committed to responding to the major challenges of our time.
University of Melbourne
25 February 2020
- PhD in Computer Science or a relevant discipline
- Experience in one or more of the following areas:
- program verification (e.g. Hoare logic)
- information flow security (e.g. non-interference)
- interactive theorem provers (e.g. Isabelle, Coq, etc.)
- Record of quality research as evidenced by research publications in leading conferences and journals, commensurate with opportunity
- Ability to perform independent research and a commitment to interdisciplinary research
- Capacity to communicate research concepts to technical and non-technical audiences
- Excellent written and verbal communication skills, demonstrated by presentation of research results at conferences, internal forums and through manuscript submissions
- Excellent interpersonal skills, including an ability to interact with internal and external stakeholders (academic, administrative support staff), in a courteous and effective manner.
- Ability to work independently and as part of a team
- Demonstrated capacity to develop expertise in research to undertake tasks with autonomy
- Excellent ability in analytical thinking, problem solving, maintaining accurate research records and developing new ideas
- Understanding of timing and side-channel attacks and principles
- Experience in supervision of undergraduate and graduate students