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-03 23:52:29 -05:00
parent 5469c50d5a
commit 5d4ea50fb3
9 changed files with 2089 additions and 2078 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3982
.latexrun.db
View File

File diff suppressed because it is too large Load Diff

22
main.aux
View File

@@ -61,6 +61,7 @@
\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}
\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}{}}
@@ -71,12 +72,12 @@
\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}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Theoretical Foundations of \textsc {Panda}\xspace }{7}{section.5}\protected@file@percent }
\newlabel{sec:proofs}{{5}{7}{Theoretical Foundations of \korg }{section.5}{}}
\citation{Hippel2022} \citation{Hippel2022}
\citation{Hippel2022} \citation{Hippel2022}
\citation{Hippel2022} \citation{Hippel2022}
\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 } \@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}{}} \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 } \@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Proofs of Soundness and Completeness}{8}{subsection.5.2}\protected@file@percent }
@@ -97,12 +98,12 @@
\bibstyle{plain} \bibstyle{plain}
\bibdata{main} \bibdata{main}
\bibcite{Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021}{1} \bibcite{Arun_Arashloo_Saeed_Alizadeh_Balakrishnan_2021}{1}
\bibcite{ParnoSOK}{2}
\bibcite{Tamarin}{3}
\@writefile{toc}{\contentsline {section}{\numberline {6}Related Work}{9}{section.6}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {6}Related Work}{9}{section.6}\protected@file@percent }
\newlabel{sec:Related Work}{{6}{9}{Related Work}{section.6}{}} \newlabel{sec:Related Work}{{6}{9}{Related Work}{section.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion}{9}{section.7}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {7}Conclusion}{9}{section.7}\protected@file@percent }
\newlabel{sec:conclusion}{{7}{9}{Conclusion}{section.7}{}} \newlabel{sec:conclusion}{{7}{9}{Conclusion}{section.7}{}}
\bibcite{ParnoSOK}{2}
\bibcite{Tamarin}{3}
\bibcite{Basin_Cremers_Meadows_2018}{4} \bibcite{Basin_Cremers_Meadows_2018}{4}
\bibcite{Henda}{5} \bibcite{Henda}{5}
\bibcite{Beurdouche}{6} \bibcite{Beurdouche}{6}
@@ -133,10 +134,11 @@
\bibcite{Rahli_Vukotic_Völp_Esteves-Verissimo_2018}{31} \bibcite{Rahli_Vukotic_Völp_Esteves-Verissimo_2018}{31}
\bibcite{Sergey_Wilcox_Tatlock_2018}{32} \bibcite{Sergey_Wilcox_Tatlock_2018}{32}
\bibcite{Smith_1997}{33} \bibcite{Smith_1997}{33}
\bibcite{mcp}{34} \bibcite{rfc9260}{34}
\bibcite{Hippel2022}{35} \bibcite{mcp}{35}
\bibcite{message_queues_TLA}{36} \bibcite{Hippel2022}{36}
\bibcite{wayne_adversaries}{37} \bibcite{message_queues_TLA}{37}
\bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{38} \bibcite{wayne_adversaries}{38}
\bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{39} \bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{39}
\bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{40}
\gdef \@abspage@last{11} \gdef \@abspage@last{11}

6
main.bbl
View File

@@ -194,6 +194,12 @@ Mark Anthony~Shawn Smith.
\newblock Thesis, Massachusetts Institute of Technology, 1997. \newblock Thesis, Massachusetts Institute of Technology, 1997.
\newblock Accepted: 2008-09-03T18:09:43Z. \newblock Accepted: 2008-09-03T18:09:43Z.
\bibitem{rfc9260}
M.~Tüxen, R.~Stewart, K.~Nielsen, R.~Jesup, and S.~Loreto.
\newblock {Stream Control Transmission Protocol (SCTP) Specification Errata and
Issues}.
\newblock Request for Comments, June 2022.
\bibitem{mcp} \bibitem{mcp}
W.~Visser, K.~Havelund, G.~Brat, and Seungjoon Park. W.~Visser, K.~Havelund, G.~Brat, and Seungjoon Park.
\newblock Model checking programs. \newblock Model checking programs.

58
main.blg
View File

