Bridging the Gap between Protocol Design and Implementation through Automated Mapping

Postdoctoral Scholar Position

We are looking for a postdoctoral scholar to work on formal methods for secure protocol development, under the NSF project "Bridging the Gap between Protocol Design and Implementation through Automated Mapping”. The goal of the project is to develop secure-by-construction methods for network protocols (such as OAuth and TLS) by automatically deriving a secure implementation from a high-level, formal protocol description. Potential research tasks include: (1) construction of network threat models for automated attack generation, (2) synthesis of secure implementations from protocol models through cross-layer mappings, and (3) formal analysis of protocols for robustness against attacks.

More information about the project, including relevant publications, can be found on the project site.

You will be working with three faculty involved in this project: Eunsuk Kang (Carnegie Mellon University), Stephane Lafortune (University of Michigan), and Stavros Tripakis (Northeastern University).

Qualifications

Candidates are expected to have a PhD in Computer Science or related fields, with a strong background and research record in formal methods, software engineering, programming languages or security. Familiarity with automated verification tools (e.g., SPIN, Alloy) is a plus although not required.

Timeline

Applications will be accepted until June 15, 2020. The position is expected to begin in September 2020 for 1 year, with a possibility of extension subject to the availability of funding.

Instructions

To apply, please send a copy of your latest CV and research statement to Stavros (stavros@northeastern.edu), Stephane (stephane@umich.edu), and Eunsuk (eskang@cmu.edu).