synchronous/korg-paper
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

IEEEtran.cls

Browse Source
This commit is contained in:
Cristina Nita-Rotaru
2024-11-28 14:54:05 -05:00
parent 62d6e309bb
commit 1846062f93
16 changed files with 572 additions and 438 deletions
Download Patch File Download Diff File Expand all files Collapse all files

116
main.aux
View File

@@ -1,46 +1,49 @@
\relax \relax
\citation{Lamport_1994,Holzmann_1997,Clarke_Wang} \citation{Lamport_1994,Holzmann_1997,Clarke_Wang}
\citation{Basin_Cremers_Dreier_Sasse_2022,Blanchet_Smyth_Cheval_Sylvestre,Kobeissi_Nicolas_Tiwari,Blanchet_Jacomme,Basin_Linker_Sasse} \citation{Basin_Cremers_Dreier_Sasse_2022,Blanchet_Smyth_Cheval_Sylvestre,Kobeissi_Nicolas_Tiwari,Blanchet_Jacomme,Basin_Linker_Sasse}
\citation{Hippel2022} \citation{Hippel2022_anonym}
\@writefile{toc}{\contentsline {section}{\numberline {I}Introduction}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {I}Introduction}{1}{}\protected@file@percent }
\newlabel{sec:introduction}{{I}{1}{}{}{}} \newlabel{sec:introduction}{{I}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {II}Design Methodology}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {II}\textsc {PANDA}\xspace Architecture}{1}{}\protected@file@percent }
\newlabel{sec:design}{{II}{1}{}{}{}} \newlabel{sec:design}{{II}{1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-A}}High-level design}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-A}}High-level design}{1}{}\protected@file@percent }
\newlabel{sub:High-level design}{{\mbox {II-A}}{1}{}{}{}} \newlabel{sub:High-level design}{{\mbox {II-A}}{1}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A high-level overview of the \textsc {Korg}\xspace workflow}}{1}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A high-level overview of the \textsc {PANDA}\xspace workflow}}{1}{}\protected@file@percent }
\newlabel{fig:korg_workflow}{{1}{1}{}{}{}} \newlabel{fig:korg_workflow}{{1}{1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-B}}Supported Attacker Models}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-B}}Supported Attacker Models}{1}{}\protected@file@percent }
\newlabel{sub:Supported Attacker Models}{{\mbox {II-B}}{1}{}{}{}} \newlabel{sub:Supported Attacker Models}{{\mbox {II-B}}{1}}
\citation{Kozen_1977} \newlabel{lst:korg_drop}{{1}{2}}
\citation{Clarke_Wang} \@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-C}}Soundness And Completeness of Korg}{2}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-C}}\textsc {PANDA}\xspace Implementation}{2}{}\protected@file@percent }
\newlabel{sub:Soundness And Completeness}{{\mbox {II-C}}{2}{}{}{}} \newlabel{sub:impl}{{\mbox {II-C}}{2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-D}}The Korg Implementation}{2}{}\protected@file@percent } \newlabel{lst:spin-model}{{6}{2}}
\newlabel{sub:The Korg Implementation}{{\mbox {II-D}}{2}{}{}{}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {6}Example \textsc {Promela}\xspace model of peers communicating over a channel. \texttt {!} indicates sending a message onto a channel, \texttt {?} indicates receiving a message from a channel.}{2}{}\protected@file@percent }
\newlabel{lst:spin-model}{{1}{2}{}{}{}} \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-D}}Usage}{2}{}\protected@file@percent }
\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Example \textsc {Promela}\xspace model of peers communicating over a channel. \texttt {!} indicates sending a message onto a channel, \texttt {?} indicates receiving a message from a channel.}{2}{}\protected@file@percent } \newlabel{sub:Usage}{{\mbox {II-D}}{2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-E}}Usage}{2}{}\protected@file@percent } \newlabel{lst:korg_replay}{{2}{3}}
\newlabel{sub:Usage}{{\mbox {II-E}}{2}{}{}{}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {2}Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{3}{}\protected@file@percent }
\newlabel{lst:abp}{{2}{3}{}{}{}} \newlabel{lst:korg_reordering}{{3}{3}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}{3}{}\protected@file@percent } \@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{3}{}\protected@file@percent }
\newlabel{lst:korg-shell}{{\mbox {II-E}}{3}{}{}{}} \newlabel{lst:abp}{{7}{3}}
\@writefile{toc}{\contentsline {section}{\numberline {III}Attacker Model Gadgets}{3}{}\protected@file@percent } \@writefile{lol}{\contentsline {lstlisting}{\numberline {7}Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}{3}{}\protected@file@percent }
\newlabel{sec:usage_attacker_models}{{III}{3}{}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-A}}Drop Attacker Model Gadget}{3}{}\protected@file@percent }
\newlabel{sub:Dropping Attacker}{{\mbox {III-A}}{3}{}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-B}}Replay Attacker Model Gadget}{3}{}\protected@file@percent }
\newlabel{sub:Replay Attacker}{{\mbox {III-B}}{3}{}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-C}}Reorder Attacker Model Gadget}{3}{}\protected@file@percent }
\newlabel{sub:reordering Attacker}{{\mbox {III-C}}{3}{}{}{}}
\citation{Cluzel_Georgiou_Moy_Zeller_2021,Smith_1997,Pacheco2022} \citation{Cluzel_Georgiou_Moy_Zeller_2021,Smith_1997,Pacheco2022}
\citation{Pacheco2022} \citation{Pacheco2022}
\citation{Pacheco2022,Hippel2022}
\citation{Pacheco2022}
\citation{Pacheco2022}
\citation{Pacheco2022} \citation{Pacheco2022}
\citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016,Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Ongaro} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016,Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Ongaro}
\citation{Ongaro} \citation{Ongaro}
\newlabel{lst:io-file}{{4}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Example I/O file targetting channel "cn"}{4}{}\protected@file@percent }
\newlabel{lst:io-file-synth}{{5}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Example gadget synthesized from an I/O file targetting the channel "cn"}{4}{}\protected@file@percent }
\newlabel{lst:korg-shell}{{\mbox {II-D}}{4}}
\@writefile{toc}{\contentsline {section}{\numberline {III}Case Studies}{4}{}\protected@file@percent }
\newlabel{sec:case_studies}{{III}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-A}}TCP}{4}{}\protected@file@percent }
\newlabel{sub:TCP}{{\mbox {III-A}}{4}}
\newlabel{res:tcp-table}{{\mbox {III-A}}{4}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Automatically discovered attacks against the hand-written TCP model from Pacheco et al. and our own, for $\phi _1$ through $\phi _4$. "x" indicates an attack was discovered, and no "x" indicates \textsc {PANDA}\xspace proved the absence of an attack via an exhaustive search. Full attack traces are available in the artifact.}}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-B}}Raft}{4}{}\protected@file@percent }
\newlabel{sub:Raft}{{\mbox {III-B}}{4}}
\citation{Ongaro} \citation{Ongaro}
\citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
\bibstyle{IEEEtran} \bibstyle{IEEEtran}
@@ -48,52 +51,21 @@
\bibcite{Lamport_1994}{1} \bibcite{Lamport_1994}{1}
\bibcite{Holzmann_1997}{2} \bibcite{Holzmann_1997}{2}
\bibcite{Clarke_Wang}{3} \bibcite{Clarke_Wang}{3}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-D}}Insert Attacker Models}{4}{}\protected@file@percent }
\newlabel{sub:Custom Attacker Models}{{\mbox {III-D}}{4}{}{}{}}
\@writefile{toc}{\contentsline {section}{\numberline {IV}Case Studies}{4}{}\protected@file@percent }
\newlabel{sec:case_studies}{{IV}{4}{}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {IV-A}}TCP}{4}{}\protected@file@percent }
\newlabel{sub:TCP}{{\mbox {IV-A}}{4}{}{}{}}
\newlabel{res:tcp-table}{{\mbox {IV-A}}{4}{}{}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Automatically discovered attacks against the hand-written TCP model from Pacheco et al. and our own, for $\phi _1$ through $\phi _4$. "x" indicates an attack was discovered, and no "x" indicates \textsc {Korg}\xspace proved the absence of an attack via an exhaustive search. Full attack traces are available in the artifact.}}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {IV-B}}Raft}{4}{}\protected@file@percent }
\newlabel{sub:Raft}{{\mbox {IV-B}}{4}{}{}{}}
\@writefile{toc}{\contentsline {section}{\numberline {V}Conclusion}{4}{}\protected@file@percent }
\newlabel{sec:conclusion}{{V}{4}{}{}{}}
\@writefile{toc}{\contentsline {section}{References}{4}{}\protected@file@percent }
\bibcite{Basin_Cremers_Dreier_Sasse_2022}{4} \bibcite{Basin_Cremers_Dreier_Sasse_2022}{4}
\bibcite{Blanchet_Smyth_Cheval_Sylvestre}{5} \bibcite{Blanchet_Smyth_Cheval_Sylvestre}{5}
\bibcite{Kobeissi_Nicolas_Tiwari}{6} \bibcite{Kobeissi_Nicolas_Tiwari}{6}
\bibcite{Blanchet_Jacomme}{7} \bibcite{Blanchet_Jacomme}{7}
\bibcite{Basin_Linker_Sasse}{8} \bibcite{Basin_Linker_Sasse}{8}
\bibcite{Hippel2022}{9} \bibcite{Hippel2022_anonym}{9}
\bibcite{Kozen_1977}{10} \bibcite{Kozen_1977}{10}
\bibcite{Cluzel_Georgiou_Moy_Zeller_2021}{11} \bibcite{Cluzel_Georgiou_Moy_Zeller_2021}{11}
\bibcite{Smith_1997}{12} \bibcite{Smith_1997}{12}
\bibcite{Pacheco2022}{13} \bibcite{Pacheco2022}{13}
\bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{14} \bibcite{Hippel2022}{14}
\bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{15} \bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{15}
\bibcite{Ongaro}{16} \bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{16}
\@writefile{toc}{\contentsline {section}{\numberline {VI}Appendix}{5}{}\protected@file@percent } \bibcite{Ongaro}{17}
\newlabel{sec:Appendix}{{VI}{5}{}{}{}} \@writefile{toc}{\contentsline {section}{\numberline {IV}Conclusion}{5}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {VI-A}}Full Korg Soundness and Completeness Proofs}{5}{}\protected@file@percent } \newlabel{sec:conclusion}{{IV}{5}}
\newlabel{sub:korg_proofs}{{\mbox {VI-A}}{5}{}{}{}} \@writefile{toc}{\contentsline {section}{References}{5}{}\protected@file@percent }
\citation{Holzmann_1997} \gdef \@abspage@last{5}
\citation{Kozen_1977}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {VI-B}}Preventing Korg Livelocks}{6}{}\protected@file@percent }
\newlabel{sub:Preventing Korg Livelocks}{{\mbox {VI-B}}{6}{}{}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {VI-C}}Attacker Model Gadget Examples}{6}{}\protected@file@percent }
\newlabel{sub:Attacker Model Gadget Examples}{{\mbox {VI-C}}{6}{}{}{}}
\newlabel{lst:drop_passer}{{3}{6}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Example dropping attacker model gadget with message skipping}{6}{}\protected@file@percent }
\newlabel{lst:korg_drop}{{4}{6}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}{6}{}\protected@file@percent }
\newlabel{lst:korg_replay}{{5}{7}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{7}{}\protected@file@percent }
\newlabel{lst:korg_reordering}{{6}{7}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{7}{}\protected@file@percent }
\newlabel{lst:io-file}{{7}{8}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {7}Example I/O file targetting channel "cn"}{8}{}\protected@file@percent }
\newlabel{lst:io-file-synth}{{8}{8}{}{}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {8}Example gadget synthesized from an I/O file targetting the channel "cn"}{8}{}\protected@file@percent }
\gdef \@abspage@last{8}

