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".
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
- 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.
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.
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),
Multi-Representational Security Analysis.
Eunsuk Kang, Aleksandar Milicevic, and Daniel Jackson.
Symposium on the Foundations of Software Engineering (FSE), 2016.
A tool for computing the robustness of systems
(described in the FSE 2020 paper)
A tool for synthesis of attackers for distributed protocols
(described in the SAFECOMP 2020 paper)
Synthesizer: A tool for automatically synthesizing secure
mappings from a protocol design to a platform model (described in
the CAV 19 paper)