Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Postdoc position: verified timing-channel security for seL4

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Postdoc position: verified timing-channel security for seL4


Chronological Thread 
  • From: Toby Murray <toby.murray AT unimelb.edu.au>
  • To: "isabelle-users AT cl.cam.ac.uk" <isabelle-users AT cl.cam.ac.uk>, "coq-club AT inria.fr" <coq-club AT inria.fr>, "fm-announcements AT lists.nasa.gov" <fm-announcements AT lists.nasa.gov>, "procos AT jiscmail.ac.uk" <procos AT jiscmail.ac.uk>, "hol-info AT lists.sourceforge.net" <hol-info AT lists.sourceforge.net>, "SECURITY AT LISTSERV.IIT.CNR.IT" <SECURITY AT LISTSERV.IIT.CNR.IT>
  • Subject: [Coq-Club] Postdoc position: verified timing-channel security for seL4
  • Date: Mon, 10 Feb 2020 12:32:50 +0000
  • Accept-language: en-AU, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Neutral smtp.pra=toby.murray AT unimelb.edu.au; spf=Pass smtp.mailfrom=toby.murray AT unimelb.edu.au; spf=None smtp.helo=postmaster AT au-smtp-delivery-203.mimecast.com
  • Ironport-phdr: 9a23:tPOXmRH8UKTs8HiEo1BbNJ1GYnF86YWxBRYc798ds5kLTJ76pcq+bnLW6fgltlLVR4KTs6sC17OK9f65EjdRqdbZ6TZeKccKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZtJ6oryxbFv3REdupSyGh1IV6fgwvw6t2/8ZJ+/Slcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd4sBAfQcM+ZEoYfzpFoOohSiCgejH+7v1iZIimPq0aEmz+gsEQfL1xEgEdIUt3TUqc34OrkVUe+uzKjD0DLNb+5M2Tfn8ofJcg0qrPaQXbJ3asXQyVMjFwbYjlWKs4zqJTOU2/8Qs2id7upgUPygi2o8pA1rvDeg29oshpPTiYII013J8zhyzogyJd29UkF7YNikHYNKuCGAOIp2Q90iT3tvuCYgxb0KoYO7fC4LyJQi2RHfb+eIf5KW7R3+SeadOy13hG9jdbmihBiy6VCtxvD/W8WoylpGsylIn93WunwT1BHf8NaLRudz80u5xDqDyQPe5vtaLU00iabXMYItzqQtmpcQqUjDEDH5lUbqgKKTc0gr4fWn5Pjlb7jjpJKRN5F4hwTgPaswhMOyAOE1MgYMUmWV+umx0qDo81fjT7VQlPI2l7HUsJDEKsQfoa60GxVa0ps65xakCjemzMwYkWAaI11bfBKHjpbpNE/UIPH4FPuznUignTlxy/DDP73hB4vCIWTZn7f6YbZx8VJTyA02zdxH5pJUDK8OIO7rV0Pst9HUEgU1PxG3zuvjEtlxyIATVXiRDqOFPq7eqVqI6fguI+mIao8VojH9K/096v7yin82gl8ccbOs3ZsKcnC4BO5pIkWCbHrxhNcBEGIKsRQ6TOPxklGNTyNcZ2uoU60m+zE3EJimApvbRoCxnLyB2z+2EYFRZmBfE1yDDXPod5ifVPoXcyKTIsphkiQeWrS7So8h0wuutA7gxLZ9IOrU4H5QiZW2ntlu7ufekRU/sCFvAt6G+2qJCWp9myUBTHkr3+o39U1mw12O1ax1xuFDGMZIz/hNFAwzMNjVxKpnCIa2EkjKec7MQ1K7SP2nByswR5Q/2ZVGN016ApCpig3J9yusGb4c0bKRUth8uKzZmnH3IcFgzX3L0aQnk0IORspUKXbggKdk/k7cAJCD2xGXkuOjc6IbwSjG+WKOy3aVlEVZSxJrF6PMRnlZaUzI+5CxrFvYSLSpEpwlMxBKzMeDLu1DYZv0jh8OEO/5P9/ZeEqzmny7AB+JwvWFZ8z3eDNZlG/dD0xBkgYd+l6CNBMiHWG6pH/EBzFgEkjgbgXq/PU04Ce7SUtxzgeEaGVl1qGp4VgOguGGQP4d2agLtWEnpikiWB735P/9NuChmztJWIRnXegQ2mkB9EPl8SdbBNqBE+oq0mUzWDlNnn/f/zFWMbl7vPIU6lIL8ExZD5je8W8XJB2C2pWlBrrdOyHX4Qq1Yr+ejk3Z2sfQ/7oV8v0pg0jlvQSkEkBk/nl6ldBIhSjPrq7WBRYfBMqiGn088AJ38umDM3sNorjM3HgpCpGa9zrL2tYnHuwgk0jyYtFeNa6AHkn/H9BcDtX8cbV2yWjsVQoNOaVpzIBxJ9mvLqXUxaiqOetklnSrgXkB6Z0viBvRpRo5cfbB2tM++9/d3gaDUGyh3l6899vyhZgBaTwWH3Sy0zmhXtYKIKhzeIsAAHyyZcaww4cmig==

Postdoc position: verified timing-channel security for seL4

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Applications close: February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

Timing channels plague modern systems, undermining their security.
Yet no operating system provides provable protection against them.
We believe that seL4 can be the first kernel to meet this challenge [1],
building on its world-first proof of confidentiality enforcement [2]
and its unique mechanisms for implementing time protection [3].

The seL4 project is seeking a highly motivated postdoctoral
researcher to investigate methods for proving that operating system
kernels can defend against timing channels. We are seeking somebody
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. Your work will also investigate how to extend seL4’s
existing proofs of information flow security, which primarily cover
storage channels, to also encompass timing channels.

Further details about the research project are summarised in the
following position paper:

Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?" in Proceedings of the
Workshop on Hot Topics in Operating Systems (HotOS),
pages 23-29, May 2019.
https://arxiv.org/abs/1901.08338

The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/). You will work with a
close-knit team here at University of Melbourne, and collaborate
heavily with UNSW and Data61’s Trustworthy Systems group, in Sydney.

Candidates should have experience in at least one of the following:
- program verification (e.g. Hoare logic)
- information flow security (e.g. non-interference)
- interactive theorem provers (e.g. Isabelle, Coq, etc.)

Applications close on February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

To apply, or fore more information, visit:

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Informal enquiries should be directed to
Toby Murray

toby.murray AT unimelb.edu.au
https://people.eng.unimelb.edu.au/tobym/

References

[1] Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?", HotOS 2019

[2] Toby Murray, et al.
"seL4: From General Purpose to a Proof of Information
Flow Enforcement", IEEE Symposium on Security and Privacy 2013

[3] Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser.
"Time Protection: The Missing OS Abstraction", EuroSys 2019




---------
Toby Murray, DPhil (University of Oxford)
Senior Lecturer, School of Computing and Information Systems
University of Melbourne

https://people.eng.unimelb.edu.au/tobym/
toby.murray AT unimelb.edu.au





  • [Coq-Club] Postdoc position: verified timing-channel security for seL4, Toby Murray, 02/10/2020

Archive powered by MHonArc 2.6.18.

Top of Page