@@ -33,45 +33,45 @@ Warning--empty journal in Hippel2022
Warning--there's a number but no volume 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 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
You've used 39 entries, You've used 40 entries,
2118 wiz_defined-function locations, 2118 wiz_defined-function locations,
749 strings with 11613 characters, 755 strings with 11797 characters,
and the built_in function-call counts, 15161 in all, are: and the built_in function-call counts, 15500 in all, are:
= -- 1482 = -- 1511
> -- 756 > -- 784
< -- 21 < -- 21
+ -- 304 + -- 315
- -- 260 - -- 270
* -- 1006 * -- 1031
:= -- 2339 := -- 2398
add.period$ -- 121 add.period$ -- 124
call.type$ -- 39 call.type$ -- 40
change.case$ -- 241 change.case$ -- 249
chr.to.int$ -- 0 chr.to.int$ -- 0
cite$ -- 69 cite$ -- 70
duplicate$ -- 723 duplicate$ -- 730
empty$ -- 1045 empty$ -- 1067
format.name$ -- 260 format.name$ -- 270
if$ -- 3308 if$ -- 3376
int.to.chr$ -- 0 int.to.chr$ -- 0
int.to.str$ -- 39 int.to.str$ -- 40
missing$ -- 42 missing$ -- 42
newline$ -- 193 newline$ -- 198
num.names$ -- 78 num.names$ -- 80
pop$ -- 331 pop$ -- 343
preamble$ -- 1 preamble$ -- 1
purify$ -- 208 purify$ -- 215
quote$ -- 0 quote$ -- 0
skip$ -- 609 skip$ -- 616
stack$ -- 0 stack$ -- 0
substring$ -- 612 substring$ -- 617
swap$ -- 311 swap$ -- 312
text.length$ -- 21 text.length$ -- 21
text.prefix$ -- 0 text.prefix$ -- 0
top$ -- 0 top$ -- 0
type$ -- 144 type$ -- 148
warning$ -- 30 warning$ -- 30
while$ -- 101 while$ -- 103
width$ -- 41 width$ -- 42
write$ -- 426 write$ -- 436
(There were 30 warnings) (There were 30 warnings)

4
main.fls
View File

@@ -582,10 +582,6 @@ INPUT /usr/share/texmf-dist/fonts/tfm/adobe/zapfchan/pzcmi8r.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/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/ptmri8t.vf
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
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/vf/adobe/times/ptmb8t.vf 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/ptmb8r.tfm
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr8t.vf INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr8t.vf

