@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 finite 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 significantly 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, 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} }