17
main.bbl
View File

@@ -58,13 +58,8 @@ B.~Blanchet and C.~Jacomme, ``\BIBforeignlanguage{en}{Cryptoverif: a
D.~Basin, F.~Linker, and R.~Sasse, ``\BIBforeignlanguage{en}{A formal analysis D.~Basin, F.~Linker, and R.~Sasse, ``\BIBforeignlanguage{en}{A formal analysis
of the imessage pq3 messaging protocol}.'' of the imessage pq3 messaging protocol}.''
\bibitem{Hippel2022} \bibitem{Hippel2022_anonym}
\BIBentryALTinterwordspacing Anonym, ``Anonymized for blinded submission,'' XXX.
M.~von Hippel, C.~Vick, S.~Tripakis, and C.~Nita-Rotaru, ``Automated attacker
synthesis for distributed protocols,'' no. arXiv:2004.01220, Apr. 2022,
arXiv:2004.01220 [cs]. [Online]. Available:
\url{http://arxiv.org/abs/2004.01220}
\BIBentrySTDinterwordspacing
\bibitem{Kozen_1977} \bibitem{Kozen_1977}
\BIBentryALTinterwordspacing \BIBentryALTinterwordspacing
@@ -104,6 +99,14 @@ M.~L. Pacheco, M.~V. Hippel, B.~Weintraub, D.~Goldwasser, and C.~Nita-Rotaru,
\url{https://ieeexplore.ieee.org/document/9833673/} \url{https://ieeexplore.ieee.org/document/9833673/}
\BIBentrySTDinterwordspacing \BIBentrySTDinterwordspacing
\bibitem{Hippel2022}
\BIBentryALTinterwordspacing
M.~von Hippel, C.~Vick, S.~Tripakis, and C.~Nita-Rotaru, ``Automated attacker
synthesis for distributed protocols,'' no. arXiv:2004.01220, Apr. 2022,
arXiv:2004.01220 [cs]. [Online]. Available:
\url{http://arxiv.org/abs/2004.01220}
\BIBentrySTDinterwordspacing
\bibitem{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016} \bibitem{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
\BIBentryALTinterwordspacing \BIBentryALTinterwordspacing
D.~Woos, J.~R. Wilcox, S.~Anton, Z.~Tatlock, M.~D. Ernst, and T.~Anderson, D.~Woos, J.~R. Wilcox, S.~Anton, Z.~Tatlock, M.~D. Ernst, and T.~Anderson,

14
main.bib
View File

@@ -1,5 +1,12 @@
@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} } @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_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 } @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, @book{clarke2000model,
@@ -22,8 +29,8 @@
doi = {10.1109/LICS.1986.227466} 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 @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. 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} } 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} } @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} }
@@ -44,7 +51,6 @@ concurrent finite-state programs.}, publisher={IEEE Computer Society}, author={V
@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} } @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} }
@article{Clarke_Wang, title={25 Years of Model Checking}, abstractNote={Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-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 financial 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 briefly 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} }
@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 first formal verification 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 verified 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} } @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 first formal verification 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 verified 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} }
@@ -56,8 +62,6 @@ concurrent finite-state programs.}, publisher={IEEE Computer Society}, author={V
@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} } @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} }
@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} }
@misc{rfc9260, @misc{rfc9260,
author = {M. Tüxen and R. Stewart and K. Nielsen and R. Jesup and S. Loreto}, author = {M. Tüxen and R. Stewart and K. Nielsen and R. Jesup and S. Loreto},

84
main.blg
View File

@@ -1,21 +1,14 @@
This is BibTeX, Version 0.99d (TeX Live 2024/Arch Linux) This is BibTeX, Version 0.99d (TeX Live 2023)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux The top-level auxiliary file: main.aux
The style file: IEEEtran.bst The style file: IEEEtran.bst
Reallocated singl_function (elt_size=8) to 100 items from 50. Reallocated singl_function (elt_size=4) to 100 items from 50.
Reallocated singl_function (elt_size=8) to 100 items from 50. Reallocated singl_function (elt_size=4) to 100 items from 50.
Reallocated singl_function (elt_size=8) to 100 items from 50. Reallocated singl_function (elt_size=4) to 100 items from 50.
Reallocated wiz_functions (elt_size=8) to 6000 items from 3000. Reallocated wiz_functions (elt_size=4) to 6000 items from 3000.
Reallocated singl_function (elt_size=8) to 100 items from 50. Reallocated singl_function (elt_size=4) to 100 items from 50.
Database file #1: main.bib Database file #1: main.bib
Repeated entry---line 49 of file main.bib Warning--I didn't find a database entry for "Hippel2022_anoym"
: @article{Clarke_Wang
: , title={25 Years of Model Checking}, abstractNote={Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-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 financial 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 briefly 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} }
I'm skipping whatever remains of this entry
Repeated entry---line 61 of file main.bib
: @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} }
I'm skipping whatever remains of this entry
-- IEEEtran.bst version 1.14 (2015/08/26) by Michael Shell. -- IEEEtran.bst version 1.14 (2015/08/26) by Michael Shell.
-- http://www.michaelshell.org/tex/ieeetran/bibtex/ -- http://www.michaelshell.org/tex/ieeetran/bibtex/
-- See the "IEEEtran_bst_HOWTO.pdf" manual for usage information. -- See the "IEEEtran_bst_HOWTO.pdf" manual for usage information.
@@ -29,6 +22,7 @@ Warning--empty journal in Blanchet_Jacomme
Warning--empty year in Blanchet_Jacomme Warning--empty year in Blanchet_Jacomme
Warning--empty journal in Basin_Linker_Sasse Warning--empty journal in Basin_Linker_Sasse
Warning--empty year in Basin_Linker_Sasse Warning--empty year in Basin_Linker_Sasse
Warning--empty journal in Hippel2022_anonym
Warning--empty journal in Hippel2022 Warning--empty journal in Hippel2022
Warning--empty journal in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson Warning--empty journal in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson
Warning--empty year in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson Warning--empty year in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson
@@ -36,45 +30,45 @@ Warning--empty journal in Ongaro
Warning--empty year in Ongaro Warning--empty year in Ongaro
Done. Done.
You've used 16 entries, You've used 17 entries,
4087 wiz_defined-function locations, 4087 wiz_defined-function locations,
927 strings with 10593 characters, 934 strings with 10701 characters,
and the built_in function-call counts, 9127 in all, are: and the built_in function-call counts, 9437 in all, are:
= -- 739 = -- 762
> -- 207 > -- 211
< -- 14 < -- 14
+ -- 98 + -- 100
- -- 49 - -- 50
* -- 519 * -- 530
:= -- 1420 := -- 1480
add.period$ -- 36 add.period$ -- 38
call.type$ -- 16 call.type$ -- 17
change.case$ -- 18 change.case$ -- 19
chr.to.int$ -- 0 chr.to.int$ -- 0
cite$ -- 31 cite$ -- 33
duplicate$ -- 786 duplicate$ -- 816
empty$ -- 765 empty$ -- 796
format.name$ -- 60 format.name$ -- 61
if$ -- 2081 if$ -- 2148
int.to.chr$ -- 0 int.to.chr$ -- 0
int.to.str$ -- 16 int.to.str$ -- 17
missing$ -- 147 missing$ -- 152
newline$ -- 83 newline$ -- 86
num.names$ -- 16 num.names$ -- 17
pop$ -- 385 pop$ -- 400
preamble$ -- 1 preamble$ -- 1
purify$ -- 0 purify$ -- 0
quote$ -- 2 quote$ -- 2
skip$ -- 691 skip$ -- 715
stack$ -- 0 stack$ -- 0
substring$ -- 134 substring$ -- 135
swap$ -- 552 swap$ -- 565
text.length$ -- 14 text.length$ -- 14
text.prefix$ -- 0 text.prefix$ -- 0
top$ -- 5 top$ -- 5
type$ -- 16 type$ -- 17
warning$ -- 15 warning$ -- 16
while$ -- 23 while$ -- 24
width$ -- 18 width$ -- 19
write$ -- 170 write$ -- 177
(There were 2 error messages) (There were 17 warnings)

446
main.log
View File