69
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 01:17 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
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
%&-line parsing enabled. %&-line parsing enabled.
@@ -1361,7 +1361,7 @@ your preamble.
\c@lstlisting=\count405 \c@lstlisting=\count405
LaTeX Font Info: Trying to load font information for OT1+ptmcm on input line LaTeX Font Info: Trying to load font information for OT1+ptmcm on input line
106. 102.
(/usr/share/texmf-dist/tex/latex/psnfss/ot1ptmcm.fd (/usr/share/texmf-dist/tex/latex/psnfss/ot1ptmcm.fd
File: ot1ptmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ptmcm. File: ot1ptmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ptmcm.
) )
@@ -1370,23 +1370,23 @@ Package microtype Info: Loading generic protrusion settings for font family
(microtype) For optimal results, create family-specific settings. (microtype) For optimal results, create family-specific settings.
(microtype) See the microtype manual for details. (microtype) See the microtype manual for details.
LaTeX Font Info: Trying to load font information for OML+ptmcm on input line LaTeX Font Info: Trying to load font information for OML+ptmcm on input line
106. 102.
(/usr/share/texmf-dist/tex/latex/psnfss/omlptmcm.fd (/usr/share/texmf-dist/tex/latex/psnfss/omlptmcm.fd
File: omlptmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ptmcm. File: omlptmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ptmcm.
) )
LaTeX Font Info: Trying to load font information for OMX+psycm on input line LaTeX Font Info: Trying to load font information for OMX+psycm on input line
106. 102.
(/usr/share/texmf-dist/tex/latex/psnfss/omxpsycm.fd (/usr/share/texmf-dist/tex/latex/psnfss/omxpsycm.fd
File: omxpsycm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/psycm. File: omxpsycm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/psycm.
) )
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
(/usr/share/texmf-dist/tex/latex/microtype/mt-msa.cfg (/usr/share/texmf-dist/tex/latex/microtype/mt-msa.cfg
File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS) File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS)
@@ -1395,20 +1395,24 @@ File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS)
File: mt-msb.cfg 2005/06/01 v1.0 microtype config. file: AMS symbols (b) (RS) File: mt-msb.cfg 2005/06/01 v1.0 microtype config. file: AMS symbols (b) (RS)
) )
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 106. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 102.
LaTeX Warning: No \author given.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 107. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 103.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7.4> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7.4> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 107. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 103.
(./sections/abstract.tex) (./sections/introduction.tex (./sections/abstract.tex) (./sections/introduction.tex
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 2 LaTeX Font Info: Trying to load font information for TS1+ptm on input line 2
8. 8.
@@ -1493,21 +1497,23 @@ 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 [7] ) (./sections/proofs.tex
Underfull \vbox (badness 2617) has occurred while \output is active []
[7]
Underfull \hbox (badness 4467) in paragraph at lines 35--36 Underfull \hbox (badness 4467) in paragraph at lines 35--36
[][]\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]
Underfull \hbox (badness 6575) in paragraph at lines 89--90 Underfull \hbox (badness 6575) in paragraph at lines 89--90
[]\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
[] []
[8]
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 106.
@@ -1529,9 +1535,12 @@ Underfull \hbox (badness 2126) in paragraph at lines 79--83
[]\T1/ptm/m/n/10 (+20) Giorgio Delzanno, Michele Tatarek, and Ric-cardo []\T1/ptm/m/n/10 (+20) Giorgio Delzanno, Michele Tatarek, and Ric-cardo
[] []
[10]) [11 [10]
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
[]
] (./main.aux) ) [11] (./main.aux)
*********** ***********
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>
@@ -1547,11 +1556,11 @@ Package rerunfilecheck Info: File `main.out' has not changed.
(rerunfilecheck) Checksum: BD71A0BDAFAA9B932BE3B9ECF5FF6C8D;1940. (rerunfilecheck) Checksum: BD71A0BDAFAA9B932BE3B9ECF5FF6C8D;1940.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
43583 strings out of 476076 43573 strings out of 476076
947409 string characters out of 5793776 947319 string characters out of 5793776
2124187 words of memory out of 5000000 2122187 words of memory out of 5000000
64119 multiletter control sequences out of 15000+600000 64118 multiletter control sequences out of 15000+600000
698237 words of font info for 510 fonts, out of 8000000 for 9000 695659 words of font info for 504 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
@@ -1565,10 +1574,10 @@ msfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb
></usr/share/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texmf-dist/ ></usr/share/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texmf-dist/
fonts/type1/urw/times/utmb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/u fonts/type1/urw/times/utmb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/u
tmr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmri8a.pfb> tmr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on ./main.pdf (11 pages, 246593 bytes). Output written on ./main.pdf (11 pages, 246961 bytes).
PDF statistics: PDF statistics:
515 PDF objects out of 1000 (max. 8388607) 517 PDF objects out of 1000 (max. 8388607)
478 compressed objects within 5 object streams 480 compressed objects within 5 object streams
241 named destinations out of 1000 (max. 500000) 242 named destinations out of 1000 (max. 500000)
124554 words of extra memory for PDF output out of 128383 (max. 10000000) 120458 words of extra memory for PDF output out of 128383 (max. 10000000)

BIN
main.pdf
View File

Binary file not shown.

22
main.tex
View File

@@ -88,20 +88,16 @@ comment,adjustbox,mdframed,changepage,algorithm,algorithmic}
\title{\korg: An Attack Synthesis Tool\\ for Distributed Protocols\footnote{}} \title{\korg: An Attack Synthesis Tool\\ for Distributed Protocols\footnote{}}
%for single author (just remove % characters) %for single author (just remove % characters)
\author{ % \author{
{\rm Jacob Ginesin}\\ % {\rm Jacob Ginesin}\\
Northeastern University % Northeastern University
\and
{\rm Max von Hippel}\\
Benchify, Inc.
\and
{\rm Cristina Nita-Rotaru}\\
Northeastern University
% copy the following lines to add more authors
% \and % \and
% {\rm Name}\\ % {\rm Max von Hippel}\\
%Name Institution % Benchify, Inc.
} % end author % \and
% {\rm Cristina Nita-Rotaru}\\
% Northeastern University
% }
\maketitle \maketitle
\footnote{\korg is an anonymized name for double-blind submission.} \footnote{\korg is an anonymized name for double-blind submission.}

4
sections/case_studies.tex
View File

@@ -111,7 +111,9 @@ In our experiments, we found just one attack on our \texttt{raft-bug.pml} \prome
\subsection{SCTP}% \subsection{SCTP}%
\label{sub:SCTP} \label{sub:SCTP}
SCTP is a transport-layer protocol proposed as an alternative to TCP, featuring a four-way handshake, multi-homing, and multi-streaming. Among other use cases, SCTP is the data transfer protocol for various telecoms signaling protocols as well as WebRTC. For our analysis, we borrow the ten LTL properties and \promela models derived from the SCTP RFCs as described in \cite{Ginesin2024}. We evaluated the SCTP \promela model against \korg's drop, replay, and reordering attacker models on a single uni-directional communication channel. SCTP is designed to resist these attacker models, and we employ \korg to exhaustively demonstrate this is the case. SCTP is a transport-layer protocol proposed as an alternative to TCP, featuring a four-way handshake, multi-homing, and multi-streaming. Among other use cases, SCTP is the data transfer protocol for various telecoms signaling protocols as well as WebRTC. For our analysis, we borrow the ten LTL properties and \promela models derived from the SCTP RFCs as described in \cite{Ginesin2024}. We evaluated the SCTP \promela model against \korg's drop, replay, and reordering attacker models on a single uni-directional communication channel. The drop attacker model was specified to max out at three dropped packets, while the replay and reordering attacker model was specified to max out at two packets. SCTP is designed to resist drop, replay, and reordering attackers \cite{rfc9260}, and we employ \korg to exhaustively demonstrate this is the case.
% these attacker models, and we employ \korg to exhaustively demonstrate this is the case.
%our Raft model satisfies $\phi_1$-$\phi_5$ assuming perfect channels, and \korg allowed us to reason precisely about the effect of imperfect, vulnerable channels. %our Raft model satisfies $\phi_1$-$\phi_5$ assuming perfect channels, and \korg allowed us to reason precisely about the effect of imperfect, vulnerable channels.