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

• Daniel Jackson (MIT)
• Eunsuk Kang (CMU)
• Stéphane Lafortune (University of Michigan)
• Cristina Nita-Rotaru (Northeastern University)
• Stavros Tripakis (Northeastern University)

Students

• Ian Dardik (PhD@CMU)
• Max von Hippel (PhD@NEU)
• Rômulo Meira-Góes (Postdoc@CMU)
• Daniel Melcer (PhD@NEU)
• Lisa Oakley (PhD@NEU)
• William Schultz (PhD@NEU)
• Ben Weintraub (PhD@NEU)
• Cheng Hao Yang (PhD@NEU)
• Connor Zanin (MS@NEU)
• Yuhao Zhou (PhD@NEU)

Publications

• Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents.
  Pacheco, Maria Leonor and Hippel, Max von and Weintraub, Ben and Goldwasser, Dan and Nita-Rotaru, Cristina.
  2022 IEEE Symposium on Security and Privacy (SP), 2022.
  
• Formal verification of a distributed dynamic reconfiguration protocol.
  Schultz, William and Dardik, Ian and Tripakis, Stavros.
  CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2022.
  
• Decentralized Observation of Discrete-Event Systems: At Least One Can Tell.
  Tripakis, Stavros and Rudie, Karen.
  IEEE Control Systems Letters, 2022.
  
• The refinement calculus of reactive systems.
  Preoteasa, Viorel and Dragomir, Iulia and Tripakis, Stavros.
  Information and Computation, 2022.
  
• On Neural Network Equivalence Checking Using SMT Solvers.
  Eleftheriadis, C. and Kekatos, N. and Katsaros, P. and Tripakis, S.
  Formal Modeling and Analysis of Timed Systems (FORMATS), 2022.
  
• Counterexample Classification.
  Vick, Cole and Kang, Eunsuk and Tripakis, Stavros.
  International Conference on Software Engineering and Formal Methods, 2021.
  
• Learning Moore machines from input–output traces.
  Giantamidis, Georgios and Tripakis, Stavros and Basagiannis, Stylianos.
  International Journal on Software Tools for Technology Transfer. 23 (1) 1 to 29, 2021.
  
• Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems.
  Rômulo Meira-Góes, Eunsuk Kang, Raymond H. Kwong, and Stéphane Lafortune.
  Automatica 121: 109172 (2020).
• Automated Attacker Synthesis for Distributed Protocols.
  Max von Hippel, Cole Vick, Stavros Tripakis, and Cristina Nita-Rotaru.
  International Conference on Computer Safety, Reliability and Security (SAFECOMP), 2020.
• A Behavioral Notion of Robustness for Software Systems.
  Changjian Zhang, David Garlan, and Eunsuk Kang.
  Symposium on the Foundations of Software Engineering (FSE), 2020.
• Towards Resilient Supervisors against Sensor Deception Attacks.
  Rômulo Meira-Góes, Hervé Marchand, and Stéphane Lafortune.
  IEEE Conference on Decision and Control (CDC), 2019.
• Automated Synthesis of Secure Platform Mappings.
  Eunsuk Kang, Stéphane Lafortune, and Stavros Tripakis.
  International Conference on Computer-Aided Verification (CAV), 2019.
  
• Multi-Representational Security Analysis.
  Eunsuk Kang, Aleksandar Milicevic, and Daniel Jackson.
  Symposium on the Foundations of Software Engineering (FSE), 2016.
  

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)