[CakeML] Fwd: Multiple Postdoc Positions on Formal Methods for Cyber Security

Mike Gordon Mike.Gordon at cl.cam.ac.uk
Thu Oct 23 07:03:14 UTC 2014


These guys might be interested in CakeML ... especially for "7. Secure
Code Generation."


---------- Forwarded message ----------
From: Liu Yang (Asst Prof) <yangliu at ntu.edu.sg>
Date: 23 October 2014 07:24
Subject: Multiple Postdoc Positions on Formal Methods for Cyber Security
To: PROCOS at jiscmail.ac.uk


Title: Multiple Postdoc Positions on Formal Methods for Cyber Security

http://www.ntu.edu.sg/home/yangliu/securify.html

Nanyang Technological University and
Singapore University of Technology and Design

Highly motivated applicants are sought to work on developing and
applying verification techniques for infinite state systems in the
project on Building Security Verified System.
The project aims to fully verify the execution stack of a cyber-physical system:
i.e., hardware, operating system, system libraries and applications,
using model checking and theorem proving technologies.
The postdocs will work with the PAT formal methods research group
(www.patroot.com) and other researchers at NTU and SUTD in Singapore.

They will also have the opportunity to travel overseas to collaborate
with partners of the project, including ETH Zurich, Oxford University,
Royal Holloway University of London, University of Luxembourg, Hong
Kong University of Science and Technology.

Positions for Research Fellow and Senior Research Fellow are available
for the following topics:

1. Hardware Verification.
   The preferred candidates are those with experience in one or more
of the following areas:
      - Formal methods, model checking, theorem proving.
      - Temporal logics, Higher order logic.
      - Functional programming.
      - Hardware design, especially SPARK/LEON architecture
    Contact: Liu Yang (yangliu at ntu.edu.sg), Alwen Tiu (atiu at ntu.edu.sg)

2. Microkernel Verification
   The preferred candidates are those with experience in one or more
of the following areas:
      - Formal methods, theorem proving.
      - Temporal logics, Higher order logic.
      - Functional programming.
      - Operating System Design.
   Contact: Liu Yang (yangliu at ntu.edu.sg)

3. Software Model Checking for Security
   The preferred candidates are those with experience in one or more
of the following areas:
      - Formal methods, model checking.
      - Temporal logics.
      - SMT solvers.
      - Formal languages and automata.
   Contact: Jun Sun (sunjun at sutd.edu.sg) and Yang Liu (yangliu at ntu.edu.sg)

4. Runtime security verification
   The preferred candidates are those with experience in one or more
of the following areas:
            - Temporal and modal logics
            - First-order theorem proving
            - Runtime verification
            - Preferably also backgrounds in operating system and
network security
   Contact: Alwen Tiu (atiu at ntu.edu.sg)

5. Compositional Verification of Security.
   The preferred candidates are those with experience in one or more
of the following areas:
      - Formal methods, model checking.
      - Assume-Guarantee Reasoning.
      - Temporal Logics.
      - Formal languages and automata.

   Contact: Yang Liu (yangliu at ntu.edu.sg) and Jun Sun (sunjun at sutd.edu.sg)

6. System Security.
   The preferred candidates are those with experience in one or more
of the following areas:
      - Binary security and analysis, especially LLVM.
      - Malware and vulnerabilities.
      - Mobile platform security.
      - Embedded system security.
      - Cloud security.

   Contact: Yang Liu (yangliu at ntu.edu.sg)

7. Secure Code Generation.
   The preferred candidates are those with experience in one or more
of the following areas:
      - Formal methods, model checking, theorem proving.
      - Temporal logics, Higher order logic.
      - Model driven development.

   Contact: Yang Liu (yangliu at ntu.edu.sg)

The position involves conducting basic research, developing tools,
working as part of a research team, travelling, and giving
presentations. The working language is English.

Apart from specific requirements to each topic candidate general
requirements are:
- A PhD in Computer Science or related areas is required.
- Strong background in logic and discrete math.
- Strong programming skills.
- An established research record.

The term is currently one to three years starting as early as January
2015 till all positions are filled.
The salary range is 4000 SGD - 6000 SGD per month for Research Fellows and
6000 - 8000 SGD per month for Senior Research Fellows.
Yearly bonus is 1 to 3 month salary based on the performance.
Singapore's tax is around 3%-5% of the annual salary.
1USD = 1.25 SGD.

Candidates interested in a particular topic or topics should contact
the contact person(s) listed in the respective topics above for more
details.

General inquiries can be directed at either Yang Liu, Jun Sun and Alwen Tiu.

________________________________
CONFIDENTIALITY: This email is intended solely for the person(s) named
and may be confidential and/or privileged. If you are not the intended
recipient, please delete it, notify us and do not copy, use, or
disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.



More information about the Users mailing list