Bridging the Gap between Protocol Design and Implementation through Automated Mapping



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.





    Current Members

    • Connor Zanin
    • Anthony Peterson
    • Max Von Hippel


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.