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

more

Browse Source
This commit is contained in:
Your Name
2025-03-04 16:28:39 -05:00
parent 5d4ea50fb3
commit d5f7fff2a7
11 changed files with 2360 additions and 2186 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4017
.latexrun.db
View File

File diff suppressed because it is too large Load Diff

54
main.aux
View File

@@ -43,14 +43,14 @@
\newlabel{lst:korg_replay}{{6}{4}{Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{figure.caption.6}{}} \newlabel{lst:korg_replay}{{6}{4}{Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{figure.caption.6}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}}{5}{figure.caption.7}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}}{5}{figure.caption.7}\protected@file@percent }
\newlabel{lst:korg_reordering}{{7}{5}{Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{figure.caption.7}{}} \newlabel{lst:korg_reordering}{{7}{5}{Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{figure.caption.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Usage}{5}{subsection.3.3}\protected@file@percent }
\newlabel{sub:Usage}{{3.3}{5}{Usage}{subsection.3.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} \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}
\citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson} \citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Usage}{6}{subsection.3.3}\protected@file@percent }
\newlabel{sub:Usage}{{3.3}{6}{Usage}{subsection.3.3}{}}
\newlabel{lst:abp}{{2}{6}{Example (simplified) \promela model of the alternating bit protocol}{lstlisting.2}{}} \newlabel{lst:abp}{{2}{6}{Example (simplified) \promela model of the alternating bit protocol}{lstlisting.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}{\ignorespaces Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}}{6}{lstlisting.2}\protected@file@percent } \@writefile{lol}{\contentsline {lstlisting}{\numberline {2}{\ignorespaces Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}}{6}{lstlisting.2}\protected@file@percent }
\newlabel{lst:korg-shell}{{3.3}{6}{}{lstlisting.-5}{}} \newlabel{lst:korg-shell}{{3.3}{6}{}{lstlisting.-5}{}}
@@ -58,38 +58,26 @@
\newlabel{sec:case_studies}{{4}{6}{Case Studies}{section.4}{}} \newlabel{sec:case_studies}{{4}{6}{Case Studies}{section.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}TCP}{6}{subsection.4.1}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {4.1}TCP}{6}{subsection.4.1}\protected@file@percent }
\newlabel{sub:TCP}{{4.1}{6}{TCP}{subsection.4.1}{}} \newlabel{sub:TCP}{{4.1}{6}{TCP}{subsection.4.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Raft}{6}{subsection.4.2}\protected@file@percent }
\newlabel{sub:Raft}{{4.2}{6}{Raft}{subsection.4.2}{}}
\citation{Ongaro} \citation{Ongaro}
\citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
\citation{Ginesin2024} \citation{Ginesin2024}
\citation{rfc9260} \citation{rfc9260}
\citation{Kobeissi_Nicolas_Tiwari,Proverif,Tamarin,Cremers}
\citation{Blanchet_Jacomme,Pereira}
\citation{ParnoSOK,Basin_Cremers_Meadows_2018}
\citation{Khan_Mukund_Suresh_2005,Clarke_Wang,wayne_adversaries,Narayana_Chen_Zhao_Chen_Fu_Zhou_2006,Delzanno_Tatarek_Traverso_2014}
\newlabel{res:tcp-table}{{\caption@xref {res:tcp-table}{ on input line 28}}{7}{TCP}{figure.caption.8}{}} \newlabel{res:tcp-table}{{\caption@xref {res:tcp-table}{ on input line 28}}{7}{TCP}{figure.caption.8}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Automatically discovered attacks against our TCP model 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. These experiments were ran on a laptop with an eighth generation i7 and 16gb of memory. Full attack traces are available in the artifact.}}{7}{figure.caption.8}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Automatically discovered attacks against our TCP model 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. These experiments were ran on a laptop with an eighth generation i7 and 16gb of memory. Full attack traces are available in the artifact.}}{7}{figure.caption.8}\protected@file@percent }
\newlabel{res:tcp-table}{{8}{7}{Automatically discovered attacks against our TCP model for $\phi _1$ through $\phi _4$. "x" indicates an attack was discovered, and no "x" indicates \korg proved the absence of an attack via an exhaustive search. These experiments were ran on a laptop with an eighth generation i7 and 16gb of memory. Full attack traces are available in the artifact}{figure.caption.8}{}} \newlabel{res:tcp-table}{{8}{7}{Automatically discovered attacks against our TCP model for $\phi _1$ through $\phi _4$. "x" indicates an attack was discovered, and no "x" indicates \korg proved the absence of an attack via an exhaustive search. These experiments were ran on a laptop with an eighth generation i7 and 16gb of memory. Full attack traces are available in the artifact}{figure.caption.8}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Raft}{7}{subsection.4.2}\protected@file@percent }
\newlabel{sub:Raft}{{4.2}{7}{Raft}{subsection.4.2}{}}
\newlabel{res:raft_table}{{\caption@xref {res:raft_table}{ on input line 91}}{7}{Raft}{figure.caption.9}{}} \newlabel{res:raft_table}{{\caption@xref {res:raft_table}{ on input line 91}}{7}{Raft}{figure.caption.9}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Breakdown of the attacker scenarios assessed with \textsc {Panda}\xspace against our buggy Raft \textsc {Promela}\xspace model, \texttt {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \textsc {Panda}\xspace synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact.}}{7}{figure.caption.9}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Breakdown of the attacker scenarios assessed with \textsc {Panda}\xspace against our buggy Raft \textsc {Promela}\xspace model, \texttt {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \textsc {Panda}\xspace synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact.}}{7}{figure.caption.9}\protected@file@percent }
\newlabel{res:raft_table}{{9}{7}{Breakdown of the attacker scenarios assessed with \korg against our buggy Raft \promela model, \texttt {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \korg synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact}{figure.caption.9}{}} \newlabel{res:raft_table}{{9}{7}{Breakdown of the attacker scenarios assessed with \korg against our buggy Raft \promela model, \texttt {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \korg synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact}{figure.caption.9}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}SCTP}{7}{subsection.4.3}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {4.3}SCTP}{7}{subsection.4.3}\protected@file@percent }
\newlabel{sub:SCTP}{{4.3}{7}{SCTP}{subsection.4.3}{}} \newlabel{sub:SCTP}{{4.3}{7}{SCTP}{subsection.4.3}{}}
\citation{Hippel2022} \@writefile{toc}{\contentsline {section}{\numberline {5}Related Work}{7}{section.5}\protected@file@percent }
\citation{Hippel2022} \newlabel{sec:Related Work}{{5}{7}{Related Work}{section.5}{}}
\citation{Hippel2022}
\citation{Hippel2022}
\@writefile{toc}{\contentsline {section}{\numberline {5}Theoretical Foundations of \textsc {Panda}\xspace }{8}{section.5}\protected@file@percent }
\newlabel{sec:proofs}{{5}{8}{Theoretical Foundations of \korg }{section.5}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Mathematical Preliminaries}{8}{subsection.5.1}\protected@file@percent }
\newlabel{sub:Mathematical Preliminaries}{{5.1}{8}{Mathematical Preliminaries}{subsection.5.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Proofs of Soundness and Completeness}{8}{subsection.5.2}\protected@file@percent }
\newlabel{sub:Proofs of Soundness and Completeness}{{5.2}{8}{Proofs of Soundness and Completeness}{subsection.5.2}{}}
\citation{Hippel2022}
\citation{Holzmann_1997}
\citation{Hippel2022}
\citation{Kozen_1977}
\citation{Kobeissi_Nicolas_Tiwari,Proverif,Tamarin,Cremers}
\citation{Blanchet_Jacomme,Pereira}
\citation{ParnoSOK,Basin_Cremers_Meadows_2018}
\citation{Khan_Mukund_Suresh_2005,Clarke_Wang,wayne_adversaries,Narayana_Chen_Zhao_Chen_Fu_Zhou_2006,Delzanno_Tatarek_Traverso_2014}
\citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Castro_Liskov_2002,Delzanno_Tatarek_Traverso_2014} \citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Castro_Liskov_2002,Delzanno_Tatarek_Traverso_2014}
\citation{Henda} \citation{Henda}
\citation{Ginesin} \citation{Ginesin}
@@ -98,10 +86,6 @@
\bibstyle{plain} \bibstyle{plain}
\bibdata{main} \bibdata{main}
\bibcite{Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021}{1} \bibcite{Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021}{1}
\@writefile{toc}{\contentsline {section}{\numberline {6}Related Work}{9}{section.6}\protected@file@percent }
\newlabel{sec:Related Work}{{6}{9}{Related Work}{section.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion}{9}{section.7}\protected@file@percent }
\newlabel{sec:conclusion}{{7}{9}{Conclusion}{section.7}{}}
\bibcite{ParnoSOK}{2} \bibcite{ParnoSOK}{2}
\bibcite{Tamarin}{3} \bibcite{Tamarin}{3}
\bibcite{Basin_Cremers_Meadows_2018}{4} \bibcite{Basin_Cremers_Meadows_2018}{4}
@@ -118,6 +102,8 @@
\bibcite{Ginesin2024}{15} \bibcite{Ginesin2024}{15}
\bibcite{Ginesin}{16} \bibcite{Ginesin}{16}
\bibcite{ironfleet}{17} \bibcite{ironfleet}{17}
\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusion}{8}{section.6}\protected@file@percent }
\newlabel{sec:conclusion}{{6}{8}{Conclusion}{section.6}{}}
\bibcite{Holzmann_2014}{18} \bibcite{Holzmann_2014}{18}
\bibcite{Holzmann_Smith_2000}{19} \bibcite{Holzmann_Smith_2000}{19}
\bibcite{Holzmann_1997}{20} \bibcite{Holzmann_1997}{20}
@@ -141,4 +127,20 @@
\bibcite{wayne_adversaries}{38} \bibcite{wayne_adversaries}{38}
\bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{39} \bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{39}
\bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{40} \bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{40}
\citation{Hippel2022}
\citation{Hippel2022}
\citation{Hippel2022}
\citation{Hippel2022}
\@writefile{toc}{\contentsline {section}{\numberline {7}Appendix}{10}{section.7}\protected@file@percent }
\newlabel{sec:appendix}{{7}{10}{Appendix}{section.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Mathematical Preliminaries}{10}{subsection.7.1}\protected@file@percent }
\newlabel{sub:Mathematical Preliminaries}{{7.1}{10}{Mathematical Preliminaries}{subsection.7.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2}Arguments for \textsc {Panda}\xspace 's Soundness, Completeness, and Complexity}{10}{subsection.7.2}\protected@file@percent }
\newlabel{sub:Proofs of Soundness and Completeness}{{7.2}{10}{Arguments for \korg 's Soundness, Completeness, and Complexity}{subsection.7.2}{}}
\citation{Hippel2022}
\citation{Holzmann_1997}
\citation{Hippel2022}
\citation{Kozen_1977}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3}Priorities \& On-the-fly B\"uchi Automata Composition}{11}{subsection.7.3}\protected@file@percent }
\newlabel{sub:Priority \& On-the-fly B\"uchi Automata Composition}{{7.3}{11}{Priorities \& On-the-fly B\"uchi Automata Composition}{subsection.7.3}{}}
\gdef \@abspage@last{11} \gdef \@abspage@last{11}

77
main.blg
View File

@@ -1,77 +0,0 @@
This is BibTeX, Version 0.99d (TeX Live 2024/Arch Linux)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux
The style file: plain.bst
Database file #1: main.bib
Warning--can't use both author and editor fields in Basin_Cremers_Meadows_2018
Warning--empty journal in Beurdouche
Warning--empty year in Beurdouche
Warning--empty journal in Blanchet_Jacomme
Warning--empty year in Blanchet_Jacomme
Warning--empty journal in Proverif
Warning--empty year in Proverif
Warning--can't use both author and editor fields in mCRL2
Warning--empty journal in Clarke_Wang
Warning--empty year in Clarke_Wang
Warning--can't use both author and editor fields in Cremers
Warning--empty journal in Ginesin2024
Warning--there's a number but no volume in Ginesin2024
Warning--empty journal in Ginesin
Warning--there's a number but no volume in Ginesin
Warning--can't use both author and editor fields in Hsieh_Mitra_2019
Warning--can't use both author and editor fields in Khan_Mukund_Suresh_2005
Warning--empty journal in Kobeissi_Nicolas_Tiwari
Warning--empty year in Kobeissi_Nicolas_Tiwari
Warning--empty journal in Ongaro
Warning--empty year in Ongaro
Warning--empty journal in Ongaro_Ousterhout
Warning--empty year in Ongaro_Ousterhout
Warning--empty journal in Pereira
Warning--empty year in Pereira
Warning--can't use both author and editor fields in Rahli_Vukotic_Völp_Esteves-Verissimo_2018
Warning--empty journal in Hippel2022
Warning--there's a number but no volume in Hippel2022
Warning--empty journal in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson
Warning--empty year in Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson
You've used 40 entries,
2118 wiz_defined-function locations,
755 strings with 11797 characters,
and the built_in function-call counts, 15500 in all, are:
= -- 1511
> -- 784
< -- 21
+ -- 315
- -- 270
* -- 1031
:= -- 2398
add.period$ -- 124
call.type$ -- 40
change.case$ -- 249
chr.to.int$ -- 0
cite$ -- 70
duplicate$ -- 730
empty$ -- 1067
format.name$ -- 270
if$ -- 3376
int.to.chr$ -- 0
int.to.str$ -- 40
missing$ -- 42
newline$ -- 198
num.names$ -- 80
pop$ -- 343
preamble$ -- 1
purify$ -- 215
quote$ -- 0
skip$ -- 616
stack$ -- 0
substring$ -- 617
swap$ -- 312
text.length$ -- 21
text.prefix$ -- 0
top$ -- 0
type$ -- 148
warning$ -- 30
while$ -- 103
width$ -- 42
write$ -- 436
(There were 30 warnings)

45
main.fls
View File

@@ -613,10 +613,6 @@ INPUT ./figures/replay.tex
INPUT ./figures/replay.tex INPUT ./figures/replay.tex
INPUT ./figures/replay.tex INPUT ./figures/replay.tex
INPUT ./figures/replay.tex INPUT ./figures/replay.tex
INPUT /usr/share/texmf-dist/fonts/vf/public/pslatex/pcrr8tn.vf
INPUT /usr/share/texmf-dist/fonts/tfm/public/pslatex/pcrr8rn.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmb8t.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT ./figures/reorder.tex INPUT ./figures/reorder.tex
INPUT ./figures/reorder.tex INPUT ./figures/reorder.tex
INPUT ./figures/reorder.tex INPUT ./figures/reorder.tex
@@ -624,6 +620,10 @@ INPUT ./figures/reorder.tex
INPUT ./figures/reorder.tex INPUT ./figures/reorder.tex
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8t.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8t.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/pslatex/pcrr8tn.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/pslatex/pcrr8tn.tfm
INPUT /usr/share/texmf-dist/fonts/vf/public/pslatex/pcrr8tn.vf
INPUT /usr/share/texmf-dist/fonts/tfm/public/pslatex/pcrr8rn.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmb8t.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmbc8t.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmbc8t.tfm
INPUT ./sections/design.tex INPUT ./sections/design.tex
INPUT ./sections/design.tex INPUT ./sections/design.tex
@@ -661,11 +661,11 @@ INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf
INPUT ./sections/proofs.tex INPUT ./sections/related_work.tex
INPUT ./sections/proofs.tex INPUT ./sections/related_work.tex
INPUT ./sections/proofs.tex INPUT ./sections/related_work.tex
INPUT ./sections/proofs.tex INPUT ./sections/related_work.tex
INPUT ./sections/proofs.tex INPUT ./sections/related_work.tex
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr8t.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr8t.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmrm.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmrm.vf
@@ -676,6 +676,19 @@ INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./main.bbl
INPUT ./main.bbl
INPUT ./main.bbl
INPUT ./sections/appendix-revised.tex
INPUT ./sections/appendix-revised.tex
INPUT ./sections/appendix-revised.tex
INPUT ./sections/appendix-revised.tex
INPUT ./sections/appendix-revised.tex
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zpzccmry.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zpzccmry.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/zapfchan/pzcmi8r.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/zapfchan/pzcmi8r.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmrm.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmrm.vf
@@ -689,19 +702,6 @@ INPUT /usr/share/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex9.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmrc8t.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmrc8t.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmrc8t.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmrc8t.tfm
INPUT ./sections/related_work.tex
INPUT ./sections/related_work.tex
INPUT ./sections/related_work.tex
INPUT ./sections/related_work.tex
INPUT ./sections/related_work.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./sections/conclusion.tex
INPUT ./main.bbl
INPUT ./main.bbl
INPUT ./main.bbl
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/zptmcmr.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /usr/share/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
@@ -712,6 +712,7 @@ INPUT ./main.aux
INPUT ./main.out INPUT ./main.out
INPUT ./main.out INPUT ./main.out
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cmextra/cmex9.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb

142
main.log
View File

@@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.7.2) 3 MAR 2025 23:52 This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.7.2) 4 MAR 2025 16:22
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
%&-line parsing enabled. %&-line parsing enabled.
@@ -1264,6 +1264,22 @@ LaTeX Warning: Label `res:tcp-table' multiply defined.
LaTeX Warning: Label `res:raft_table' multiply defined. LaTeX Warning: Label `res:raft_table' multiply defined.
! Missing \endcsname inserted.
<to be read again>
\&
l.145 ... Automata Composition}{subsection.7.3}{}}
The control sequence marked <to be read again> should
not appear between \csname and \endcsname.
! Missing \endcsname inserted.
<to be read again>
\&
l.145 ... Automata Composition}{subsection.7.3}{}}
The control sequence marked <to be read again> should
not appear between \csname and \endcsname.
) )
\openout1 = `main.aux'. \openout1 = `main.aux'.
@@ -1432,13 +1448,13 @@ Excluding 'comment' comment.) (./sections/gadgets.tex (./figures/drop.tex
LaTeX Warning: `h' float specifier changed to `ht'. LaTeX Warning: `h' float specifier changed to `ht'.
) (./figures/replay.tex) [2] (./figures/reorder.tex ) (./figures/replay.tex) (./figures/reorder.tex
Overfull \hbox (18.32658pt too wide) in paragraph at lines 33--34 Overfull \hbox (18.32658pt too wide) in paragraph at lines 33--34
[][] [][]
[] []
)) (./sections/design.tex [2])) (./sections/design.tex
<assets/diagram3.png, id=119, 733.99219pt x 277.035pt> <assets/diagram3.png, id=122, 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 23. Package pdftex.def Info: assets/diagram3.png used on input line 23.
@@ -1453,19 +1469,18 @@ LaTeX Warning: `h' float specifier changed to `ht'.
Package hyperref Info: bookmark level for unknown lstlisting defaults to 0 on i Package hyperref Info: bookmark level for unknown lstlisting defaults to 0 on i
nput line 78. nput line 78.
[3 <./assets/diagram3.png (PNG copy)>] [4] [3 <./assets/diagram3.png (PNG copy)>]
LaTeX Warning: `h' float specifier changed to `ht'. LaTeX Warning: `h' float specifier changed to `ht'.
LaTeX Warning: Reference `lst:drop_passer' on page 5 undefined on input line 28
5.
Underfull \vbox (badness 10000) has occurred while \output is active [] Underfull \vbox (badness 10000) has occurred while \output is active []
[5] [4]
Excluding 'comment' comment.) (./sections/case_studies.tex
LaTeX Warning: `h' float specifier changed to `ht'.
[5] Excluding 'comment' comment.) (./sections/case_studies.tex
Underfull \hbox (badness 10000) in paragraph at lines 19--19 Underfull \hbox (badness 10000) in paragraph at lines 19--19
[]\T1/pcr/m/n/10 SYN_RECEIVED \T1/ptm/m/n/10 (+20) is even-tu-ally fol-lowed by []\T1/pcr/m/n/10 SYN_RECEIVED \T1/ptm/m/n/10 (+20) is even-tu-ally fol-lowed by
@@ -1497,18 +1512,28 @@ Underfull \hbox (badness 1043) in paragraph at lines 107--107
nst our buggy Raft \T1/ptm/m/sc/10 (+20) Promela \T1/ptm/m/n/10 (+20) model, nst our buggy Raft \T1/ptm/m/sc/10 (+20) Promela \T1/ptm/m/n/10 (+20) model,
[] []
) (./sections/proofs.tex
Underfull \vbox (badness 2617) has occurred while \output is active []
[7] LaTeX Warning: `!h' float specifier changed to `!ht'.
Underfull \hbox (badness 4467) in paragraph at lines 35--36
) (./sections/related_work.tex [7]) (./sections/conclusion.tex) (./main.bbl
Underfull \hbox (badness 2126) in paragraph at lines 79--83
[]\T1/ptm/m/n/10 (+20) Giorgio Delzanno, Michele Tatarek, and Ric-cardo
[]
[8]
Underfull \hbox (badness 1810) in paragraph at lines 198--202
[]\T1/ptm/m/n/10 (+20) M. T<>xen, R. Stew-art, K. Nielsen, R. Je-sup, and
[]
) (./sections/appendix-revised.tex [9]
Underfull \hbox (badness 4467) in paragraph at lines 33--34
[][]\T1/ptm/b/n/10 (+20) Definition 2 \T1/ptm/m/n/10 (+20) (Pro-cess)\T1/ptm/b/ [][]\T1/ptm/b/n/10 (+20) Definition 2 \T1/ptm/m/n/10 (+20) (Pro-cess)\T1/ptm/b/
n/10 (+20) . []\T1/ptm/m/it/10 (+20) A \T1/ptm/m/n/10 (+20) Pro-cess \T1/ptm/m/ n/10 (+20) . []\T1/ptm/m/it/10 (+20) A \T1/ptm/m/n/10 (+20) Pro-cess \T1/ptm/m/
it/10 (+20) is a tu-ple $\OML/ptmcm/m/it/10 P \OT1/ptmcm/m/n/10 = it/10 (+20) is a tu-ple $\OML/ptmcm/m/it/10 P \OT1/ptmcm/m/n/10 =
[] []
[8] [10]
Underfull \hbox (badness 6575) in paragraph at lines 89--90 Underfull \hbox (badness 6575) in paragraph at lines 87--88
[]\T1/ptm/m/n/10 (+20) In the Pro-cess: $\OML/ptmcm/m/it/10 s[]; s[]; s[]; []$ []\T1/ptm/m/n/10 (+20) In the Pro-cess: $\OML/ptmcm/m/it/10 s[]; s[]; s[]; []$
\T1/ptm/m/n/10 (+20) with $\OML/ptmcm/m/it/10 s[] \OT1/ptmcm/m/n/10 = \OML/ptmc \T1/ptm/m/n/10 (+20) with $\OML/ptmcm/m/it/10 s[] \OT1/ptmcm/m/n/10 = \OML/ptmc
m/m/it/10 s[]$ \T1/ptm/m/n/10 (+20) and m/m/it/10 s[]$ \T1/ptm/m/n/10 (+20) and
@@ -1516,51 +1541,67 @@ m/m/it/10 s[]$ \T1/ptm/m/n/10 (+20) and
LaTeX Font Warning: Font shape `T1/ptm/m/scit' undefined LaTeX Font Warning: Font shape `T1/ptm/m/scit' undefined
(Font) using `T1/ptm/m/sc' instead on input line 106. (Font) using `T1/ptm/m/sc' instead on input line 104.
Underfull \hbox (badness 1132) in paragraph at lines 113--115 Underfull \hbox (badness 1132) in paragraph at lines 111--113
\T1/ptm/m/n/10 (+20) tents of this proof, equiv-a-lent to a pro-cess. There-for \T1/ptm/m/n/10 (+20) tents of this proof, equiv-a-lent to a pro-cess. There-for
e, e,
[] []
Underfull \hbox (badness 1043) in paragraph at lines 113--115 Underfull \hbox (badness 1043) in paragraph at lines 111--113
\T1/ptm/m/n/10 (+20) via the pre-vi-ous the-o-rem we can con-struct B<>chi Au- \T1/ptm/m/n/10 (+20) via the pre-vi-ous the-o-rem we can con-struct B<>chi Au-
[] []
) (./sections/related_work.tex) (./sections/conclusion.tex) (./main.bbl ! Undefined control sequence.
[9] l.144 ...constructing it in memory. Recall the \BA
Underfull \hbox (badness 2126) in paragraph at lines 79--83 is defined as a 5-tuple (...
[]\T1/ptm/m/n/10 (+20) Giorgio Delzanno, Michele Tatarek, and Ric-cardo The control sequence at the end of the top line
[] of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
[10] ! Missing delimiter (. inserted).
Underfull \hbox (badness 1810) in paragraph at lines 198--202 <to be read again>
[]\T1/ptm/m/n/10 (+20) M. T<>xen, R. Stew-art, K. Nielsen, R. Je-sup, and \left
[] l.147 ...times \Sigma) \times \ldots \right \left
. \times (\delta^{(P_n)} :...
I was expecting to see something like `(' or `\{' or
`\}' here. If you typed, e.g., `{' instead of `\{', you
should probably delete the `{' by typing `1' now, so that
braces don't get unbalanced. Otherwise just proceed.
Acceptable delimiters are characters whose \delcode is
nonnegative, or you can use `\delimiter <delimiter code>'.
) [11] (./main.aux) ) [11] (./main.aux
! Missing \endcsname inserted.
<to be read again>
\&
l.145 ... Automata Composition}{subsection.7.3}{}}
The control sequence marked <to be read again> should
not appear between \csname and \endcsname.
)
*********** ***********
LaTeX2e <2023-11-01> patch level 1 LaTeX2e <2023-11-01> patch level 1
L3 programming layer <2024-02-20> L3 programming layer <2024-02-20>
*********** ***********
LaTeX Warning: There were undefined references.
LaTeX Warning: There were multiply-defined labels. LaTeX Warning: There were multiply-defined labels.
Package rerunfilecheck Info: File `main.out' has not changed. Package rerunfilecheck Info: File `main.out' has not changed.
(rerunfilecheck) Checksum: BD71A0BDAFAA9B932BE3B9ECF5FF6C8D;1940. (rerunfilecheck) Checksum: 211FF4D7E8372196F5FA1B23FB434BB5;2271.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
43573 strings out of 476076 43583 strings out of 476076
947319 string characters out of 5793776 947496 string characters out of 5793776
2122187 words of memory out of 5000000 2121187 words of memory out of 5000000
64118 multiletter control sequences out of 15000+600000 64119 multiletter control sequences out of 15000+600000
695659 words of font info for 504 fonts, out of 8000000 for 9000 696072 words of font info for 510 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191 14 hyphenation exceptions out of 8191
102i,11n,117p,1636b,1244s stack positions out of 10000i,1000n,20000p,200000b,200000s 102i,11n,117p,1636b,1244s stack positions out of 10000i,1000n,20000p,200000b,200000s
@@ -1568,16 +1609,17 @@ pdfTeX warning (dest): name{Hfootnote.1} has been referenced but does not exist
, replaced by a fixed one , replaced by a fixed one
</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/te </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fonts xmf-dist/fonts/type1/public/amsfonts/cmextra/cmex9.pfb></usr/share/texmf-dist/f
/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/a onts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fonts/type1/pub
msfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb lic/amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm
></usr/share/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texmf-dist/ /cmsy10.pfb></usr/share/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb></usr/sha
fonts/type1/urw/times/utmb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/u re/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texmf-dist/fonts/type
tmr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmri8a.pfb> 1/urw/times/utmb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmr8a.pfb>
Output written on ./main.pdf (11 pages, 246961 bytes). </usr/share/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on ./main.pdf (11 pages, 259218 bytes).
PDF statistics: PDF statistics:
517 PDF objects out of 1000 (max. 8388607) 527 PDF objects out of 1000 (max. 8388607)
480 compressed objects within 5 object streams 488 compressed objects within 5 object streams
242 named destinations out of 1000 (max. 500000) 243 named destinations out of 1000 (max. 500000)
120458 words of extra memory for PDF output out of 128383 (max. 10000000) 120466 words of extra memory for PDF output out of 128383 (max. 10000000)

11
main.out
View File

@@ -8,8 +8,9 @@
\BOOKMARK [2][-]{subsection.4.1}{\376\377\000T\000C\000P}{section.4}% 8 \BOOKMARK [2][-]{subsection.4.1}{\376\377\000T\000C\000P}{section.4}% 8
\BOOKMARK [2][-]{subsection.4.2}{\376\377\000R\000a\000f\000t}{section.4}% 9 \BOOKMARK [2][-]{subsection.4.2}{\376\377\000R\000a\000f\000t}{section.4}% 9
\BOOKMARK [2][-]{subsection.4.3}{\376\377\000S\000C\000T\000P}{section.4}% 10 \BOOKMARK [2][-]{subsection.4.3}{\376\377\000S\000C\000T\000P}{section.4}% 10
\BOOKMARK [1][-]{section.5}{\376\377\000T\000h\000e\000o\000r\000e\000t\000i\000c\000a\000l\000\040\000F\000o\000u\000n\000d\000a\000t\000i\000o\000n\000s\000\040\000o\000f\000\040\000P\000a\000n\000d\000a}{}% 11 \BOOKMARK [1][-]{section.5}{\376\377\000R\000e\000l\000a\000t\000e\000d\000\040\000W\000o\000r\000k}{}% 11
\BOOKMARK [2][-]{subsection.5.1}{\376\377\000M\000a\000t\000h\000e\000m\000a\000t\000i\000c\000a\000l\000\040\000P\000r\000e\000l\000i\000m\000i\000n\000a\000r\000i\000e\000s}{section.5}% 12 \BOOKMARK [1][-]{section.6}{\376\377\000C\000o\000n\000c\000l\000u\000s\000i\000o\000n}{}% 12
\BOOKMARK [2][-]{subsection.5.2}{\376\377\000P\000r\000o\000o\000f\000s\000\040\000o\000f\000\040\000S\000o\000u\000n\000d\000n\000e\000s\000s\000\040\000a\000n\000d\000\040\000C\000o\000m\000p\000l\000e\000t\000e\000n\000e\000s\000s}{section.5}% 13 \BOOKMARK [1][-]{section.7}{\376\377\000A\000p\000p\000e\000n\000d\000i\000x}{}% 13
\BOOKMARK [1][-]{section.6}{\376\377\000R\000e\000l\000a\000t\000e\000d\000\040\000W\000o\000r\000k}{}% 14 \BOOKMARK [2][-]{subsection.7.1}{\376\377\000M\000a\000t\000h\000e\000m\000a\000t\000i\000c\000a\000l\000\040\000P\000r\000e\000l\000i\000m\000i\000n\000a\000r\000i\000e\000s}{section.7}% 14
\BOOKMARK [1][-]{section.7}{\376\377\000C\000o\000n\000c\000l\000u\000s\000i\000o\000n}{}% 15 \BOOKMARK [2][-]{subsection.7.2}{\376\377\000A\000r\000g\000u\000m\000e\000n\000t\000s\000\040\000f\000o\000r\000\040\000P\000a\000n\000d\000a\000'\000s\000\040\000S\000o\000u\000n\000d\000n\000e\000s\000s\000,\000\040\000C\000o\000m\000p\000l\000e\000t\000e\000n\000e\000s\000s\000,\000\040\000a\000n\000d\000\040\000C\000o\000m\000p\000l\000e\000x\000i\000t\000y}{section.7}% 15
\BOOKMARK [2][-]{subsection.7.3}{\376\377\000P\000r\000i\000o\000r\000i\000t\000i\000e\000s\000\040\000\046\000\040\000O\000n\000-\000t\000h\000e\000-\000f\000l\000y\000\040\000B\000\374\000c\000h\000i\000\040\000A\000u\000t\000o\000m\000a\000t\000a\000\040\000C\000o\000m\000p\000o\000s\000i\000t\000i\000o\000n}{section.7}% 16

BIN
main.pdf
View File

Binary file not shown.

11
main.tex
View File

@@ -128,9 +128,9 @@ comment,adjustbox,mdframed,changepage,algorithm,algorithmic}
\label{sec:case_studies} \label{sec:case_studies}
\input{sections/case_studies} \input{sections/case_studies}
\section{Theoretical Foundations of \korg} % \section{Theoretical Foundations of \korg}
\label{sec:proofs} % \label{sec:proofs}
\input{sections/proofs} % \input{sections/proofs}
\section{Related Work}% \section{Related Work}%
\label{sec:Related Work} \label{sec:Related Work}
@@ -140,11 +140,12 @@ comment,adjustbox,mdframed,changepage,algorithm,algorithmic}
\label{sec:conclusion} \label{sec:conclusion}
\input{sections/conclusion} \input{sections/conclusion}
\bibliographystyle{plain} \bibliographystyle{plain}
\bibliography{main} \bibliography{main}
\section{Appendix}
\label{sec:appendix}
\input{sections/appendix-revised}
\end{document} \end{document}

184
sections/appendix-revised.tex Normal file
View File

@@ -0,0 +1,184 @@
\subsection{Mathematical Preliminaries}%
\label{sub:Mathematical Preliminaries}
Linear Temporal Logic (LTL) is a model logic for reasoning about program executions. In LTL, we say a program $P$ \textit{models} a property $\phi$ (notationally, $P \models \phi$). That is, $\phi$ holds over every execution of $P$. If $\phi$ does not hold over every execution of $P$, we say $P \not\models \phi$. The LTL language is given by predicates over a first-order logic with additional temporal operators: \textit{next}, \textit{always}, \textit{eventually}, and \textit{until}.
An LTL model checker is a tool that, given $P$ and $\phi$, can automatically check whether or not $P \models \phi$; in general, LTL is a \textit{decidable} logic, and LTL model checkers will always be able to decide whether $P \models \phi$ given enough time and resources.
We use $\mid \mid$ to denote rendezvous composition. That is, if $S = P \mid \mid Q$, processes $P$ and $Q$ are composed together into a singular state machine by matching their equivalent transitions.
\textit{LTL program synthesis} is the problem of, given an LTL specification $\phi$, automatically deriving a program $P$ that satisfies $\phi$ (that is, $P \models \phi$). \textit{LTL attack synthesis} is logically dual to LTL program synthesis. In attack synthesis, the problem is flipped: given a program $P$ and a property $\phi$ such that $P \models \phi$, we ask whether there exists some "attack" $A$ such that $(P \mid \mid A) \not\models \phi$. Fundamentally, \korg is a synthesizer for such an $A$, based upon the distributed systems attacker framework as described in \cite{Hippel2022}.
\subsection{Arguments for \korg's Soundness, Completeness, and Complexity}%
\label{sub:Proofs of Soundness and Completeness}
As aforementioned, \korg is an extended implementation of the theoretical attack synthesis framework proposed by \cite{Hippel2022}. 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 \cite{Hippel2022} 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 \cite{Hippel2022_anonym}, 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.
\begin{definition}[\ba]
A \ba is a tuple \( B = (Q, \Sigma, \delta, Q_0, F) \) where:
\begin{itemize}
\item \( Q \) is a finite set of states,
\item \( \Sigma \) is a finite alphabet,
\item \( \delta \subseteq Q \times \Sigma \times Q \) is a transition relation,
\item \( Q_0 \subseteq Q \) is a set of initial states,
\item \( F \subseteq Q \) is a set of accepting states.
\end{itemize}
A run of a \ba is an infinite sequence of states \( q_0, q_1, q_2, \ldots \) such that \( q_0 \in Q_0 \) and \( (q_i, a, q_{i+1}) \in \delta \) for some \( a \in \Sigma \) at each step \( i \). The run is considered accepting if it visits states in \( F \) infinitely often.
\end{definition}
\begin{definition}[Process]
A \emph{Process} is a tuple \( P = \langle AP, I, O, S, s_0, T, L \rangle \), where:
\begin{itemize}
\item \( AP \) is a finite set of atomic propositions,
\item \( I \) is a set of inputs,
\item \( O \) is a set of output, such that \( I \cap O = \emptyset \),
\item \( S \) is a finite set of states,
\item \( s_0 \in S \) is the initial state,
\item \( T \subseteq S \times (I \cup O) \times S \) is the transition relation,
\item \( L: S \to 2^{AP} \) is a labeling function mapping each state to a subset of atomic propositions.
\end{itemize}
A transition \( (s, x, s') \in T \) is called an \emph{input transition} if \( x \in I \) and an \emph{output transition} if \( x \in O \).
\end{definition}
\setcounter{theorem}{0}
\begin{theorem}
A process, as defined in \cite{Hippel2022}, always directly corresponds to a \ba.
\end{theorem}
\begin{proof}
Given a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \), we construct a corresponding Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) as follows:
\begin{itemize}
\item Atomic Propositions: \( AP = \{ \text{accept} \} \), a singleton set containing a special proposition indicating acceptance.
\item Inputs and Outputs: \( I = \Sigma \) and \( O = \emptyset \).
\item States: \( S = Q \) and \( s_0 \in Q_0 \).
\item Transition Relation: \( T = \delta \).
\item Labeling Function: \( L: S \to 2^{AP} \) defined by
\end{itemize}
\[
L(s) =
\begin{cases}
\{ \text{accept} \} & \text{if } s \in F, \\
\emptyset & \text{otherwise}.
\end{cases}
\]
In this mapping, the states and transitions of the BA are preserved in the Process, and the accepting states \( F \) are identified via the labeling function \( L \).
Conversely, given a Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) with an acceptance condition defined by a distinguished proposition \( p \in AP \), we define a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \) as follows:
\begin{itemize}
\item States: \( Q = S \) and \( Q_0 = \{ s_0 \} \).
\item Alphabet: \( \Sigma = I \cup O \).
\item Transition Relation: \( \delta = T \).
\item Accepting States: \( F = \{ s \in S \mid p \in L(s) \} \).
\end{itemize}
Here, the accepting states in the BA correspond to those states in the Process that are labeled with the distinguished proposition \( p \).
In both structures, a run is an infinite sequence of states connected by transitions:
\begin{itemize}
\item In the \ba: \( q_0, q_1, q_2, \ldots \) with \( q_0 \in Q_0 \) and \( (q_i, a_i, q_{i+1}) \in \delta \) for some \( a_i \in \Sigma \).
\item In the Process: \( s_0, s_1, s_2, \ldots \) with \( s_0 = s_0 \) and \( (s_i, x_i, s_{i+1}) \in T \) for some \( x_i \in I \cup O \).
\end{itemize}
An accepting run in the \ba visits states in \( F \) infinitely often. Similarly, an accepting run in the Process visits states labeled with \( p \) infinitely often. Since \( F = \{ s \in S \mid p \in L(s) \} \), the acceptance conditions are preserved under the mappings.
\end{proof}
\begin{definition}[Threat Model]
A threat model is a tuple \( (P, (Q_i)_{i=0}^m, \phi) \) where:
\begin{itemize}
\item \( P, Q_0, \ldots, Q_m \) are processes.
\item Each process \( Q_i \) has no atomic propositions (i.e., its set of atomic propositions is empty).
\item \( \varphi \) is an LTL formula such that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \models \phi \).
\item The system \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) satisfies the formula \( \phi \) in a non-trivial manner, meaning that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) has at least one infinite run.
\end{itemize}
\end{definition}
\begin{theorem}
Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022}, is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
\end{theorem}
\begin{proof}
For a given threat model \( (P, (Q_i)_{i=0}^m, \phi) \), checking $\exists ASP$ is equivalent to checking
\[
R = MC(P \mid \mid \text{Daisy}(Q_0) \mid \mid \ldots \mid \mid \text{Daisy}(Q_m), \phi)
\]
Where $MC$ is a model checker, and Daisy($Q_i$) is for intents of this proof, equivalent to a process. Therefore, via the previous theorem we can construct \ba \( BA_{P}, BA_{\text{Daisy}(Q_0)}, \ldots, BA_{\text{Daisy}(Q_m)} \) from the processes \( P, \text{Daisy}(Q_0), \ldots ,\text{Daisy}(Q_m) \). Then, we check
\[
\text{\spin}(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}, \phi)
\]
Or equivalently, translating $\phi$ to the equivalent \ba $BA_{\phi}$ via \cite{Holzmann_1997}, we equivalently check
\[
\left(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}\right) \subseteq BA_{\phi}
\]
Where rendezvous composition for I/O \ba is precise the same as for I/O Kripke Automata; that is, input and output transitions are matched. It's easy to see these composition operations are equivalent.
\end{proof}
\begin{theorem}
Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022}, is in PSPACE.
\end{theorem}
\begin{proof}
By the previous argument the $\exists$ASP problem corresponds to \ba language inclusion, which is well-known to be PSPACE-complete \cite{Kozen_1977}.
\end{proof}
\subsection{Priorities \& On-the-fly B\"uchi Automata Composition}%
\label{sub:Priority \& On-the-fly B\"uchi Automata Composition}
As described in Appendix Section \ref{sub:Proofs of Soundness and Completeness}, \spin reduces verification problems to deciding B\"uchi Automata intersection emptiness. That is, given $n$ B\"uchi Automata programs $P_1,\ldots.,P_n$, \spin decides:
\[
L(P_1) \cap L(P_2) \cap \ldots \cap L(P_n) = \emptyset
\]
Or equivalently:
\[
\exists w \in \Sigma \text{ such that } w \in \bigcap_{i=1}^n L(P_i)
\]
The canonical decision procedure for deciding intersection emptiness involves constructing a composite automata $P_1 \mid \mid P_2 \mid \mid \ldots \mid \mid P_n$ whose acceptance states are the intersection of each process's acceptance states. Then, this composite automata is exhaustively searched. This method is infeasible in practice, as it requires building the entire automata -- which is $\: \vert \: P_1 \: \vert \: \times \ldots \times \: \vert \: P_n \: \vert \:$ in size -- in memory.
Therefore, every practical intersection emptiness implementation employs \textit{on-the-fly composition} to search the composite automata without explicitly constructing it in memory. Recall the \BA is defined as a 5-tuple (as defined in Appendix Section \ref{sub:Proofs of Soundness and Completeness}), $(Q, \Sigma, \delta, Q_0, F)$. The state of the composite automata is denoted as $(q^{(P_1)}, \ldots,q^{(P_n)}$) where $q^{(P_i)} \in Q^{(P_i)}$, for $1 \leq i \leq n$. Similarly, the transition function becomes:
\begin{equation*}
\begin{aligned}
\delta : &\left( (\delta^{(P_1)} : Q^{(P_1)} \times \Sigma) \times \ldots \right \left. \times (\delta^{(P_n)} : Q^{(P_n)} \times \Sigma) \right) \\
& \to (Q^{(P_1)} \times \ldots \times Q^{(P_n)})
\end{aligned}
\end{equation*}
Such that only one such $\delta^{(P_i)}$ can be invoked per transition of $\delta$. Therefore, \textit{priorities} in \spin are implemented by always invoking the highest priority $\delta^{(P_i)}$ among all the possible process transition functions that can be invoked.
% \begin{figure}[h!]
% \centering
% \begin{tikzpicture}
% % Top row (adjusted X positions for even closer horizontal spacing)
% \node (M) at (0,6.25) {\Large $\mathcal{M}$};
% \node (mod) at (2.5,6.25) {\Large $\models$}; % Moved even closer horizontally
% \node (phi) at (5,6.25) {\Large $\varphi$}; % Moved even closer horizontally
% % Labels for the top row
% % \node (t1) at (0, 5.5) {\text{Kripke Structure} \\ \text{of Promela Model}};
% \node (t1) at (0, 5.5) {\parbox{3cm}{\centering Kripke Structure \\ of Promela Model}};
% \node (t2) at (2.5, 5.65) {\textcolor{red}{\text{???}}}; % Moved even closer horizontally
% \node (t3) at (5, 5.5) {\text{LTL Formula}}; % Moved even closer horizontally
% % Downward arrows
% \node (d1) at (0, 4.75) {\Large \textcolor{red}{$\downarrow$}};
% \node (d2) at (5, 4.75) {\Large \textcolor{red}{$\downarrow$}}; % Moved even closer horizontally
% % Middle row with the automaton languages
% \node (q1) at (0,4) {\Large $L(\mathcal{M}_A)$};
% \node (q2) at (2.5,4) {\Large $\cap$}; % Moved even closer horizontally
% \node (q3) at (5,4) {\Large $L(\overline{\varphi_A})$}; % Moved even closer horizontally
% % Bottom row (Büchi Automata labels)
% \node (t4) at (0, 3.25) {\text{B\"uchi Automaton}};
% \node (t5) at (5, 3.25) {\text{B\"uchi Automaton}}; % Moved even closer horizontally
% \end{tikzpicture}
% \caption{The SPIN model checker translates user-defined Promela models into Kripkie structures, which is then translated into a B\"uchi Automata. The LTL formula is turned into a never claim (as to avoid an expensive complementation procedure), then translated into a B\"uchi Automata. Then, intersection non-emptiness is checked. }
% \label{fig:trs}
% \end{figure}

2
sections/design.tex
View File

@@ -282,7 +282,7 @@ When evaluating a \korg attacker model gadget against a \promela model and a liv
property and produce a garbage attack trace. To prevent this, we make the following considerations. property and produce a garbage attack trace. To prevent this, we make the following considerations.
First, we design our \korg gadgets such that they never arbitrarily send and consume messages to a single channel. Second, we allow \korg gadgets, First, we design our \korg gadgets such that they never arbitrarily send and consume messages to a single channel. Second, we allow \korg gadgets,
which are always processing messages on channels, to arbitrarily "skip" messages on a channel if need be. To demonstrate the latter, consider the extension of the drop attacker model gadget in Figure \ref{lst:drop_passer}. We implement message skipping by arbitrarily stopping and waiting after observing a message on a channel; once the channel is observed changing lengths, the message is considered skipped and future messages can be consumed. which are always processing messages on channels, to arbitrarily "skip" messages on a channel if need be. We implement message skipping by arbitrarily stopping and waiting after observing a message on a channel; once the channel is observed changing lengths, the message is considered skipped and future messages can be consumed.
\textbf{Passing Messages On Channels}. \textbf{Passing Messages On Channels}.
In order to arbitrarily pass messages on channels in \spin, required functionality for all three gadgets we present, we exploit the finite channel length assumption. Our \spin gadget is shown below. In order to arbitrarily pass messages on channels in \spin, required functionality for all three gadgets we present, we exploit the finite channel length assumption. Our \spin gadget is shown below.

3
sections/introduction.tex
View File

@@ -31,7 +31,8 @@ We summarize our contributions:
\item We present three case studies for three well-known protocols, TCP, Raft, and SCTP, illustrating the usefulness of \korg. \item We present three case studies for three well-known protocols, TCP, Raft, and SCTP, illustrating the usefulness of \korg.
\end{itemize} \end{itemize}
We release our code and our models as open source at \url{https://anonymous.4open.science/r/attacksynth-artifact-1B5D}. We release our code and our models as open source at \url{https://zenodo.org/records/14968780}.
%\url{https://anonymous.4open.science/r/attacksynth-artifact-1B5D}.
%Formal methods work typically assumes the communication channe %Formal methods work typically assumes the communication channe