Bridging the Gap between Protocol Design and Implementation through Automated Mapping

(logo)

Overview

The project follows a formal approach building upon a novel combination of techniques from security modeling, automated software synthesis, and program analysis to bridge the gap between an abstract protocol design and a low-level implementation. In particular, the methodology of the project will be 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. Building on this model, this project will provide (1) 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, (2) a synthesis tool that will automatically construct a secure mapping from the abstract protocol to the appropriate choice of platform features, and (3) a program analysis tool that leverages platform-specific information to check that an implementation satisfies a desired property of the protocol. In addition, the project will develop a library of reusable platform models, and demonstrate the effectiveness of the methodology in a series of case studies.

Publications

    Conferences

    • Automated Attacker Synthesis for Distributed Protocols
      Max von Hippel, Cole Vick, Stavros Tripakis, & Cristina Nita-Rotaru

      Distributed protocols should be robust to both benign malfunction (e.g. packet loss or delay) and attacks (e.g. message replay) from internal or external adversaries. In this paper we take a formal approach to the automated synthesis of attackers, i.e. adversarial processes that can cause the protocol to malfunction. Specifically, given a formal threat model capturing the distributed protocol model and network topology, as well as the placement, goals, and interface (inputs and outputs) of potential attackers, we automatically synthesize an attacker. We formalize four attacker synthesis problems - across attackers that always succeed versus those that sometimes fail, and attackers that attack forever versus those that do not - and we propose algorithmic solutions to two of them. We report on a prototype implementation called KORG and its application to TCP as a case-study. Our experiments show that KORG can automatically generate well-known attacks for TCP within seconds or minutes. [arXiv] [SRC] [SafeComp 2020] [💻 Blog Post]

    Presentations

    • Synthesizing Attacks Against Communication Protocols
      Max von Hippel

      Presented on 26 November 2019 to the University of Arizona Mathematics Department. [Event]

Students

    Current Members

    Previous Members

    • Connor Zanin
    • Anthony Peterson

Funding

This project is funded by SaTC 1801546 NSF grant: PI Stavros Tripakis, co-PI Cristina Nita-Rotaru (Northeastern University). This is a collaboration with Eunsuk Kang (Carnegie Mellon University), Stephane Lafortune (University of Michigan), and Daniel Jackson (MIT).