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

smore

Browse Source
This commit is contained in:
Your Name
2025-03-03 02:19:07 -05:00
parent fd02cf5c83
commit 5469c50d5a
6 changed files with 1954 additions and 1961 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
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}{}}
\@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}{}}
\@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{Pacheco2022}
\citation{Pacheco2022}
\citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016,Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Ongaro}
\citation{Ongaro}
\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}{}}
\@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}{}}
@@ -58,14 +58,14 @@
\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 }
\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{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
\citation{Ginesin2024}
\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 }
\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}{}}
\@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}{}}
@@ -73,12 +73,12 @@
\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}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Mathematical Preliminaries}{7}{subsection.5.1}\protected@file@percent }
\newlabel{sub:Mathematical Preliminaries}{{5.1}{7}{Mathematical Preliminaries}{subsection.5.1}{}}
\citation{Hippel2022}
\citation{Hippel2022}
\citation{Hippel2022}
\citation{Hippel2022}
\@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}