korg-paper/main.bib

@article{Proverif, title={ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial}, author={Blanchet, Bruno and Smyth, Ben and Cheval, Vincent and Sylvestre, Marc}, language={en} }

@inproceedings{Pacheco2022, address={San Francisco, CA, USA}, title={Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents}, ISBN={978-1-66541-316-9}, url={https://ieeexplore.ieee.org/document/9833673/}, DOI={10.1109/SP46214.2022.9833673}, abstractNote={Automated attack discovery techniques, such as attacker synthesis or model-based fuzzing, provide powerful ways to ensure network protocols operate correctly and securely. Such techniques, in general, require a formal representation of the protocol, often in the form of a ﬁnite state machine (FSM). Unfortunately, many protocols are only described in English prose, and implementing even a simple network protocol as an FSM is time-consuming and prone to subtle logical errors. Automatically extracting protocol FSMs from documentation can signiﬁcantly contribute to increased use of these techniques and result in more robust and secure protocol implementations.}, booktitle={2022 IEEE Symposium on Security and Privacy (SP)}, publisher={IEEE}, author={Pacheco, Maria Leonor and Hippel, Max Von and Weintraub, Ben and Goldwasser, Dan and Nita-Rotaru, Cristina}, year={2022}, month=may, pages={51–68}, language={en} }

@article{Hippel2022_anonym,
  title={Anonymized for blinded submission},
 author={Anonym},
 year={XXX}
 }


@article{Hippel2022, title={Automated Attacker Synthesis for Distributed Protocols}, url={http://arxiv.org/abs/2004.01220}, DOI={10.48550/arXiv.2004.01220}, abstractNote={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.}, note={arXiv:2004.01220 [cs]}, number={arXiv:2004.01220}, publisher={arXiv}, author={von Hippel, Max and Vick, Cole and Tripakis, Stavros and Nita-Rotaru, Cristina}, year={2022}, month=apr }

@book{clarke2000model,
  title     = {Model Checking},
  author    = {Clarke, Edmund M. and Grumberg, Orna and Peled, Doron A.},
  year      = {2000},
  publisher = {MIT Press},
  address   = {Cambridge, MA},
  isbn      = {978-0-262-03270-4}
}

@inproceedings{vardi1986automata,
  title     = {An Automata-Theoretic Approach to Automatic Program Verification},
  author    = {Vardi, Moshe Y. and Wolper, Pierre},
  booktitle = {Proceedings of the First Annual Symposium on Logic in Computer Science (LICS)},
  pages     = {332--344},
  year      = {1986},
  publisher = {IEEE},
  address   = {Cambridge, MA},
  doi       = {10.1109/LICS.1986.227466}
}

@inproceedings{Vardi_Wolper_1986, title={An Automata-Theoretic Approach to Automatic Program Verification}, ISBN={978-0-8186-0720-2}, url={https://orbi.uliege.be/handle/2268/116609}, abstractNote={We describe an automata-theoretic  approach to the automatic verification of concurrent finite-state programs by
model checking.The basic idea underlying this approach is that for any temporal formula we can construct an automaton that accepts precisely the computations that satisfy the formula. The model-checking algorithm that results from this approach is much simpler and cleaner than tableau-based algorithms. We use this approach to extend model checking to probabilistic concurrent finite-state programs.
concurrent finite-state programs.}, publisher={IEEE Computer Society}, author={Vardi, Moshe Y. and Wolper, Pierre}, year={1986}, language={English} }

@inproceedings{Kozen_1977, address={Providence, RI, USA}, title={Lower bounds for natural proof systems}, url={http://ieeexplore.ieee.org/document/4567949/}, DOI={10.1109/SFCS.1977.16}, abstractNote={Two decidable logical theories are presented, one complete for deterministic polynomial time, one complete for polynomial space. Both have natural proof systems. A lower space bound of n/log(n) is shown for the proof system for the PTIME complete theory and a lower length bound of 2cn / 1og(n) is shown for the proof system for the PSPACE complete theory.}, booktitle={18th Annual Symposium on Foundations of Computer Science (sfcs 1977)}, publisher={IEEE}, author={Kozen, Dexter}, year={1977}, month=sep, pages={254–266}, language={en} }

@article{Holzmann_1997, title={The model checker SPIN}, volume={23}, rights={https://ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html}, ISSN={00985589}, DOI={10.1109/32.588521}, abstractNote={SPIN is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges. This paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications.}, number={5}, journal={IEEE Transactions on Software Engineering}, author={Holzmann, G.J.}, year={1997}, month=may, pages={279–295}, language={en} }

@article{Lamport_1994, title={The temporal logic of actions}, volume={16}, ISSN={0164-0925, 1558-4593}, DOI={10.1145/177492.177726}, abstractNote={The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician’s toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.}, number={3}, journal={ACM Transactions on Programming Languages and Systems}, author={Lamport, Leslie}, year={1994}, month=may, pages={872–923}, language={en} }

@article{Basin_Cremers_Dreier_Sasse_2022, title={Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols}, volume={20}, rights={https://ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html}, ISSN={1540-7993, 1558-4046}, DOI={10.1109/MSEC.2022.3154689}, abstractNote={Tamarin is a mature, state-of-the-art tool for cryptographic protocol veriﬁcation. We introduce Tamarin and survey some of the larger, tour-de-force results achieved with it. We also show how Tamarin can formalize a wide range of protocols, adversary models, and properties, and scale to substantial, real-world, veriﬁcation problems.}, number={3}, journal={IEEE Security \& Privacy}, author={Basin, David and Cremers, Cas and Dreier, Jannik and Sasse, Ralf}, year={2022}, month=may, pages={24–32}, language={en} }


@article{Kobeissi_Nicolas_Tiwari, title={Verifpal: Cryptographic Protocol Analysis for the Real World}, abstractNote={Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is easier to write and understand than the languages employed by existing tools. Its formal verification paradigm is also designed explicitly to provide protocol modeling that avoids user error. Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation. Furthermore, Verifpal’s semantics have been formalized within the Coq theorem prover, and Verifpal models can be automatically translated into Coq as well as into ProVerif models for further verification. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 as well as the first formal model for the DP-3T pandemic-tracing protocol, which we present in this work. Through Verifpal, we show that advanced verification with formalized semantics and sound logic can exist without any expense towards the convenience of real-world practitioners.}, author={Kobeissi, Nadim and Nicolas, Georgio and Tiwari, Mukesh}, language={en} }

@article{Blanchet_Jacomme, title={CryptoVerif: a Computationally-Sound Security Protocol Verifier}, abstractNote={This document presents the security protocol verifier CryptoVerif. CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy, correspondence properties (which include authentication), and indistinguishability properties. It produces proofs presented as sequences of games, like those manually written by cryptographers; these games are formalized in a probabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives. It produces proofs valid for any number of sessions of the protocol, and provides an upper bound on the probability of success of an attack against the protocol as a function of the probability of breaking each primitive and of the number of sessions. CryptoVerif is post-quantum sound: when the used cryptographic assumptions are valid for quantum adversaries, the proofs hold for quantum adversaries. It can work automatically, or the user can guide it with manual proof indications.}, author={Blanchet, Bruno and Jacomme, Charlie}, language={en} }

@article{Clarke_Wang, title={25 Years of Model Checking}, abstractNote={Model Checking is an automatic veriﬁcation technique for large state transition systems. It was originally developed for reasoning about ﬁnite-state concurrent systems. The technique has been used successfully to debug complex computer hardware, communication protocols, and software. It is beginning to be used for analyzing cyberphysical, biological, and ﬁnancial systems as well. The major challenge for the technique is a phenomenon called the State Explosion Problem. This issue is impossible to avoid in the worst case; but, by using sophisticated data structures and clever search algorithms, it is now possible to verify state transition systems with an astronomical number of states. In this paper, we will brieﬂy review the development of Model Checking over the past 32 years, with an emphasis on model checking stochastic hybrid systems.}, author={Clarke, Edmund M and Wang, Qinsi}, language={en} }

@article{Basin_Linker_Sasse, title={A Formal Analysis of the iMessage PQ3 Messaging Protocol}, abstractNote={We report on the design and verification of a highly performant, device-to-device messaging protocol offering strong security guarantees even against an adversary with quantum computing capabilities, called iMessage PQ3. The protocol leverages Apple’s identity services together with a custom, post-quantum secure initialization phase and afterwards it employs constructs from a double ratchet in the style of Signal, extended to provide post-quantum, post-compromise security. We present a detailed formal model of the protocol, a precise specification of its fine-grained security properties, and machine-checked proofs using the Tamarin prover. Particularly novel are the integration of postquantum secure key encapsulation into the relevant protocol phases and the detailed security claims along with their complete formal analysis, covering both key ratchets, including unbounded loops.}, author={Basin, David and Linker, Felix and Sasse, Ralf}, language={en} }


@inproceedings{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016, address={St. Petersburg FL USA}, title={Planning for change in a formal verification of the raft consensus protocol}, ISBN={978-1-4503-4127-1}, url={https://dl.acm.org/doi/10.1145/2854065.2854081}, DOI={10.1145/2854065.2854081}, abstractNote={We present the ﬁrst formal veriﬁcation of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an end-to-end guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our veriﬁed implementation is extracted to OCaml and runs on real networks.}, booktitle={Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs}, publisher={ACM}, author={Woos, Doug and Wilcox, James R. and Anton, Steve and Tatlock, Zachary and Ernst, Michael D. and Anderson, Thomas}, year={2016}, month=jan, pages={154–165}, language={en} }

@article{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson, title={Verdi: A Framework for Implementing and Formally Verifying Distributed Systems}, abstractNote={Distributed systems are difﬁcult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages.}, author={Wilcox, James R and Woos, Doug and Panchekha, Pavel and Tatlock, Zachary and Wang, Xi and Ernst, Michael D and Anderson, Thomas}, language={en} }

@article{Ongaro, title={Consensus: Bridging Theory and Practice}, author={Ongaro, Diego}, language={en} }

@inproceedings{Cluzel_Georgiou_Moy_Zeller_2021, address={Atlanta, GA, USA}, title={Layered Formal Verification of a TCP Stack}, rights={https://doi.org/10.15223/policy-009}, ISBN={978-1-66543-170-5}, url={https://ieeexplore.ieee.org/document/9652642/}, DOI={10.1109/SecDev51306.2021.00028}, abstractNote={The Transmission Control Protocol (TCP) at the heart of TCP/IP protocol stacks is a critical part of our current digital infrastructure. In this article, we show how an existing professional-grade open source embedded TCP/IP library can beneﬁt from a formally veriﬁed TCP reimplementation. Our approach is to apply formal veriﬁcation to the TCP layer only, relying on validated models of the lower layers on which it depends.}, booktitle={2021 IEEE Secure Development Conference (SecDev)}, publisher={IEEE}, author={Cluzel, Guillaume and Georgiou, Kyriakos and Moy, Yannick and Zeller, Clément}, year={2021}, month=oct, pages={86–93}, language={en} }

@phdthesis{Smith_1997, type={Thesis}, title={Formal verification of TCP and T/TCP}, rights={M.I.T. theses are protected by  copyright. They may be viewed from this source for any purpose, but  reproduction or distribution in any format is prohibited without written  permission. See provided URL for inquiries about permission.}, url={https://dspace.mit.edu/handle/1721.1/42779}, abstractNote={Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 1997.}, note={Accepted: 2008-09-03T18:09:43Z}, school={Massachusetts Institute of Technology}, author={Smith, Mark Anthony Shawn}, year={1997}, language={eng} }


@misc{rfc9260,
  author    = {M. Tüxen and R. Stewart and K. Nielsen and R. Jesup and S. Loreto},
  title     = {{Stream Control Transmission Protocol (SCTP) Specification Errata and Issues}},
  howpublished = {Request for Comments},
  number    = {9260},
  year      = {2022},
  month     = {June},
  publisher = {RFC Editor},
  url       = {https://www.rfc-editor.org/rfc/rfc9260},
  doi       = {10.17487/RFC9260}
}

@article{Holzmann_2014, title={Mars code}, volume={57}, ISSN={0001-0782, 1557-7317}, DOI={10.1145/2560217.2560218}, abstractNote={Redundant software (and hardware) ensured Curiosity reached its destination and functioned as its designers intended.}, number={2}, journal={Communications of the ACM}, author={Holzmann, Gerard J.}, year={2014}, month=feb, pages={64–73}, language={en} }

@article{Holzmann_Smith_2000, title={Automating software feature verification}, volume={5}, ISSN={1538-7305}, DOI={10.1002/bltj.2223}, abstractNote={A significant part of the call processing software for Lucent’s new PathStar™ Access Server was checked with formal verification techniques. The verification system we built for this purpose, named FeaVer, is accessed via a standard Web browser. The system maintains a database of feature requirements, together with the results of the most recently performed verifications. Via the browser the user can invoke new verification runs, which are performed in the background with the help of a logic model checking tool. Requirement violations are reported either as high-level message sequence charts or as detailed execution traces of the system source. A main strength of the system is its capability to detect potential feature interaction problems at an early stage of systems design. This type of problem is difficult to detect with traditional testing techniques. Error reports are typically generated by the system within minutes after a comprehensive check is initiated, allowing near-interactive probing of feature requirements and quick confirmation (or rejection) of the validity of tentative software fixes.}, number={2}, journal={Bell Labs Technical Journal}, author={Holzmann, Gerard J. and Smith, Margaret H.}, year={2000}, pages={72–87}, language={en} }

@inproceedings{mcp, address={Grenoble, France}, title={Model checking programs}, ISBN={978-0-7695-0710-1}, url={http://ieeexplore.ieee.org/document/873645/}, DOI={10.1109/ASE.2000.873645}, abstractNote={The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers, proof checkers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a veriﬁcation and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle big states, and partial order and symmetry reduction, slicing, abstraction, and runtime analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, runtime analysis, and slicing with model checking.}, booktitle={Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering}, publisher={IEEE}, author={Visser, W. and Havelund, K. and Brat, G. and Seungjoon Park}, year={2000}, pages={3–11}, language={en} }

@misc{wayne_adversaries,
  author       = {Hillel Wayne},
  title        = {Modeling Adversaries with TLA+},
  year         = {2019},
  url          = {https://www.hillelwayne.com/post/adversaries/},
  note         = {Accessed: 2024-12-03},
  howpublished = {\url{https://www.hillelwayne.com/post/adversaries/}}
}

@article{Pereira, title={EasyCrypt - a (brief) tutorial}, author={Pereira, Vitor}, language={en} }


@inbook{Cremers, address={Berlin, Heidelberg}, series={Lecture Notes in Computer Science}, title={The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols}, volume={5123}, ISBN={978-3-540-70543-7}, ISSN={0302-9743, 1611-3349}, url={http://link.springer.com/10.1007/978-3-540-70545-1_38}, DOI={10.1007/978-3-540-70545-1_38}, booktitle={Computer Aided Verification}, publisher={Springer Berlin Heidelberg}, author={Cremers, Cas J. F.}, editor={Gupta, Aarti and Malik, Sharad}, year={2008}, pages={414–418}, collection={Lecture Notes in Computer Science}, language={en} }

@article{Tamarin, title={Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols}, volume={20}, rights={https://ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html}, ISSN={1540-7993, 1558-4046}, DOI={10.1109/MSEC.2022.3154689}, abstractNote={Tamarin is a mature, state-of-the-art tool for cryptographic protocol veriﬁcation. We introduce Tamarin and survey some of the larger, tour-de-force results achieved with it. We also show how Tamarin can formalize a wide range of protocols, adversary models, and properties, and scale to substantial, real-world, veriﬁcation problems.}, number={3}, journal={IEEE Security \& Privacy}, author={Basin, David and Cremers, Cas and Dreier, Jannik and Sasse, Ralf}, year={2022}, month=may, pages={24–32}, language={en} }

@inproceedings{ParnoSOK, title={SoK: Computer-Aided Cryptography}, ISSN={2375-1207}, url={https://ieeexplore.ieee.org/document/9519449/?arnumber=9519449}, DOI={10.1109/SP40001.2021.00008}, abstractNote={Computer-aided cryptography is an active area of research that develops and applies formal, machine-checkable approaches to the design, analysis, and implementation of cryptography. We present a cross-cutting systematization of the computer-aided cryptography literature, focusing on three main areas: (i) design-level security (both symbolic security and computational security), (ii) functional correctness and efficiency, and (iii) implementation-level security (with a focus on digital side-channel resistance). In each area, we first clarify the role of computer-aided cryptography—how it can help and what the caveats are—in addressing current challenges. We next present a taxonomy of state-of-the-art tools, comparing their accuracy, scope, trustworthiness, and usability. Then, we highlight their main achievements, trade-offs, and research challenges. After covering the three main areas, we present two case studies. First, we study efforts in combining tools focused on different areas to consolidate the guarantees they can provide. Second, we distill the lessons learned from the computer-aided cryptography community’s involvement in the TLS 1.3 standardization effort. Finally, we conclude with recommendations to paper authors, tool developers, and standardization bodies moving forward.}, booktitle={2021 IEEE Symposium on Security and Privacy (SP)}, author={Barbosa, Manuel and Barthe, Gilles and Bhargavan, Karthik and Blanchet, Bruno and Cremers, Cas and Liao, Kevin and Parno, Bryan}, year={2021}, month=may, pages={777–795} }

@article{Castro_Liskov_2002, title={Practical byzantine fault tolerance and proactive recovery}, volume={20}, ISSN={0734-2071, 1557-7333}, DOI={10.1145/571637.571640}, abstractNote={Our growing reliance on online services accessible on the Internet demands highly available systems that provide correct service without interruptions. Software bugs, operator mistakes, and malicious attacks are a major cause of service interruptions and they can cause arbitrary behavior, that is, Byzantine faults. This article describes a new replication algorithm, BFT, that can be used to build highly available systems that tolerate Byzantine faults. BFT can be used in practice to implement real services: it performs well, it is safe in asynchronous environments such as the Internet, it incorporates mechanisms to defend against Byzantine-faulty clients, and it recovers replicas proactively. The recovery mechanism allows the algorithm to tolerate any number of faults over the lifetime of the system provided fewer than 1/3 of the replicas become faulty within a small window of vulnerability. BFT has been implemented as a generic program library with a simple interface. We used the library to implement the first Byzantine-fault-tolerant NFS file system, BFS. The BFT library and BFS perform well because the library incorporates several important optimizations, the most important of which is the use of symmetric cryptography to authenticate messages. The performance results show that BFS performs 2% faster to 24% slower than production implementations of the NFS protocol that are not replicated. This supports our claim that the BFT library can be used to build practical systems that tolerate Byzantine faults.}, number={4}, journal={ACM Transactions on Computer Systems}, author={Castro, Miguel and Liskov, Barbara}, year={2002}, month=nov, pages={398–461}, language={en} }

@inproceedings{Henda, address={San Jose CA USA}, title={Generic and efficient attacker models in SPIN}, ISBN={978-1-4503-2452-6}, url={https://dl.acm.org/doi/10.1145/2632362.2632378}, DOI={10.1145/2632362.2632378}, abstractNote={In telecommunication networks, it is common that security protocol procedures rely on context information and other parameters of the global system state. Current security veriﬁcation tools are well suited for analyzing protocols in isolation and it is not clear how they can be used for protocols intended to be run in more “dynamic” settings. Think of protocol procedures sharing parameters, arbitrarily interleaved or used as building blocks in more complex compound procedures. SPIN is a well established general purpose veriﬁcation tool that has good support for modeling such systems. In contrast to specialized tools, SPIN lacks support for cryptographic primitives and intruder model which are necessary for checking security properties. We consider a special class of security protocols that ﬁt well in the SPIN framework. Our modeling method is systematic, generic and eﬃcient enough so that SPIN could ﬁnd all the expected attacks on several of the classical key distribution protocols.}, booktitle={Proceedings of the 2014 International SPIN Symposium on Model Checking of Software}, publisher={ACM}, author={Ben Henda, Noomene}, year={2014}, month=jul, pages={77–86}, language={en} }

@article{Ginesin, title={A Formal Analysis of SCTP: Attack Synthesis and Patch Verification}, url={http://arxiv.org/abs/2403.05663}, abstractNote={SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance tests using the PacketDrill tool. Conformance testing is not exhaustive and a recent vulnerability (CVE-2021-3772) showed SCTP is not immune to attacks. Changes addressing the vulnerability were implemented, but the question remains whether other flaws might persist in the protocol design. We study the security of the SCTP design, taking a rigorous approach rooted in formal methods. We create a formal Promela model of SCTP, and define 10 properties capturing the essential protocol functionality based on its RFC specification and consultation with the lead RFC author. Then we show using the Spin model checker that our model satisfies these properties. We define 4 attacker models - Off-Path, where the attacker is an outsider that can spoof the port and IP of a peer; Evil-Server, where the attacker is a malicious peer; Replay, where an attacker can capture and replay, but not modify, packets; and On-Path, where the attacker controls the channel between peers. We modify an attack synthesis tool designed for transport protocols, Korg, to support our SCTP model and four attacker models. We synthesize 14 unique attacks using the attacker models - including the CVE vulnerability in the Off-Path attacker model, 4 attacks in the Evil-Server attacker model, an opportunistic ABORT attack in the Replay attacker model, and eight connection manipulation attacks in the On-Path attacker model. We show that the proposed patch eliminates the vulnerability and does not introduce new ones according to our model and protocol properties. Finally, we identify and analyze an ambiguity in the RFC, which we show can be interpreted insecurely. We propose an erratum and show that it eliminates the ambiguity.}, note={arXiv:2403.05663 [cs]}, number={arXiv:2403.05663}, publisher={arXiv}, author={Ginesin, Jacob and von Hippel, Max and Defloor, Evan and Nita-Rotaru, Cristina and Tüxen, Michael}, year={2024}, month=mar }

@inproceedings{TCPwn, address={San Diego, CA}, title={Automated Attack Discovery in TCP Congestion Control Using a Model-guided Approach}, ISBN={978-1-891562-49-5}, url={https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_02A-1_Jero_paper.pdf}, DOI={10.14722/ndss.2018.23115}, abstractNote={One of the most important goals of TCP is to ensure fairness and prevent congestion collapse by implementing congestion control. Various attacks against TCP congestion control have been reported over the years, most of which have been discovered through manual analysis. In this paper, we propose an automated method that combines the generality of implementation-agnostic fuzzing with the precision of runtime analysis to ﬁnd attacks against implementations of TCP congestion control. It uses a model-guided approach to generate abstract attack strategies, by leveraging a state machine model of TCP congestion control to ﬁnd vulnerable state machine paths that an attacker could exploit to increase or decrease the throughput of a connection to his advantage. These abstract strategies are then mapped to concrete attack strategies, which consist of sequences of actions such as injection or modiﬁcation of acknowledgements and a logical time for injection. We design and implement a virtualized platform, TCPWN, that consists of a a proxy-based attack injector and a TCP congestion control state tracker that uses only network trafﬁc to create and inject these concrete attack strategies. We evaluated 5 TCP implementations from 4 Linux distributions and Windows 8.1. Overall, we found 11 classes of attacks, of which 8 are new.}, booktitle={Proceedings 2018 Network and Distributed System Security Symposium}, publisher={Internet Society}, author={Jero, Samuel and Hoque, Endadul and Choffnes, David and Mislove, Alan and Nita-Rotaru, Cristina}, year={2018}, language={en} }

@inbook{Khan_Mukund_Suresh_2005, address={Berlin, Heidelberg}, series={Lecture Notes in Computer Science}, title={Generic Verification of Security Protocols}, volume={3639}, ISBN={978-3-540-28195-5}, url={http://link.springer.com/10.1007/11537328_18}, DOI={10.1007/11537328_18}, abstractNote={Security protocols are notoriously diﬃcult to debug. One approach to the automatic veriﬁcation of security protocols with a bounded set of agents uses logic programming with analysis and synthesis rules to describe how the attacker gains information and constructs new messages.}, booktitle={Model Checking Software}, publisher={Springer Berlin Heidelberg}, author={Khan, Abdul Sahid and Mukund, Madhavan and Suresh, S. P.}, editor={Godefroid, Patrice}, year={2005}, pages={221–235}, collection={Lecture Notes in Computer Science}, language={en} }


@inbook{Basin_Cremers_Meadows_2018, address={Cham}, title={Model Checking Security Protocols}, ISBN={978-3-319-10574-1}, url={http://link.springer.com/10.1007/978-3-319-10575-8_22}, DOI={10.1007/978-3-319-10575-8_22}, booktitle={Handbook of Model Checking}, publisher={Springer International Publishing}, author={Basin, David and Cremers, Cas and Meadows, Catherine}, editor={Clarke, Edmund M. and Henzinger, Thomas A. and Veith, Helmut and Bloem, Roderick}, year={2018}, pages={727–762}, language={en} }

@inbook{Basin_Mödersheim_Viganò_2003, address={Berlin, Heidelberg}, series={Lecture Notes in Computer Science}, title={An On-the-Fly Model-Checker for Security Protocol Analysis}, volume={2808}, rights={http://www.springer.com/tdm}, ISBN={978-3-540-20300-1}, url={http://link.springer.com/10.1007/978-3-540-39650-5_15}, DOI={10.1007/978-3-540-39650-5_15}, abstractNote={We introduce the on-the-ﬂy model-checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The ﬁrst is the use of lazy data-types as a simple way of building eﬃcient on-the-ﬂy model checkers for protocols with inﬁnite state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev-Yao intruder, whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness.}, booktitle={Computer Security – ESORICS 2003}, publisher={Springer Berlin Heidelberg}, author={Basin, David and Mödersheim, Sebastian and Viganò, Luca}, editor={Snekkenes, Einar and Gollmann, Dieter}, year={2003}, pages={253–270}, collection={Lecture Notes in Computer Science}, language={en} }

@inproceedings{Narayana_Chen_Zhao_Chen_Fu_Zhou_2006, title={Automatic Vulnerability Checking of IEEE 802.16 WiMAX Protocols through TLA+}, url={https://ieeexplore.ieee.org/document/4110436/?arnumber=4110436}, DOI={10.1109/NPSEC.2006.320346}, abstractNote={Vulnerability analysis is indispensably the first step towards securing a network protocol, but currently remains mostly a best effort manual process with no completeness guarantee. Formal methods are proposed for vulnerability analysis and most existing work focus on security properties such as perfect forwarding secrecy and correctness of authentication. However, it remains unclear how to apply these methods to analyze more subtle vulnerabilities such as denial-of-service (DoS) attacks. To address this challenge, in this paper, we propose use of TLA+ to automatically check DoS vulnerability of network protocols with completeness guarantee. In particular, we develop new schemes to avoid state space explosion in property checking and to model attackers’ capabilities for finding realistic attacks. As a case study, we successfully identify threats to IEEE 802.16 air interface protocols.}, booktitle={2006 2nd IEEE Workshop on Secure Network Protocols}, author={Narayana, Prasad and Chen, Ruiming and Zhao, Yao and Chen, Yan and Fu, Zhi and Zhou, Hai}, year={2006}, month=nov, pages={44–49} }

@article{Delzanno_Tatarek_Traverso_2014, title={Model Checking Paxos in Spin}, volume={161}, ISSN={2075-2180}, DOI={10.4204/EPTCS.161.13}, journal={Electronic Proceedings in Theoretical Computer Science}, author={Delzanno, Giorgio and Tatarek, Michele and Traverso, Riccardo}, year={2014}, month=aug, pages={131–146}, language={en} }


 @article{Sergey_Wilcox_Tatlock_2018, title={Programming and proving with distributed protocols}, volume={2}, ISSN={2475-1421}, DOI={10.1145/3158116}, abstractNote={Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on top of a two-phase commit instance). Recent work has developed several approaches for addressing (a) by means of mechanically verifying implementations of core distributed components, but no methodology exists to address (b) by composing such verified components into larger verified applications. As a result, expensive verification efforts for key system components are not easily reusable, which hinders further verification efforts. In this paper, we present Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant. In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel’s dependent type system, well-typed implementations always satisfy their protocols’ invariants and never go wrong, allowing users to verify system implementations interactively using Disel’s Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting. By virtue of the substitution principle and frame rule provided by Disel’s logic, system components can be composed leading to modular, reusable verified distributed systems. We describe Disel, illustrate its use with a series of examples, outline its logic and metatheory, and report on our experience using it as a framework for implementing, specifying, and verifying distributed systems.}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, author={Sergey, Ilya and Wilcox, James R. and Tatlock, Zachary}, year={2018}, month=jan, pages={1–30}, language={en} }


 @inproceedings{ironfleet, address={Monterey California}, title={IronFleet: proving practical distributed systems correct}, ISBN={978-1-4503-3834-9}, url={https://dl.acm.org/doi/10.1145/2815400.2815428}, DOI={10.1145/2815400.2815428}, abstractNote={Distributed systems are notorious for harboring subtle bugs. Veriﬁcation can, in principle, eliminate these bugs a priori, but veriﬁcation has historically been difﬁcult to apply at fullprogram scale, much less distributed-system scale.}, booktitle={Proceedings of the 25th Symposium on Operating Systems Principles}, publisher={ACM}, author={Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jacob R. and Parno, Bryan and Roberts, Michael L. and Setty, Srinath and Zill, Brian}, year={2015}, month=oct, pages={1–17}, language={en} }


 @inbook{Rahli_Vukotic_Völp_Esteves-Verissimo_2018, address={Cham}, series={Lecture Notes in Computer Science}, title={Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq}, volume={10801}, ISBN={978-3-319-89883-4}, url={http://link.springer.com/10.1007/978-3-319-89884-1_22}, DOI={10.1007/978-3-319-89884-1_22}, abstractNote={Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended eﬀorts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least n − f out of n replicas survive arbitrary faults. This paper presents Velisarios, a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the ﬁrst machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT.}, booktitle={Programming Languages and Systems}, publisher={Springer International Publishing}, author={Rahli, Vincent and Vukotic, Ivana and Völp, Marcus and Esteves-Verissimo, Paulo}, editor={Ahmed, Amal}, year={2018}, pages={619–650}, collection={Lecture Notes in Computer Science}, language={en} }

@article{Ongaro_Ousterhout, title={In Search of an Understandable Consensus Algorithm}, abstractNote={Raft is a consensus algorithm for managing a replicated log. It produces a result equivalent to (multi-)Paxos, and it is as efﬁcient as Paxos, but its structure is different from Paxos; this makes Raft more understandable than Paxos and also provides a better foundation for building practical systems. In order to enhance understandability, Raft separates the key elements of consensus, such as leader election, log replication, and safety, and it enforces a stronger degree of coherency to reduce the number of states that must be considered. Results from a user study demonstrate that Raft is easier for students to learn than Paxos. Raft also includes a new mechanism for changing the cluster membership, which uses overlapping majorities to guarantee safety.}, author={Ongaro, Diego and Ousterhout, John}, language={en} }


 @inproceedings{Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021, address={Virtual Event USA}, title={Toward formally verifying congestion control behavior}, ISBN={978-1-4503-8383-7}, url={https://dl.acm.org/doi/10.1145/3452296.3472912}, DOI={10.1145/3452296.3472912}, abstractNote={The diversity of paths on the Internet makes it difficult for designers and operators to confidently deploy new congestion control algorithms (CCAs) without extensive real-world experiments, but such capabilities are not available to most of the networking community. And even when they are available, understanding why a CCA under-performs by trawling through massive amounts of statistical data from network connections is challenging. The history of congestion control is replete with many examples of surprising and unanticipated behaviors unseen in simulation but observed on realworld paths. In this paper, we propose initial steps toward modeling and improving our confidence in a CCA’s behavior. We have developed Congestion Control Anxiety Controller (CCAC),1 a tool that uses formal verification to establish certain properties of CCAs. It is able to prove hypotheses about CCAs or generate counterexamples for invalid hypotheses. With CCAC, a designer can not only gain greater confidence prior to deployment to avoid unpleasant surprises, but can also use the counterexamples to iteratively improve their algorithm. We have modeled additive-increase/multiplicativedecrease (AIMD), Copa, and BBR with CCAC, and describe some surprising results from the exercise.}, booktitle={Proceedings of the 2021 ACM SIGCOMM 2021 Conference}, publisher={ACM}, author={Arun, Venkat and Arashloo, Mina Tahmasbi and Saeed, Ahmed and Alizadeh, Mohammad and Balakrishnan, Hari}, year={2021}, month=aug, pages={1–16}, language={en} }


 @article{Beurdouche, title={Formal Verification for High Assurance Security Software in FStar}, author={Beurdouche, Benjamin}, language={en} }

@inbook{Hsieh_Mitra_2019, address={Cham}, series={Lecture Notes in Computer Science}, title={Dione: A Protocol Verification System Built with Dafny for I/O Automata}, volume={11918}, ISBN={978-3-030-34967-7}, url={http://link.springer.com/10.1007/978-3-030-34968-4_13}, DOI={10.1007/978-3-030-34968-4_13}, abstractNote={Input/Output Automata (IOA) is an expressive speciﬁcation framework with built-in properties for compositional reasoning. It has been shown to be eﬀective in specifying and analyzing distributed and networked systems. The available veriﬁcation engines for IOA are based on interactive theorem provers such as Isabelle, Larch, PVS, and Coq, and are expressive but require heavy human interaction. Motivated by the advances in SMT solvers, in this work we explore a diﬀerent expressivity-automation tradeoﬀ for IOA. We present Dione, the ﬁrst IOA analysis system built with Dafny and its SMT-powered toolchain and demonstrate its eﬀectiveness on four distributed applications. Our translator tool converts Python-esque Dione language speciﬁcation of IOA and their properties to parameterized Dafny modules. Dione automatically generates the relevant compatibility and composition lemmas for the IOA speciﬁcations, which can then be checked with Dafny on a per module-basis. We ensure that all resulting formulas are expressed mostly in fragments solvable by SMT solvers and hence enables Bounded Model Checking and k-induction-based invariant checking using Z3. We present successful applications of Dione in veriﬁcation of an asynchronous leader election algorithm, two self-stabilizing mutual exclusion algorithms, and CAN bus Arbitration. We automatically prove key invariants of all four protocols; for the last three this involves reasoning about arbitrary number of participants. These analyses are largely automatic with minimal manual inputs needed, and they demonstrate the eﬀectiveness of this approach in analyzing networked and distributed systems.}, booktitle={Integrated Formal Methods}, publisher={Springer International Publishing}, author={Hsieh, Chiao and Mitra, Sayan}, editor={Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth}, year={2019}, pages={227–245}, collection={Lecture Notes in Computer Science}, language={en} }

@misc{message_queues_TLA, title={TLA+ Message Passing}, author={Hillel Wayne}, url={https://www.hillelwayne.com/post/tla-messages/}, abstractNote={I recently did a corporate TLA+ workshop and some people asked what TLA+ specs look like in practice. If you looked at the most common public examples, you’d probably come away thinking that people only used it for critical consensus algorithms. This is a problem for two reasons: first, it makes it harder to learn TLA+, as there aren’t simpler examples to experiment with. Second, it makes it hard for people to see how TLA+ is useful for them.}, journal={Hillel Wayne}, year={2018}, month=oct, language={en} }

@inbook{TLSMIN, address={Berlin, Heidelberg}, series={Lecture Notes in Computer Science}, title={LTSmin: High-Performance Language-Independent Model Checking}, volume={9035}, rights={http://www.springer.com/tdm}, ISBN={978-3-662-46680-3}, url={http://link.springer.com/10.1007/978-3-662-46681-0_61}, DOI={10.1007/978-3-662-46681-0_61}, abstractNote={In recent years, the LTSmin model checker has been extended with support for several new modelling languages, including probabilistic (Mapa) and timed systems (Uppaal). Also, connecting additional language front-ends or ad-hoc state-space generators to LTSmin was simpliﬁed using custom C-code. From symbolic and distributed reachability analysis and minimisation, LTSmin’s functionality has developed into a model checker with multi-core algorithms for on-the-ﬂy LTL checking with partial-order reduction, and multi-core symbolic checking for the modal µ-calculus, based on the multi-core decision diagram package Sylvan.}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, publisher={Springer Berlin Heidelberg}, author={Kant, Gijs and Laarman, Alfons and Meijer, Jeroen and Van De Pol, Jaco and Blom, Stefan and Van Dijk, Tom}, editor={Baier, Christel and Tinelli, Cesare}, year={2015}, pages={692–707}, collection={Lecture Notes in Computer Science}, language={en} }

@inbook{mCRL2, address={Cham}, series={Lecture Notes in Computer Science}, title={The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability}, volume={11428}, ISBN={978-3-030-17464-4}, url={http://link.springer.com/10.1007/978-3-030-17465-1_2}, DOI={10.1007/978-3-030-17465-1_2}, abstractNote={Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and language have been developed over a course of more than ﬁfteen years. In this paper, we report on the progress and advancements over the past six years. Firstly, the mCRL2 language has been extended to support the modelling of probabilistic behaviour. Furthermore, the usability has been improved with the addition of reﬁnement checking, counterexample generation and a user-friendly GUI. Finally, several performance improvements have been made in the treatment of behavioural equivalences. Besides the changes to the toolset itself, we cover recent applications of mCRL2 in software product line engineering and the use of domain speciﬁc languages (DSLs).}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, publisher={Springer International Publishing}, author={Bunte, Olav and Groote, Jan Friso and Keiren, Jeroen J. A. and Laveaux, Maurice and Neele, Thomas and De Vink, Erik P. and Wesselink, Wieger and Wijs, Anton and Willemse, Tim A. C.}, editor={Vojnar, Tomáš and Zhang, Lijun}, year={2019}, pages={21–39}, collection={Lecture Notes in Computer Science}, language={en} }

@article{Ginesin2024, title={A Formal Analysis of SCTP: Attack Synthesis and Patch Verification}, url={http://arxiv.org/abs/2403.05663}, abstractNote={SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance tests using the PacketDrill tool. Conformance testing is not exhaustive and a recent vulnerability (CVE-2021-3772) showed SCTP is not immune to attacks. Changes addressing the vulnerability were implemented, but the question remains whether other flaws might persist in the protocol design. We study the security of the SCTP design, taking a rigorous approach rooted in formal methods. We create a formal Promela model of SCTP, and define 10 properties capturing the essential protocol functionality based on its RFC specification and consultation with the lead RFC author. Then we show using the Spin model checker that our model satisfies these properties. We define 4 attacker models - Off-Path, where the attacker is an outsider that can spoof the port and IP of a peer; Evil-Server, where the attacker is a malicious peer; Replay, where an attacker can capture and replay, but not modify, packets; and On-Path, where the attacker controls the channel between peers. We modify an attack synthesis tool designed for transport protocols, Korg, to support our SCTP model and four attacker models. We synthesize 14 unique attacks using the attacker models - including the CVE vulnerability in the Off-Path attacker model, 4 attacks in the Evil-Server attacker model, an opportunistic ABORT attack in the Replay attacker model, and eight connection manipulation attacks in the On-Path attacker model. We show that the proposed patch eliminates the vulnerability and does not introduce new ones according to our model and protocol properties. Finally, we identify and analyze an ambiguity in the RFC, which we show can be interpreted insecurely. We propose an erratum and show that it eliminates the ambiguity.}, note={arXiv:2403.05663 [cs]}, number={arXiv:2403.05663}, publisher={arXiv}, author={Ginesin, Jacob and von Hippel, Max and Defloor, Evan and Nita-Rotaru, Cristina and Tüxen, Michael}, year={2024}, month=mar }