Bridging the Gap between Protocol Design and Implementation through Automated Mapping


This page is the offical site for the NSF SaTC Medium project #1801546: "Bridging the Gap between Protocol Design and Implementation through Automated Mapping".

Introduction

Computer networking and the internet have revolutionized our societies, but are plagued with security problems which are difficult to tame. Serious vulnerabilities are constantly being discovered in network protocols that affect the work and lives of millions. Even some protocols that have been carefully scrutinized by their designers and by the computer engineering community have been shown to be vulnerable afterwards. Why is developing secure protocols so hard? This project seeks to address this question by developing novel design and implementation methods for identifying and fixing security vulnerabilities in network protocols semi-automatically.

Technically, the goal of this project is to bridge the gap between an abstract protocol design and a low-level implementation through a novel combination of security modeling, automated software synthesis, and program analysis. In particular, the methodology of the project is based on a new formal behavioral model of software that explicitly captures how the choice of a mapping from a protocol design onto an implementation platform may result in different security vulnerabilities. The outcome of this project will include:

  • A modeling approach that cleanly separates the descriptions of an abstract design from a concrete platform, and allows the platform to be modeled just once and reused.
  • A synthesis tool that will automatically construct a secure mapping from the abstract protocol to the appropriate choice of platform features.
  • A program analysis tool that leverages platform-specific information to check that an implementation satisfies a desired property of the protocol.
  • A library of reusable platform models.

Target case studies include popular authorization and communication protocols such as OAuth, OpenID, SAML, and TLS.

People

Principal Investigators

Students

Publications

Tools

  • Robustness Calculator: A tool for computing the robustness of systems (described in the FSE 2020 paper)
  • Korg: A tool for synthesis of attackers for distributed protocols (described in the SAFECOMP 2020 paper)
  • Mapping Synthesizer: A tool for automatically synthesizing secure mappings from a protocol design to a platform model (described in the CAV 19 paper)