@@ -1,25 +1,25 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.7.2) 25 NOV 2024 05:14 This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex 2023.12.22) 28 NOV 2024 14:52
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled.
%&-line parsing enabled. %&-line parsing enabled.
**main.tex **main.tex
(./main.tex (./main.tex
LaTeX2e <2023-11-01> patch level 1 LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2024-02-20> L3 programming layer <2023-02-22> (./IEEEtran.cls
(./IEEEtran.cls
Document Class: IEEEtran 2015/08/26 V1.8b by Michael Shell Document Class: IEEEtran 2015/08/26 V1.8b by Michael Shell
-- See the "IEEEtran_HOWTO" manual for usage information. -- See the "IEEEtran_HOWTO" manual for usage information.
-- http://www.michaelshell.org/tex/ieeetran/ -- http://www.michaelshell.org/tex/ieeetran/
\@IEEEtrantmpdimenA=\dimen140 \@IEEEtrantmpdimenA=\dimen140
\@IEEEtrantmpdimenB=\dimen141 \@IEEEtrantmpdimenB=\dimen141
\@IEEEtrantmpdimenC=\dimen142 \@IEEEtrantmpdimenC=\dimen142
\@IEEEtrantmpcountA=\count188 \@IEEEtrantmpcountA=\count185
\@IEEEtrantmpcountB=\count189 \@IEEEtrantmpcountB=\count186
\@IEEEtrantmpcountC=\count190 \@IEEEtrantmpcountC=\count187
\@IEEEtrantmptoksA=\toks17 \@IEEEtrantmptoksA=\toks16
LaTeX Font Info: Trying to load font information for OT1+ptm on input line 5 LaTeX Font Info: Trying to load font information for OT1+ptm on input line 5
03. 03.
(/usr/share/texmf-dist/tex/latex/psnfss/ot1ptm.fd (/usr/local/texlive/2023/texmf-dist/tex/latex/psnfss/ot1ptm.fd
File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
) )
-- Using 8.5in x 11in (letter) paper. -- Using 8.5in x 11in (letter) paper.
@@ -91,63 +91,63 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/it' in size <24> not available
\IEEEiednormlabelsep=\dimen156 \IEEEiednormlabelsep=\dimen156
\IEEEiedmathlabelsep=\dimen157 \IEEEiedmathlabelsep=\dimen157
\IEEEiedtopsep=\skip48 \IEEEiedtopsep=\skip48
\c@section=\count191 \c@section=\count188
\c@subsection=\count192 \c@subsection=\count189
\c@subsubsection=\count193 \c@subsubsection=\count190
\c@paragraph=\count194 \c@paragraph=\count191
\c@IEEEsubequation=\count195 \c@IEEEsubequation=\count192
\abovecaptionskip=\skip49 \abovecaptionskip=\skip49
\belowcaptionskip=\skip50 \belowcaptionskip=\skip50
\c@figure=\count196 \c@figure=\count193
\c@table=\count197 \c@table=\count194
\@IEEEeqnnumcols=\count198 \@IEEEeqnnumcols=\count195
\@IEEEeqncolcnt=\count199 \@IEEEeqncolcnt=\count196
\@IEEEsubeqnnumrollback=\count266 \@IEEEsubeqnnumrollback=\count197
\@IEEEquantizeheightA=\dimen158 \@IEEEquantizeheightA=\dimen158
\@IEEEquantizeheightB=\dimen159 \@IEEEquantizeheightB=\dimen159
\@IEEEquantizeheightC=\dimen160 \@IEEEquantizeheightC=\dimen160
\@IEEEquantizeprevdepth=\dimen161 \@IEEEquantizeprevdepth=\dimen161
\@IEEEquantizemultiple=\count267 \@IEEEquantizemultiple=\count198
\@IEEEquantizeboxA=\box51 \@IEEEquantizeboxA=\box51
\@IEEEtmpitemindent=\dimen162 \@IEEEtmpitemindent=\dimen162
\IEEEPARstartletwidth=\dimen163 \IEEEPARstartletwidth=\dimen163
\c@IEEEbiography=\count268 \c@IEEEbiography=\count199
\@IEEEtranrubishbin=\box52 \@IEEEtranrubishbin=\box52
) )
** ATTENTION: Overriding command lockouts (line 2). ** ATTENTION: Overriding command lockouts (line 2).
(/usr/share/texmf-dist/tex/latex/cite/cite.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/cite/cite.sty
LaTeX Info: Redefining \cite on input line 302. LaTeX Info: Redefining \cite on input line 302.
LaTeX Info: Redefining \nocite on input line 332. LaTeX Info: Redefining \nocite on input line 332.
Package: cite 2015/02/27 v 5.5 Package: cite 2015/02/27 v 5.5
) )
(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2023/05/13 v2.17o AMS math features Package: amsmath 2022/04/08 v2.17n AMS math features
\@mathmargin=\skip51 \@mathmargin=\skip51
For additional information on amsmath, use the `?' option. For additional information on amsmath, use the `?' option.
(/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2021/08/26 v2.01 AMS text Package: amstext 2021/08/26 v2.01 AMS text
(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0 generic functions File: amsgen.sty 1999/11/30 v2.0 generic functions
\@emptytoks=\toks18 \@emptytoks=\toks17
\ex@=\dimen164 \ex@=\dimen164
)) ))
(/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen165 \pmbraise@=\dimen165
) )
(/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names Package: amsopn 2022/04/08 v2.04 operator names
) )
\inf@bad=\count269 \inf@bad=\count266
LaTeX Info: Redefining \frac on input line 234. LaTeX Info: Redefining \frac on input line 234.
\uproot@=\count270 \uproot@=\count267
\leftroot@=\count271 \leftroot@=\count268
LaTeX Info: Redefining \overline on input line 399. LaTeX Info: Redefining \overline on input line 399.
LaTeX Info: Redefining \colon on input line 410. LaTeX Info: Redefining \colon on input line 410.
\classnum@=\count272 \classnum@=\count269
\DOTSCASE@=\count273 \DOTSCASE@=\count270
LaTeX Info: Redefining \ldots on input line 496. LaTeX Info: Redefining \ldots on input line 496.
LaTeX Info: Redefining \dots on input line 499. LaTeX Info: Redefining \dots on input line 499.
LaTeX Info: Redefining \cdots on input line 620. LaTeX Info: Redefining \cdots on input line 620.
@@ -160,38 +160,38 @@ LaTeX Info: Redefining \Bigg on input line 725.
\big@size=\dimen166 \big@size=\dimen166
LaTeX Font Info: Redeclaring font encoding OML on input line 743. LaTeX Font Info: Redeclaring font encoding OML on input line 743.
LaTeX Font Info: Redeclaring font encoding OMS on input line 744. LaTeX Font Info: Redeclaring font encoding OMS on input line 744.
\macc@depth=\count274 \macc@depth=\count271
LaTeX Info: Redefining \bmod on input line 905. LaTeX Info: Redefining \bmod on input line 905.
LaTeX Info: Redefining \pmod on input line 910. LaTeX Info: Redefining \pmod on input line 910.
LaTeX Info: Redefining \smash on input line 940. LaTeX Info: Redefining \smash on input line 940.
LaTeX Info: Redefining \relbar on input line 970. LaTeX Info: Redefining \relbar on input line 970.
LaTeX Info: Redefining \Relbar on input line 971. LaTeX Info: Redefining \Relbar on input line 971.
\c@MaxMatrixCols=\count275 \c@MaxMatrixCols=\count272
\dotsspace@=\muskip16 \dotsspace@=\muskip16
\c@parentequation=\count276 \c@parentequation=\count273
\dspbrk@lvl=\count277 \dspbrk@lvl=\count274
\tag@help=\toks19 \tag@help=\toks18
\row@=\count278 \row@=\count275
\column@=\count279 \column@=\count276
\maxfields@=\count280 \maxfields@=\count277
\andhelp@=\toks20 \andhelp@=\toks19
\eqnshift@=\dimen167 \eqnshift@=\dimen167
\alignsep@=\dimen168 \alignsep@=\dimen168
\tagshift@=\dimen169 \tagshift@=\dimen169
\tagwidth@=\dimen170 \tagwidth@=\dimen170
\totwidth@=\dimen171 \totwidth@=\dimen171
\lineht@=\dimen172 \lineht@=\dimen172
\@envbody=\toks21 \@envbody=\toks20
\multlinegap=\skip52 \multlinegap=\skip52
\multlinetaggap=\skip53 \multlinetaggap=\skip53
\mathdisplay@stack=\toks22 \mathdisplay@stack=\toks21
LaTeX Info: Redefining \[ on input line 2953. LaTeX Info: Redefining \[ on input line 2953.
LaTeX Info: Redefining \] on input line 2954. LaTeX Info: Redefining \] on input line 2954.
) )
(/usr/share/texmf-dist/tex/latex/amsfonts/amssymb.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols Package: amssymb 2013/01/14 v3.01 AMS font symbols
(/usr/share/texmf-dist/tex/latex/amsfonts/amsfonts.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\symAMSa=\mathgroup4 \symAMSa=\mathgroup4
\symAMSb=\mathgroup5 \symAMSb=\mathgroup5
@@ -199,143 +199,141 @@ LaTeX Font Info: Redeclaring math symbol \hbar on input line 98.
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106. (Font) U/euf/m/n --> U/euf/b/n on input line 106.
)) ))
(/usr/share/texmf-dist/tex/latex/algorithms/algorithmic.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/algorithms/algorithmic.sty
Package: algorithmic 2009/08/24 v0.1 Document Style `algorithmic' Package: algorithmic 2009/08/24 v0.1 Document Style `algorithmic'
(/usr/share/texmf-dist/tex/latex/base/ifthen.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/base/ifthen.sty
Package: ifthen 2022/04/13 v1.1d Standard LaTeX ifthen package (DPC) Package: ifthen 2022/04/13 v1.1d Standard LaTeX ifthen package (DPC)
) )
(/usr/share/texmf-dist/tex/latex/graphics/keyval.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/keyval.sty
Package: keyval 2022/05/29 v1.15 key=value parser (DPC) Package: keyval 2022/05/29 v1.15 key=value parser (DPC)
\KV@toks@=\toks23 \KV@toks@=\toks22
) )
\c@ALC@unique=\count281 \c@ALC@unique=\count278
\c@ALC@line=\count282 \c@ALC@line=\count279
\c@ALC@rem=\count283 \c@ALC@rem=\count280
\c@ALC@depth=\count284 \c@ALC@depth=\count281
\ALC@tlm=\skip54 \ALC@tlm=\skip54
\algorithmicindent=\skip55 \algorithmicindent=\skip55
) )
(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/graphicx.sty
Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR)
(/usr/share/texmf-dist/tex/latex/graphics/graphics.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/graphics.sty
Package: graphics 2022/03/10 v1.4e Standard LaTeX Graphics (DPC,SPQR) Package: graphics 2022/03/10 v1.4e Standard LaTeX Graphics (DPC,SPQR)
(/usr/share/texmf-dist/tex/latex/graphics/trig.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/trig.sty
Package: trig 2021/08/11 v1.11 sin cos tan (DPC) Package: trig 2021/08/11 v1.11 sin cos tan (DPC)
) )
(/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
) )
Package graphics Info: Driver file: pdftex.def on input line 107. Package graphics Info: Driver file: pdftex.def on input line 107.
(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics-def/pdftex.def
File: pdftex.def 2022/09/22 v1.2b Graphics/color driver for pdftex File: pdftex.def 2022/09/22 v1.2b Graphics/color driver for pdftex
)) ))
\Gin@req@height=\dimen173 \Gin@req@height=\dimen173
\Gin@req@width=\dimen174 \Gin@req@width=\dimen174
) )
(/usr/share/texmf-dist/tex/latex/base/textcomp.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/base/textcomp.sty
Package: textcomp 2020/02/02 v2.0n Standard LaTeX package Package: textcomp 2020/02/02 v2.0n Standard LaTeX package
) )
(/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/xcolor/xcolor.sty
Package: xcolor 2023/11/15 v3.01 LaTeX color extensions (UK) Package: xcolor 2022/06/12 v2.14 LaTeX color extensions (UK)
(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics-cfg/color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration File: color.cfg 2016/01/02 v1.6 sample color configuration
) )
Package xcolor Info: Driver file: pdftex.def on input line 274. Package xcolor Info: Driver file: pdftex.def on input line 227.
(/usr/share/texmf-dist/tex/latex/graphics/mathcolor.ltx) (/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/mathcolor.ltx)
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1350. Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1353.
Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1354. Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1357.
Package xcolor Info: Model `RGB' extended on input line 1366. Package xcolor Info: Model `RGB' extended on input line 1369.
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1368. Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1371.
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1369. Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1372.
Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1370. Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1373.
Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1371. Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1374.
Package xcolor Info: Model `Gray' substituted by `gray' on input line 1372. Package xcolor Info: Model `Gray' substituted by `gray' on input line 1375.
Package xcolor Info: Model `wave' substituted by `hsb' on input line 1373. Package xcolor Info: Model `wave' substituted by `hsb' on input line 1376.
) )
(/usr/share/texmf-dist/tex/latex/amscls/amsthm.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/amscls/amsthm.sty
Package: amsthm 2020/05/29 v2.20.6 Package: amsthm 2020/05/29 v2.20.6
\thm@style=\toks24 \thm@style=\toks23
\thm@bodyfont=\toks25 \thm@bodyfont=\toks24
\thm@headfont=\toks26 \thm@headfont=\toks25
\thm@notefont=\toks27 \thm@notefont=\toks26
\thm@headpunct=\toks28 \thm@headpunct=\toks27
\thm@preskip=\skip56 \thm@preskip=\skip56
\thm@postskip=\skip57 \thm@postskip=\skip57
\thm@headsep=\skip58 \thm@headsep=\skip58
\dth@everypar=\toks29 \dth@everypar=\toks28
) )
(/usr/share/texmf-dist/tex/latex/tools/xspace.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/tools/xspace.sty
Package: xspace 2014/10/28 v1.13 Space after command names (DPC,MH) Package: xspace 2014/10/28 v1.13 Space after command names (DPC,MH)
) )
(/usr/share/texmf-dist/tex/latex/tools/array.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/tools/array.sty
Package: array 2023/10/16 v2.5g Tabular extension package (FMi) Package: array 2022/09/04 v2.5g Tabular extension package (FMi)
\col@sep=\dimen175 \col@sep=\dimen175
\ar@mcellbox=\box55 \ar@mcellbox=\box55
\extrarowheight=\dimen176 \extrarowheight=\dimen176
\NC@list=\toks30 \NC@list=\toks29
\extratabsurround=\skip59 \extratabsurround=\skip59
\backup@length=\skip60 \backup@length=\skip60
\ar@cellbox=\box56 \ar@cellbox=\box56
) )
(/usr/share/texmf-dist/tex/latex/comment/comment.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/comment/comment.sty
\CommentStream=\write3 \CommentStream=\write3
Excluding comment 'comment') Excluding comment 'comment')
\c@definition=\count285 \c@definition=\count282
(/usr/share/texmf-dist/tex/latex/listings/listings.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/listings.sty
\lst@mode=\count286 \lst@mode=\count283
\lst@gtempboxa=\box57 \lst@gtempboxa=\box57
\lst@token=\toks31 \lst@token=\toks30
\lst@length=\count287 \lst@length=\count284
\lst@currlwidth=\dimen177 \lst@currlwidth=\dimen177
\lst@column=\count288 \lst@column=\count285
\lst@pos=\count289 \lst@pos=\count286
\lst@lostspace=\dimen178 \lst@lostspace=\dimen178
\lst@width=\dimen179 \lst@width=\dimen179
\lst@newlines=\count290 \lst@newlines=\count287
\lst@lineno=\count291 \lst@lineno=\count288
\lst@maxwidth=\dimen180 \lst@maxwidth=\dimen180
(/usr/share/texmf-dist/tex/latex/listings/lstpatch.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstpatch.sty 2024/02/21 1.10 (Carsten Heinz) File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz)
) \c@lstnumber=\count289
(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty \lst@skipnumbers=\count290
File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz)
\c@lstnumber=\count292
\lst@skipnumbers=\count293
\lst@framebox=\box58 \lst@framebox=\box58
) )
(/usr/share/texmf-dist/tex/latex/listings/listings.cfg (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/listings.cfg
File: listings.cfg 2024/02/21 1.10 listings configuration File: listings.cfg 2023/02/27 1.9 listings configuration
)) ))
Package: listings 2024/02/21 1.10 (Carsten Heinz) Package: listings 2023/02/27 1.9 (Carsten Heinz)
(/usr/share/texmf-dist/tex/latex/listings/lstlang1.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang1.sty
File: lstlang1.sty 2024/02/21 1.10 listings language file File: lstlang1.sty 2023/02/27 1.9 listings language file
) )
(/usr/share/texmf-dist/tex/latex/listings/lstlang2.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang2.sty
File: lstlang2.sty 2024/02/21 1.10 listings language file File: lstlang2.sty 2023/02/27 1.9 listings language file
) )
(/usr/share/texmf-dist/tex/latex/listings/lstlang3.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang3.sty
File: lstlang3.sty 2024/02/21 1.10 listings language file File: lstlang3.sty 2023/02/27 1.9 listings language file
) )
(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty (/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz) File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz)
) )
\c@theorem=\count294 \c@theorem=\count291
(/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def (/usr/local/texlive/2023/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX) File: l3backend-pdftex.def 2023-01-16 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count295 \l__color_backend_stack_int=\count292
\l__pdf_internal_box=\box59 \l__pdf_internal_box=\box59
) (./main.aux) )
(./main.aux)
\openout1 = `main.aux'. \openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 53. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 53.
@@ -354,100 +352,125 @@ LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 53.
LaTeX Font Info: ... okay on input line 53. LaTeX Font Info: ... okay on input line 53.
-- Lines per column: 56 (exact). -- Lines per column: 56 (exact).
(/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii (/usr/local/texlive/2023/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).] [Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count296 \scratchcounter=\count293
\scratchdimen=\dimen181 \scratchdimen=\dimen181
\scratchbox=\box60 \scratchbox=\box60
\nofMPsegments=\count297 \nofMPsegments=\count294
\nofMParguments=\count298 \nofMParguments=\count295
\everyMPshowfont=\toks32 \everyMPshowfont=\toks31
\MPscratchCnt=\count299 \MPscratchCnt=\count296
\MPscratchDim=\dimen182 \MPscratchDim=\dimen182
\MPnumerator=\count300 \MPnumerator=\count297
\makeMPintoPDFobject=\count301 \makeMPintoPDFobject=\count298
\everyMPtoPDFconversion=\toks33 \everyMPtoPDFconversion=\toks32
) (/usr/share/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty ) (/usr/local/texlive/2023/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4 Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
85. 85.
(/usr/share/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg (/usr/local/texlive/2023/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv
e e
)) ))
\c@lstlisting=\count302 \c@lstlisting=\count299
(./sections/abstract.tex) (./sections/introduction.tex) (./sections/design.tex
LaTeX Warning: No \author given.
LaTeX Warning: No \author given.
LaTeX Warning: No \author given.
(./sections/abstract.tex) (./sections/introduction.tex
LaTeX Font Info: Trying to load font information for U+msa on input line 6.
(/usr/local/texlive/2023/texmf-dist/tex/latex/amsfonts/umsa.fd
File: umsa.fd 2013/01/14 v3.01 AMS symbols A
)
LaTeX Font Info: Trying to load font information for U+msb on input line 6.
(/usr/local/texlive/2023/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
))
(./sections/design.tex
<assets/diagram3.png, id=1, 733.99219pt x 277.035pt> <assets/diagram3.png, id=1, 733.99219pt x 277.035pt>
File: assets/diagram3.png Graphic file (type png) File: assets/diagram3.png Graphic file (type png)
<use assets/diagram3.png> <use assets/diagram3.png>
Package pdftex.def Info: assets/diagram3.png used on input line 11. Package pdftex.def Info: assets/diagram3.png used on input line 14.
(pdftex.def) Requested size: 258.0pt x 97.37796pt. (pdftex.def) Requested size: 258.0pt x 97.37796pt.
Overfull \hbox (6.0pt too wide) in paragraph at lines 11--12 Overfull \hbox (6.0pt too wide) in paragraph at lines 14--15
[][] [][]
[] []
LaTeX Font Info: Trying to load font information for U+msa on input line 22. [1{/usr/local/texlive/2023/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/l
ocal/texlive/2023/texmf-dist/fonts/enc/dvips/base/8r.enc}
(/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd
File: umsa.fd 2013/01/14 v3.01 AMS symbols A <./assets/diagram3.png (PNG copy)>] (./sections/examples.tex
LaTeX Font Info: Trying to load font information for OT1+pcr on input line 5
.
(/usr/local/texlive/2023/texmf-dist/tex/latex/psnfss/ot1pcr.fd
File: ot1pcr.fd 2001/06/04 font definitions for OT1/pcr.
) )
LaTeX Font Info: Trying to load font information for U+msb on input line 22.
LaTeX Warning: `h' float specifier changed to `ht'.
(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd LaTeX Warning: `h' float specifier changed to `ht'.
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
) [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/f
onts/enc/dvips/base/8r.enc}
<./assets/diagram3.png (PNG copy)>] LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: `h' float specifier changed to `ht'.
)
LaTeX Font Warning: Font shape `OT1/ptm/m/scit' undefined LaTeX Font Warning: Font shape `OT1/ptm/m/scit' undefined
(Font) using `OT1/ptm/m/sc' instead on input line 57. (Font) using `OT1/ptm/m/sc' instead on input line 85.
LaTeX Font Info: Trying to load font information for OT1+pcr on input line 9
5. Underfull \vbox (badness 10000) has occurred while \output is active []
(/usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
File: ot1pcr.fd 2001/06/04 font definitions for OT1/pcr. [2]
) [2] Underfull \vbox (badness 1067) has occurred while \output is active []
[3]
LaTeX Font Info: Trying to load font information for TS1+pcr on input line 1 LaTeX Font Info: Trying to load font information for TS1+pcr on input line 1
55. 49.
(/usr/share/texmf-dist/tex/latex/psnfss/ts1pcr.fd (/usr/local/texlive/2023/texmf-dist/tex/latex/psnfss/ts1pcr.fd
File: ts1pcr.fd 2001/06/04 font definitions for TS1/pcr. File: ts1pcr.fd 2001/06/04 font definitions for TS1/pcr.
) )
Excluding 'comment' comment.) (./sections/attacker_models.tex [3]) Excluding 'comment' comment.) (./sections/case_studies.tex
(./sections/case_studies.tex Underfull \hbox (badness 4144) in paragraph at lines 18--18
Underfull \hbox (badness 4144) in paragraph at lines 13--13
[]\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by []\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by
[] []
Underfull \hbox (badness 4144) in paragraph at lines 13--13 Underfull \hbox (badness 4144) in paragraph at lines 18--18
[]\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by []\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by
[] []
Underfull \hbox (badness 4144) in paragraph at lines 13--13 Underfull \hbox (badness 4144) in paragraph at lines 18--18
[]\OT1/pcr/m/n/7 SYN_RECEIVED \OT1/ptm/m/n/7 is even-tu-ally fol-lowed by []\OT1/pcr/m/n/7 SYN_RECEIVED \OT1/ptm/m/n/7 is even-tu-ally fol-lowed by
[] []
Underfull \hbox (badness 4144) in paragraph at lines 13--13 Underfull \hbox (badness 4144) in paragraph at lines 18--18
[]\OT1/pcr/m/n/5 SYN_RECEIVED \OT1/ptm/m/n/5 is even-tu-ally fol-lowed by []\OT1/pcr/m/n/5 SYN_RECEIVED \OT1/ptm/m/n/5 is even-tu-ally fol-lowed by
[] []
Excluding 'comment' comment. [4]
Overfull \hbox (4.66487pt too wide) in paragraph at lines 25--38 LaTeX Warning: Reference `' on page 5 undefined on input line 84.
[][]
[]
Excluding 'comment' comment.
LaTeX Warning: Reference `' on page 4 undefined on input line 82.
) (./sections/conclusion.tex) (./main.bbl ) (./sections/conclusion.tex) (./main.bbl
** WARNING: IEEEtran.bst: No hyphenation pattern has been ** WARNING: IEEEtran.bst: No hyphenation pattern has been
@@ -465,7 +488,6 @@ LaTeX Warning: Reference `' on page 4 undefined on input line 82.
** WARNING: IEEEtran.bst: No hyphenation pattern has been ** WARNING: IEEEtran.bst: No hyphenation pattern has been
** loaded for the language `en'. Using the pattern for ** loaded for the language `en'. Using the pattern for
** the default language instead. ** the default language instead.
[4]
** WARNING: IEEEtran.bst: No hyphenation pattern has been ** WARNING: IEEEtran.bst: No hyphenation pattern has been
** loaded for the language `en'. Using the pattern for ** loaded for the language `en'. Using the pattern for
** the default language instead. ** the default language instead.
@@ -500,7 +522,7 @@ LaTeX Warning: Reference `' on page 4 undefined on input line 82.
** loaded for the language `eng'. Using the pattern for ** loaded for the language `eng'. Using the pattern for
** the default language instead. ** the default language instead.
Underfull \hbox (badness 1509) in paragraph at lines 90--95 Underfull \hbox (badness 1509) in paragraph at lines 85--90
\OT1/ptm/m/n/8 t/tcp,'' The-sis, Mas-sachusetts In-sti-tute of Tech-nol-ogy, \OT1/ptm/m/n/8 t/tcp,'' The-sis, Mas-sachusetts In-sti-tute of Tech-nol-ogy,
[] []
@@ -522,44 +544,6 @@ Underfull \hbox (badness 1509) in paragraph at lines 90--95
** WARNING: IEEEtran.bst: No hyphenation pattern has been ** WARNING: IEEEtran.bst: No hyphenation pattern has been
** loaded for the language `en'. Using the pattern for ** loaded for the language `en'. Using the pattern for
** the default language instead. ** the default language instead.
) (./sections/appendix.tex
Underfull \hbox (badness 3503) in paragraph at lines 17--19
[]\OT1/ptm/b/n/10 Definition 2 \OT1/ptm/m/n/10 (Pro-cess)\OT1/ptm/b/n/10 . []\O
T1/ptm/m/it/10 A \OT1/ptm/m/n/10 Pro-cess \OT1/ptm/m/it/10 is a tu-ple $\OML/cm
m/m/it/10 P \OT1/cmr/m/n/10 =
[]
Underfull \hbox (badness 2165) in paragraph at lines 71--72
[]\OT1/ptm/m/n/10 In the Pro-cess: $\OML/cmm/m/it/10 s[]; s[]; s[]; []$ \OT1/pt
m/m/n/10 with $\OML/cmm/m/it/10 s[] \OT1/cmr/m/n/10 = \OML/cmm/m/it/10 s[]$ \OT
1/ptm/m/n/10 and
[]
LaTeX Font Warning: Font shape `OT1/ptm/m/scit' undefined
(Font) using `OT1/ptm/m/sc' instead on input line 89.
[5]
Underfull \hbox (badness 1715) in paragraph at lines 96--98
\OT1/ptm/m/n/10 via the pre-vi-ous the-o-rem we can con-struct B[]uchi Au-
[]
LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: `h' float specifier changed to `ht'.
) )
** Conference Paper ** ** Conference Paper **
@@ -572,43 +556,35 @@ Before submitting the final camera ready copy, remember to:
uses only Type 1 fonts and that every step in the generation uses only Type 1 fonts and that every step in the generation
process uses the appropriate paper size. process uses the appropriate paper size.
[6] [7] [8 [5] (./main.aux)
] (./main.aux)
***********
LaTeX2e <2023-11-01> patch level 1
L3 programming layer <2024-02-20>
***********
LaTeX Warning: There were undefined references. LaTeX Warning: There were undefined references.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
6647 strings out of 476076 6603 strings out of 476025
98844 string characters out of 5793776 99219 string characters out of 5790016
2225187 words of memory out of 5000000 2132388 words of memory out of 5000000
28643 multiletter control sequences out of 15000+600000 26945 multiletter control sequences out of 15000+600000
605917 words of font info for 126 fonts, out of 8000000 for 9000 557765 words of font info for 119 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191 1141 hyphenation exceptions out of 8191
57i,11n,65p,1153b,1534s stack positions out of 10000i,1000n,20000p,200000b,200000s 57i,11n,62p,1306b,1641s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/ </usr/local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fon ></usr/local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb><
ts/type1/public/amsfonts/cm/cmmi5.pfb></usr/share/texmf-dist/fonts/type1/public /usr/local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></u
/amsfonts/cm/cmmi7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cm sr/local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr
mi8.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/s /local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/lo
hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/share/texmf-dist/ cal/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/local
fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texmf-dist/fonts/type1/publ /texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/local/te
ic/amsfonts/cm/cmr7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c xlive/2023/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb></usr/local/texlive/20
msy10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr 23/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/local/texlive/2023/texmf-d
/share/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb></usr/share/texmf-dist/fon ist/fonts/type1/urw/times/utmbi8a.pfb></usr/local/texlive/2023/texmf-dist/fonts
ts/type1/urw/times/utmb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmb /type1/urw/times/utmr8a.pfb></usr/local/texlive/2023/texmf-dist/fonts/type1/urw
i8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/tex /times/utmri8a.pfb>
mf-dist/fonts/type1/urw/times/utmri8a.pfb> Output written on main.pdf (5 pages, 216255 bytes).
Output written on ./main.pdf (8 pages, 277407 bytes).
PDF statistics: PDF statistics:
113 PDF objects out of 1000 (max. 8388607) 82 PDF objects out of 1000 (max. 8388607)
69 compressed objects within 1 object stream 49 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
6 words of extra memory for PDF output out of 10000 (max. 10000000) 6 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
main.pdf
View File

Binary file not shown.

BIN
main.synctex.gz Normal file
View File

Binary file not shown.

36
main.tex
View File

@@ -19,7 +19,7 @@
\newcommand{\mvh}[1]{\textcolor{magenta}{Max says: {#1}}} \newcommand{\mvh}[1]{\textcolor{magenta}{Max says: {#1}}}
\newcommand{\jg}[1]{\textcolor{purple}{Jake says: {#1}}} \newcommand{\jg}[1]{\textcolor{purple}{Jake says: {#1}}}
\newcommand{\spin}[0]{\textsc{Spin}\xspace} \newcommand{\spin}[0]{\textsc{Spin}\xspace}
\newcommand{\korg}[0]{\textsc{Korg}\xspace} \newcommand{\korg}[0]{\textsc{PANDA}\xspace}
\newcommand{\promela}[0]{\textsc{Promela}\xspace} \newcommand{\promela}[0]{\textsc{Promela}\xspace}
\usepackage{listings} \usepackage{listings}
@@ -52,19 +52,19 @@
T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}} T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}
\begin{document} \begin{document}
\title{\korg: An Attack Synthesizer for Distributed Protocols\\ \title{\korg: An Attack Synthesis Tool\\ for Distributed Protocols\\
} }
\author{\IEEEauthorblockN{Jacob Ginesin} %\author{\IEEEauthorblockN{Jacob Ginesin}
\IEEEauthorblockA{\textit{Northeastern University}} %\IEEEauthorblockA{\textit{Northeastern University}}
\and %\and
\IEEEauthorblockN{Max von Hippel} %\IEEEauthorblockN{Max von Hippel}
\IEEEauthorblockA{\textit{Northeastern University}} %\IEEEauthorblockA{\textit{Northeastern University}}
\and %\and
\IEEEauthorblockN{Cristina Nita-Rotaru} %\IEEEauthorblockN{Cristina Nita-Rotaru}
\IEEEauthorblockA{\textit{Northeastern University}} %\IEEEauthorblockA{\textit{Northeastern University}}
} %}
\maketitle \maketitle
@@ -81,13 +81,13 @@ Protocols, Attack Synthesis, Denial of Service, Model Checking
\label{sec:introduction} \label{sec:introduction}
\input{sections/introduction} \input{sections/introduction}
\section{Design Methodology} \section{\korg Architecture}
\label{sec:design} \label{sec:design}
\input{sections/design} \input{sections/design}
\section{Attacker Model Gadgets} %\section{Attacker Model Gadgets}
\label{sec:usage_attacker_models} %\label{sec:usage_attacker_models}
\input{sections/attacker_models} %\input{sections/attacker_models}
\section{Case Studies} \section{Case Studies}
\label{sec:case_studies} \label{sec:case_studies}
@@ -101,9 +101,9 @@ Protocols, Attack Synthesis, Denial of Service, Model Checking
\bibliographystyle{IEEEtran} \bibliographystyle{IEEEtran}
\bibliography{main} \bibliography{main}
\section{Appendix}% %\section{Appendix}%
\label{sec:Appendix} %\label{sec:Appendix}
\input{sections/appendix} %\input{sections/appendix}
\end{document} \end{document}

0
sections/case_studies.log Normal file
View File

26
sections/case_studies.tex
View File

@@ -1,8 +1,13 @@
%!TEX root = ../main.tex
In this section we describe two case study, TCP transport protocol and RAFT state machine replication protocol.
\subsection{TCP}% \subsection{TCP}%
\label{sub:TCP} \label{sub:TCP}
TCP (Transmission Control Protocol) is a transport-layer protocol designed to establish reliable, ordered communications between two peers. TCP is ubiquitous in today's internet, and therefore has seen ample formal verification efforts \cite{Cluzel_Georgiou_Moy_Zeller_2021, Smith_1997, Pacheco2022}, including using \promela and \spin \cite{Pacheco2022}. A previous version of \korg has been applied TCP in \cite{Pacheco2022, Hippel2022}; TCP (Transmission Control Protocol) is a transport-layer protocol designed to establish reliable, ordered communications between two peers. TCP is ubiquitous in today's internet, and therefore has seen ample formal verification efforts \cite{Cluzel_Georgiou_Moy_Zeller_2021, Smith_1997, Pacheco2022}, including using \promela and \spin \cite{Pacheco2022}.
in particular, we study our \korg extensions using the hand-written TCP \promela model from \cite{Pacheco2022}. Additionally, we construct a TCP \promela model referencing the set of TCP RFCs. %A previous version of \korg has been applied TCP in \cite{Pacheco2022, Hippel2022};
%in particular, we study our \korg extensions using the hand-written TCP \promela model from \cite{Pacheco2022}.
We construct a TCP \promela model referencing the set of TCP RFCs.
For our analysis, we borrow the four LTL properties used in \cite{Pacheco2022}, as detailed below: For our analysis, we borrow the four LTL properties used in \cite{Pacheco2022}, as detailed below:
%we study our \korg extensions using the \promela models from Pacheco et al., which includes a "gold" model whose underlying state machine is derived via an NLP-based algorithm applied to the SCTP RFC \cite{rfc9260} and a "canonical" model hand-written by domain experts \cite{Pacheco2022}. %we study our \korg extensions using the \promela models from Pacheco et al., which includes a "gold" model whose underlying state machine is derived via an NLP-based algorithm applied to the SCTP RFC \cite{rfc9260} and a "canonical" model hand-written by domain experts \cite{Pacheco2022}.
\[ \[
@@ -14,7 +19,7 @@ For our analysis, we borrow the four LTL properties used in \cite{Pacheco2022},
\end{aligned} \end{aligned}
\] \]
We evaluated the our TCP \promela model and the hand-written TCP \promela model presented by \cite{Pacheco2022} against \korg's drop, replay, and reordering attacker models on a single uni-directional communication channel. The resulting breakdown of attacks discovered is shown in Figure \ref{res:tcp-table}. We evaluated the TCP \promela model against \korg's drop, replay, and reordering attacker models on a single uni-directional communication channel. The resulting breakdown of attacks discovered is shown in Figure \ref{res:tcp-table}.
%Evaluating the canonical TCP model using \korg led us to identify edge-cases in the connection establishment routine that weren't accounted for, leading us to construct a "revised" TCP model accounting for these missing edge cases. %Evaluating the canonical TCP model using \korg led us to identify edge-cases in the connection establishment routine that weren't accounted for, leading us to construct a "revised" TCP model accounting for these missing edge cases.
@@ -22,16 +27,13 @@ We evaluated the our TCP \promela model and the hand-written TCP \promela model
\begin{figure}[h!] \begin{figure}[h!]
\centering \centering
\begin{scriptsize} \begin{scriptsize}
\begin{tabular}{|c|c|c|c|c|c|c|} \begin{tabular}{|c|c|c|c|}
\hline \hline
& \multicolumn{2}{c|}{Drop Attacker} & \multicolumn{2}{c|}{Replay Attacker} & \multicolumn{2}{c|}{Reorder Attacker} \\ & Drop Attacker & Replay Attacker & Reorder Attacker\\\hline
\hline $\phi_1$ & & &\\
& Pacheco et al. & Ours & Pacheco et al. & Ours & Pacheco et al. & Ours \\ $\phi_2$ & x & x & \\
\hline $\phi_3$ & & &\\
$\phi_1$ & & & & & & \\ $\phi_4$ & & &\\
$\phi_2$ & x & x & x & x & & \\
$\phi_3$ & & & & & & \\
$\phi_4$ & & & & & x & \\
\hline \hline
\end{tabular} \end{tabular}
\end{scriptsize} \end{scriptsize}

0
sections/design.log Normal file
View File

80
sections/design.tex
View File

@@ -1,8 +1,11 @@
%!TEX root = ../main.tex
In this section we discuss the details behind the design, formal guarantees, implementation, and usage of \korg. In this section we discuss the details behind the design, formal guarantees, implementation, and usage of \korg.
\subsection{High-level design}% \subsection{High-level design}%
\label{sub:High-level design} \label{sub:High-level design}
\cnr{need introductory paragraph about program synthesis, the main idea}
At the highest level, \korg sits on user-specified communication channels in a program written in \promela, the modeling language of the \spin model checker. The user selects an attacker model of choice and correctness properties of choice. \korg then invokes \spin, which exhaustively searches for attacks with respect to the chosen attacker model, \promela model, and correctness property. At the highest level, \korg sits on user-specified communication channels in a program written in \promela, the modeling language of the \spin model checker. The user selects an attacker model of choice and correctness properties of choice. \korg then invokes \spin, which exhaustively searches for attacks with respect to the chosen attacker model, \promela model, and correctness property.
A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg_workflow}. A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg_workflow}.
@@ -16,48 +19,48 @@ A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg
\subsection{Supported Attacker Models}% \subsection{Supported Attacker Models}%
\label{sub:Supported Attacker Models} \label{sub:Supported Attacker Models}
\korg supports the automatic synthesis of attacks with respect to four general pre-defined attacker models applicable to any communication channel: %\korg supports the automatic synthesis of attacks with respect to four general pre-defined attacker models applicable to any communication channel:
\begin{itemize} %\begin{itemize}
\item \textbf{Drop Attacker Model}. Drop attackers are capable of dropping a finite number of messages off a channel. %\item \textbf{Drop Attacker Model}. Drop attackers are capable of dropping a finite number of messages off a channel.
\item \textbf{Replay Attacker Model}. Replay attackers are capable of replaying previously seen messages back onto a channel. %\item \textbf{Replay Attacker Model}. Replay attackers are capable of replaying previously seen messages back onto a channel.
\item \textbf{Reorder Attacker Model}. Reorder attackers are capable of reordering messages on a channel. %\item \textbf{Reorder Attacker Model}. Reorder attackers are capable of reordering messages on a channel.
\item \textbf{Insert Attacker Model}. Insert attackers are capable of inserting arbitrary messages (as specifiable by the user) onto a channel. %\item \textbf{Insert Attacker Model}. Insert attackers are capable of inserting arbitrary messages (as specifiable by the user) onto a channel.
\end{itemize} %\end{itemize}
\korg supports four general attacker model gadgets: an attacker that can drop, replay, reorder, or insert messages on a channel. In this section we discuss the various details that went into the implementation of the gadgets that encapsulate the behavior of the respective attacker models.
% Additionally, \korg supports user-defined attacker that insert arbitrary messages onto a channel. In this section we discuss the various details that go into each attacker model.
\textbf{Drop Attacker Model Gadget}
The most simple attacker model \korg supports is an attacker that can \textit{drop} messages from a channel. The user specifies a "drop limit" value that limits the number of packets the attacker can drop from the channel. Note, a higher drop limit will increase the search space of possible attacks, thereby increasing execution time.
The dropper attacker model gadget \korg synthesizes works as follows. The gadget will nondeterministically choose to observe a message on a channel. Then, if the drop limit variable is not zero, it will consume the message. An example is shown in Figure \ref{lst:korg_drop}.
\textbf{Replay Attacker Model Gadget}
The next attacker model \korg supports is an attacker that can observe and \textit{replay} messages back onto a channel. Similarly to the drop limit for the dropping attacker model, the user can specify a "replay limit" that caps the number of observed messages the attacker can replay back onto the specified channel.
The replay attacker model gadget \korg employs works as follows. The gadget has two states, \textsc{Consume} and \textsc{Replay}. The gadget starts in the \textsc{Consume} state and nondeterministically reads (but not consumes) messages on the target channel, sending them into a local storage buffer. Once the gadget read the number of messages on the channel equivalent to the defined replay limit, its state changes to \textsc{Replay}. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{lst:korg_replay}.
\textbf{Reorder Attacker Model Gadget}
\korg supports synthesizing attackers that can \textit{reorder} messages on a channel. Like the drop and replay attacker model gadgets, the user can specify a "reordering limit" that caps the number of messages that can be reordered by the attacker on the specified channel.
The reordering attacker model gadget \korg synthesizes works as follows. The gadget has three states, \textsc{Init}, \textsc{Consume}, and \textsc{Replay}. The gadget begins in the \textsc{Init} state, where it arbitrarily chooses a message to start consuming by transitioning to the \textsc{Consume} state. When in the \textsc{Consume} state, the gadget consumes all messages that appear on the channel, filling up a local buffer, until hitting the defined reordering limit. Once this limit is hit, the gadget transitions into the \textsc{Replay} state. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{lst:korg_reordering}.
\textbf{Insert Attacker Models}
\korg supports the synthesis of attackers that can simply insert messages onto a channel. While the drop, replay, and reordering attacker model gadgets as previously described have complex gadgets that \korg synthesizes with respect to a user-specified channel, the insert attacker model gadget is synthesized with respect to a user-defined \textit{IO-file}. This file denotes the specific outputs and channels the attacker is capable of sending, and \korg generates a gadget capable of synthesizing attacks using the given inputs. An example I/O file is given in Figure \ref{lst:io-file}, and the generated gadget is given in Figure \ref{lst:io-file-synth}.
These attacker models can be mixed and matched as desired by the \korg user. For example, a user can specify a drop attacker and replay attacker to target channel 1, a reordering attacker to target channel 2, and an insert attacker to target channel 3. If multiple attacker models are declared, \korg will synthesize attacks where the attackers on different channel \textit{coordinate} to construct a unifying attack. These attacker models can be mixed and matched as desired by the \korg user. For example, a user can specify a drop attacker and replay attacker to target channel 1, a reordering attacker to target channel 2, and an insert attacker to target channel 3. If multiple attacker models are declared, \korg will synthesize attacks where the attackers on different channel \textit{coordinate} to construct a unifying attack.
\subsection{Soundness And Completeness of Korg}% \input{sections/examples}
\label{sub:Soundness And Completeness}
\newcommand{\comp}{\mid\mid} % \korg also supports the synthesis of gadgets with respect to user-defined inputs and outputs. The user defines an \textit{IO-file} denoting the specific input and output messages the attacker is capable of sending, and \korg generates a gadget capable of synthesizing attacks with respect to the user's specification.
\newcommand{\ioint}{\mathcal{C}}
Fundamentally, the theoretical framework that \korg implements proposed by Hippel et al. reasons about \textit{communicating processes}; similarly, \korg is best understood as a synthesizer for attackers that sit \textit{between} communicating processes.
The theoretical attack synthesis framework and \korg use slightly different formalisms. Both employ derivations the general \textit{Input/Output (I/O) automata}, state machines whose transitions indicate sending or receiving a message.\footnote{
A fundamental assumption both \korg and the theoretical attack synthesis framework rely upon is unicast transition relations of I/O automata within this context. That is, if one sending automata has an output transition matching an input transition of two receiving automata, only one input/output transition pair can be composed upon. Model checkers for I/O automata such as \spin will explore both possibilities.
}
In particular, the theoretical attack synthesis framework defines their own notion of a \textit{process} and argues their attack synthesis algorithm maintains soundness and completeness guarantees with respect to it, while \korg relies upon \spin's preferred model checking formalism, the B\"uchi Automata. Both utilize linear temporal logic as their specification language of choice.
We ultimately seek to conclude \korg maintains the guarantees of the theoretical framework it implements, therefore it is necessary to demonstrate the equivalence of \textit{processes} from the theoretical attack synthesis framework with the B\"uchi Automata. For ease of reading and clarity, we only provide shortened narrations of the arguments here. The detailed, definitions, theorems, and proofs are provided in Appendix Section \ref{sub:korg_proofs}.
%\korg is an implementation of the theoretical attack synthesis framework proposed by Hippel et al. This framework enjoys soundness and completeness guarantees for attacks discovered; that is, if there exists an attack, it is discovered, and if an attack is discovered, it is valid. However, the attack synthesis framework proposed by Hippel et al. reasons about an abstracted, theoretical process construct. Therefore, in order to correctly claim \korg is also sound and complete, it is necessary to demonstrate discovering an attack within the theoretical framework reduces to the semantics of \spin, the model checker \korg is built on top of. %\korg is an implementation of the theoretical attack synthesis framework proposed by Hippel et al. This framework enjoys soundness and completeness guarantees for attacks discovered; that is, if there exists an attack, it is discovered, and if an attack is discovered, it is valid. However, the attack synthesis framework proposed by Hippel et al. reasons about an abstracted, theoretical process construct. Therefore, in order to correctly claim \korg is also sound and complete, it is necessary to demonstrate discovering an attack within the theoretical framework reduces to the semantics of \spin, the model checker \korg is built on top of.
%There exists a semantic gap between the theoretical attack synthesis framework proposed by Hippel et al., and the semantics of \korg. Therefore, in order to correctly claim \korg maintains the soundness and completeness of the theoretical framework it implements, it suffices to demonstrate finding an attack within the theoretical attack synthesis framework precisely reduces to the semantics of \spin. %There exists a semantic gap between the theoretical attack synthesis framework proposed by Hippel et al., and the semantics of \korg. Therefore, in order to correctly claim \korg maintains the soundness and completeness of the theoretical framework it implements, it suffices to demonstrate finding an attack within the theoretical attack synthesis framework precisely reduces to the semantics of \spin.
%the model checker \korg is implemented on top of. %the model checker \korg is implemented on top of.
\begin{theorem}
A process, as defined in Hippel et al., always directly corresponds to a B\"uchi Automata.
\end{theorem}
In short, a process in the theoretical attack synthesis framework is a Kripke Structure equipped with input and output transitions. That is, when composing two processes, an output transition must be matched to a respective input transition. Processes also include atomic propositions, which the given linear temporal logic specifications are defined over. We invoke and build on the well-known correspondence between Kripke Structures and \ba to show our desired correspondence.
\begin{theorem}
Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
\end{theorem}
Via the previous theorem, we can translate the threat model processes and the victim processes to \ba and intersect them. B\"uchi Automata intersection corresponds with \ba language inclusion, which is in turn solved by \spin. From this result, we naturally get a complexity-theoretic result for finding an attacker from a given threat model.
%\begin{proof} %\begin{proof}
%Recalling the definitions from Hippel et al., a \textit{process} is Kripke structure whose transitions are equipped additional input and output operations in the same flavor as a standard I/O automata.\footnote{Modeling processes in this way allows for the simultaneous modeling of message passing while also maintaining the ability to leverage Linear Temporal Logic for specification} %Recalling the definitions from Hippel et al., a \textit{process} is Kripke structure whose transitions are equipped additional input and output operations in the same flavor as a standard I/O automata.\footnote{Modeling processes in this way allows for the simultaneous modeling of message passing while also maintaining the ability to leverage Linear Temporal Logic for specification}
@@ -75,20 +78,12 @@ Via the previous theorem, we can translate the threat model processes and the vi
%\end{proof} %\end{proof}
\begin{theorem}
Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is PSPACE-complete.
\end{theorem}
By the previous argument the attack synthesis problem reduces to intersecting multiple \ba (or alternatively \ba language inclusion), which is well-known to be PSPACE-complete \cite{Kozen_1977}.
Although this result implies \korg has a rough upper bound complexity, in practice due the various implementation-level optimizations of \spin finding attacks on some property is generally fast, but proving their absence via a state-space search can expensive \cite{Clarke_Wang}.
Since \korg uses \spin as its underlying model checker, we can effectively conclude \korg is sound and complete.
%By the previous argument, the R-$\exists$ASP problem reduces to intersecting multiple \ba, which is well-known to be PSPACE-complete \cite{Kozen_1977}. %By the previous argument, the R-$\exists$ASP problem reduces to intersecting multiple \ba, which is well-known to be PSPACE-complete \cite{Kozen_1977}.
\subsection{The Korg Implementation}% \subsection{\korg Implementation}%
\label{sub:The Korg Implementation} \label{sub:impl}
We implemented \korg on top of the \spin, a popular and robust model checker for reasoning about distributed and concurrent systems. Intuitively, models written in \promela, the modeling language of \spin, are communicating state machines whose messages are passed over defined \textit{channels}. Channels in \promela can either be unbuffered \textit{synchronous} channels, or buffered \textit{asynchronous} channels. \korg generates attacks \textit{with respect} to these defined channels. We implemented \korg on top of the \spin, a popular and robust model checker for reasoning about distributed and concurrent systems. Intuitively, models written in \promela, the modeling language of \spin, are communicating state machines whose messages are passed over defined \textit{channels}. Channels in \promela can either be unbuffered \textit{synchronous} channels, or buffered \textit{asynchronous} channels. \korg generates attacks \textit{with respect} to these defined channels.
@@ -106,7 +101,7 @@ active proctype Peer2() {
} }
\end{lstlisting} \end{lstlisting}
\korg is designed to parse user-chosen channels and generate gadgets for sending, receiving, and manipulating messages on them. \korg has built-in gadgets that are designed to emulate various real-world attacker models, as further described in Section \ref{sec:usage_attacker_models}. \korg is designed to parse user-chosen channels and generate gadgets for sending, receiving, and manipulating messages on them. \korg has built-in gadgets that are designed to emulate various real-world attacker models.
%Additionally, users can explicitly define which messages a generated gadget can send and receive. %Additionally, users can explicitly define which messages a generated gadget can send and receive.
Once one or multiple gadgets are generated, \korg invokes \spin to check if a given property of interest remains satisfied in the presence of the attacker gadgets. Once one or multiple gadgets are generated, \korg invokes \spin to check if a given property of interest remains satisfied in the presence of the attacker gadgets.
@@ -114,8 +109,7 @@ Once one or multiple gadgets are generated, \korg invokes \spin to check if a gi
\label{sub:Usage} \label{sub:Usage}
To demonstrate the usage of \korg, we provide a step-by-step example of proving the alternate bit protocol (ABP) is secure with respect to attackers that can replay messages. ABP is a simple communication protocol that provides reliable communication between two peers over an unreliable communication by continually agreeing on a bit value.
To demonstrate the usage of \korg, we'll walk through an example of proving the alternate bit protocol (ABP) is secure with respect to attackers that can replay messages. ABP is a simple communication protocol that provides reliable communication between two peers over an unreliable communication by continually agreeing on a bit value.
To use \korg, the user first authors a \promela model and a correctness property in LTL. For example, take the \promela model as shown in Listing \ref{lst:abp}. The sender repeatedly sends its stored bit, \texttt{A\_curr}, to the receiver. The receiver changes its internal bit, \texttt{B\_curr}, and sends an acknowledgement to the sender. When the sender receives the acknowledgement, it will bitflip \texttt{A\_curr} and repeatedly send the updated bit. A natural specification for this protocol, formalized into the LTL property \texttt{eventually\_agrees}, states that if the sender and receiver do not currently agree on a bit, they eventually will be able to reach an agreement. To use \korg, the user first authors a \promela model and a correctness property in LTL. For example, take the \promela model as shown in Listing \ref{lst:abp}. The sender repeatedly sends its stored bit, \texttt{A\_curr}, to the receiver. The receiver changes its internal bit, \texttt{B\_curr}, and sends an acknowledgement to the sender. When the sender receives the acknowledgement, it will bitflip \texttt{A\_curr} and repeatedly send the updated bit. A natural specification for this protocol, formalized into the LTL property \texttt{eventually\_agrees}, states that if the sender and receiver do not currently agree on a bit, they eventually will be able to reach an agreement.
@@ -152,7 +146,7 @@ ltl eventually_agrees {
Next, the user selects a \textit{channel} to generate an attacker on, and an attacker model of choice. For example, we select \texttt{StoR} and \texttt{RtoS} as our channels of choice, \texttt{replay} as our attacker model of choice, and assume the ABP model is in the file \texttt{abp.pml}. Then, we run \korg via command line. Next, the user selects a \textit{channel} to generate an attacker on, and an attacker model of choice. For example, we select \texttt{StoR} and \texttt{RtoS} as our channels of choice, \texttt{replay} as our attacker model of choice, and assume the ABP model is in the file \texttt{abp.pml}. Then, we run \korg via command line.
\begin{lstlisting}[label={lst:korg-shell}] \begin{lstlisting}[label={lst:korg-shell}]
$ ./korg --model=abp.pml --attacker=replay --channel=StoR,RtoS --eval $ ./panda --model=abp.pml --attacker=replay --channel=StoR,RtoS --eval
\end{lstlisting} \end{lstlisting}
\korg will then modify the \texttt{abp.pml} file to include the \texttt{replay} attacker gadgets attacking channels \texttt{StoR} and \texttt{RtoS}, and model-check it with \spin. \korg outputs the following text, cut down for readability, indicating an exhaustive search for attacks: \korg will then modify the \texttt{abp.pml} file to include the \texttt{replay} attacker gadgets attacking channels \texttt{StoR} and \texttt{RtoS}, and model-check it with \spin. \korg outputs the following text, cut down for readability, indicating an exhaustive search for attacks:
@@ -162,7 +156,7 @@ Full statespace search for:
ltl eventually_agree ((A_curr!=B_curr))) implies (eventually ((A_curr==B_curr)) ltl eventually_agree ((A_curr!=B_curr))) implies (eventually ((A_curr==B_curr))
Korg's exhaustive search is complete, no attacks found! PANDA's exhaustive search is complete, no attacks found!
\end{lstlisting} \end{lstlisting}
If desired, \texttt{--output} can also be specified so the \korg-modified \texttt{abp.pml} can be more closely examined and modified. A full shell-script replicating this example is available in the artifact. If desired, \texttt{--output} can also be specified so the \korg-modified \texttt{abp.pml} can be more closely examined and modified. A full shell-script replicating this example is available in the artifact.

151
sections/examples.tex Normal file
View File

@@ -0,0 +1,151 @@
%\section{Attacker Model Gadget Examples}%
%\label{sub:Attacker Model Gadget Examples}
\begin{figure}[h]
\begin{lstlisting}[caption={Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}, label={lst:korg_drop}]
chan cn = [8] of { int, int, int };
active proctype attacker_drop() {
int b_0, b_1, b_2;
byte lim = 3; // drop limit
MAIN:
do
:: cn ? [b_0, b_1, b_2] -> atomic {
if
:: lim == 0 -> goto BREAK;
:: else ->
cn ? b_0, b_1, b_2; // consume message on the channel
lim = lim - 1;
goto MAIN;
fi
}
od
BREAK:
}
\end{lstlisting}
\end{figure}
\begin{figure}[h]
\begin{lstlisting}[caption={Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_replay}]
chan cn = [8] of { int, int, int };
// local memory for the gadget
chan gadget_mem = [3] of { int, int, int };
active proctype attacker_replay() {
int b_0, b_1, b_2;
int i = 3;
CONSUME:
do
// read messages until the limit is passed
:: cn ? [b_0, b_1, b_2] -> atomic {
cn ? <b_0, b_1, b_2> -> gadget_mem ! b_0, b_1, b_2;
i--;
if
:: i == 0 -> goto REPLAY;
:: i != 0 -> goto CONSUME;
fi
}
od
REPLAY:
do
:: atomic {
// nondeterministically select a random value from the storage buffer
int am;
select(am : 0 .. len(gadget_mem)-1);
do
:: am != 0 ->
am = am-1;
gadget_mem ? b_0, b_1, b_2 -> gadget_mem ! b_0, b_1, b_2;
:: am == 0 ->
gadget_mem ? b_0, b_1, b_2 -> cn ! b_0, b_1, b_2;
break;
od
}
// doesn't need to use all messages on the channel
:: atomic {gadget_mem ? b_0, b_1, b_2; }
// once mem has no more messages, we're done
:: empty(gadget_mem) -> goto BREAK;
od
BREAK:
}
\end{lstlisting}
\end{figure}
\begin{figure}[h]
\begin{lstlisting}[caption={Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_reordering}]
chan cn = [8] of { int, int, int };
chan gadget_mem = [3] of { int, int, int };
active proctype attacker_reordering() priority 255 {
byte b_0, b_1, b_2, blocker;
int i = 3;
INIT:
do
// arbitrarily choose a message to start consuming on
:: {
blocker = len(cn);
do
:: b != len(c) -> goto INIT;
od
}
:: goto CONSUME;
od
CONSUME:
do
// consume messages with high priority
:: c ? [b_0] -> atomic {
c ? b_0 -> gadget_mem ! b_0;
i--;
if
:: i == 0 -> goto REPLAY;
:: i != 0 -> goto CONSUME;
fi
}
od
REPLAY:
do
// replay messages back onto the channel, also with priority
:: atomic {
int am;
select(am : 0 .. len(gadget_mem)-1);
do
:: am != 0 ->
am = am-1;
gadget_mem ? b_0 -> attacker_mem_0 ! b_0;
:: am == 0 ->
gadget_mem ? b_0 -> c ! b_0;
break;
od
}
:: atomic { empty(gadget_mem) -> goto BREAK; }
od
BREAK:
}
\end{lstlisting}
\end{figure}
\begin{figure}[h]
\begin{lstlisting}[caption={Example I/O file targetting channel "cn"}, label={lst:io-file}]
cn:
I:
O:1-1-1, 1-2-3, 3-4-5
\end{lstlisting}
\begin{lstlisting}[caption={Example gadget synthesized from an I/O file targetting the channel "cn"}, label={lst:io-file-synth}]
chan cn = [8] of { int, int, int };
active proctype daisy() {
INIT:
do
:: cn ! 1,1,1;
:: cn ! 1,2,3;
:: cn ! 3,4,5;
:: goto RECOVERY;
od
RECOVERY:
}
\end{lstlisting}
\end{figure}

0
sections/introduction.log Normal file
View File

4
sections/introduction.tex
View File

@@ -1,4 +1,6 @@
%!TEX root = ../main.tex
Distributed protocols are the foundation for the modern internet, and therefore ensuring their correctness and security is paramount. To this end, formal methods, the use of mathematically rigorous techniques for reasoning about software, has been increasingly employed to analyze and study distributed protocols. Historically, formal methods has been employed for reasoning about concurrency and distributed algorithms \cite{Lamport_1994, Holzmann_1997, Clarke_Wang}, and in recent years formal methods have been employed at scale to reason about the security of cryptographic protocols and primitives \cite{Basin_Cremers_Dreier_Sasse_2022, Blanchet_Smyth_Cheval_Sylvestre, Kobeissi_Nicolas_Tiwari, Blanchet_Jacomme, Basin_Linker_Sasse}. Distributed protocols are the foundation for the modern internet, and therefore ensuring their correctness and security is paramount. To this end, formal methods, the use of mathematically rigorous techniques for reasoning about software, has been increasingly employed to analyze and study distributed protocols. Historically, formal methods has been employed for reasoning about concurrency and distributed algorithms \cite{Lamport_1994, Holzmann_1997, Clarke_Wang}, and in recent years formal methods have been employed at scale to reason about the security of cryptographic protocols and primitives \cite{Basin_Cremers_Dreier_Sasse_2022, Blanchet_Smyth_Cheval_Sylvestre, Kobeissi_Nicolas_Tiwari, Blanchet_Jacomme, Basin_Linker_Sasse}.
This myriad of formal methods tooling applicable to secure protocols has enabled reasoning about security-relevant properties involving secrecy, authentication, indistinguishability in addition to concurrency, safety, and liveness. However, no previous formal methods tooling offered an effective solution for rigorously studying an attacker that controls communication channels. That is, how do you reason about an attacker that can arbitrarily drop, reorder, replay, or insert messages onto a communication channel? This myriad of formal methods tooling applicable to secure protocols has enabled reasoning about security-relevant properties involving secrecy, authentication, indistinguishability in addition to concurrency, safety, and liveness. However, no previous formal methods tooling offered an effective solution for rigorously studying an attacker that controls communication channels. That is, how do you reason about an attacker that can arbitrarily drop, reorder, replay, or insert messages onto a communication channel?
To fill this gap, we introduce \korg, a tool for synthesizing attacks on distributed protocols that implements the theoretical framework proposed in Hippel et al. \cite{Hippel2022}. In particular, \korg targets the communication channels between the protocol endpoints, and synthesizes attacks to violate arbitrary linear temporal logic (LTL) specifications. \korg either synthesizes attack, or proves the absence of such via an exhaustive state-space search. \korg is sound and complete, meaning if there exists an attack \korg will find it, and \korg will never have false positives. \korg supports pre-defined attacker models, including attackers that can replay, reorder, or drop messages on channels, as well as custom user-defined attacker models. Although \korg best lends itself for reasoning about denial of service attacks, it can target any specification expressable in LTL. We present a variety of case studies illustrating the employability and usefulness of \korg. To fill this gap, we introduce \korg \footnote{\korg is a fictitious name for our system, for double-blind submission.}, a tool for synthesizing attacks on distributed protocols that implements and extends the theoretical framework proposed in \cite{Hippel2022_anonym}. In particular, \korg targets the communication channels between the protocol endpoints, and synthesizes attacks to violate arbitrary linear temporal logic (LTL) specifications. \korg either synthesizes attack, or proves the absence of such via an exhaustive state-space search. \korg is sound and complete, meaning if there exists an attack \korg will find it, and \korg will never have false positives. \korg supports pre-defined attacker models, including attackers that can replay, reorder, or drop messages on channels, as well as custom user-defined attacker models. Although \korg best lends itself for reasoning about denial of service attacks, it can target any specification expressable in LTL. We present several case studies illustrating the usefulness of \korg. We release our code as our models as open source at \cnr{here add the anonymous link}.

36
sections/proofs.tex Normal file
View File

@@ -0,0 +1,36 @@
\subsection{Soundness And Completeness of \korg}%
\label{sub:Soundness And Completeness}
\newcommand{\comp}{\mid\mid}
\newcommand{\ioint}{\mathcal{C}}
Fundamentally, the theoretical framework that \korg implements was presented in \cite{Hippel2022_anoym} about \textit{communicating processes}; similarly, \korg is best understood as a synthesizer for attackers that sit \textit{between} communicating processes.
The theoretical attack synthesis framework and \korg use slightly different formalisms. Both employ derivations the general \textit{Input/Output (I/O) automata}, state machines whose transitions indicate sending or receiving a message.\footnote{
A fundamental assumption both \korg and the theoretical attack synthesis framework rely upon is unicast transition relations of I/O automata within this context. That is, if one sending automata has an output transition matching an input transition of two receiving automata, only one input/output transition pair can be composed upon. Model checkers for I/O automata such as \spin will explore both possibilities.
}
In particular, the theoretical attack synthesis framework defines their own notion of a \textit{process} and argues their attack synthesis algorithm maintains soundness and completeness guarantees with respect to it, while \korg relies upon \spin's preferred model checking formalism, the B\"uchi Automata. Both utilize linear temporal logic as their specification language of choice.
We ultimately seek to conclude \korg maintains the guarantees of the theoretical framework it implements, therefore it is necessary to demonstrate the equivalence of \textit{processes} from the theoretical attack synthesis framework with the B\"uchi Automata. For ease of reading and clarity, we only provide shortened narrations of the arguments here. The detailed, definitions, theorems, and proofs are provided in Appendix Section \ref{sub:korg_proofs}.
\begin{theorem}
A process, always directly corresponds to a B\"uchi Automata.
\end{theorem}
In short, a process in the theoretical attack synthesis framework is a Kripke Structure equipped with input and output transitions. That is, when composing two processes, an output transition must be matched to a respective input transition. Processes also include atomic propositions, which the given linear temporal logic specifications are defined over. We invoke and build on the well-known correspondence between Kripke Structures and \ba to show our desired correspondence.
\begin{theorem}
Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
\end{theorem}
Via the previous theorem, we can translate the threat model processes and the victim processes to \ba and intersect them. B\"uchi Automata intersection corresponds with \ba language inclusion, which is in turn solved by \spin. From this result, we naturally get a complexity-theoretic result for finding an attacker from a given threat model.
\begin{theorem}
Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is PSPACE-complete.
\end{theorem}
By the previous argument the attack synthesis problem reduces to intersecting multiple \ba (or alternatively \ba language inclusion), which is well-known to be PSPACE-complete \cite{Kozen_1977}.
Although this result implies \korg has a rough upper bound complexity, in practice due the various implementation-level optimizations of \spin finding attacks on some property is generally fast, but proving their absence via a state-space search can expensive \cite{Clarke_Wang}.
Since \korg uses \spin as its underlying model checker, we can effectively conclude \korg is sound and complete.