diff --git a/main.aux b/main.aux index f855618..f9c148f 100644 --- a/main.aux +++ b/main.aux @@ -3,61 +3,58 @@ \citation{Basin_Cremers_Dreier_Sasse_2022,Blanchet_Smyth_Cheval_Sylvestre,Kobeissi_Nicolas_Tiwari,Blanchet_Jacomme,Basin_Linker_Sasse} \citation{Hippel2022_anonym} \@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}\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}}Mathematical Preliminaries}{1}{}\protected@file@percent } -\newlabel{sub:Mathematical Preliminaries}{{\mbox {II-A}}{1}{}{}{}} +\newlabel{sub:Mathematical Preliminaries}{{\mbox {II-A}}{1}} \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-B}}High-level design}{1}{}\protected@file@percent } -\newlabel{sub:High-level design}{{\mbox {II-B}}{1}{}{}{}} -\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A high-level overview of the \textsc {PANDA}\xspace workflow}}{2}{}\protected@file@percent } -\newlabel{fig:korg_workflow}{{1}{2}{}{}{}} +\newlabel{sub:High-level design}{{\mbox {II-B}}{1}} \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-C}}Supported Attacker Models}{2}{}\protected@file@percent } -\newlabel{sub:Supported Attacker Models}{{\mbox {II-C}}{2}{}{}{}} -\newlabel{lst:korg_drop}{{1}{2}{}{}{}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}{2}{}\protected@file@percent } +\newlabel{sub:Supported Attacker Models}{{\mbox {II-C}}{2}} \@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-D}}\textsc {PANDA}\xspace Implementation}{2}{}\protected@file@percent } -\newlabel{sub:impl}{{\mbox {II-D}}{2}{}{}{}} -\newlabel{lst:korg_replay}{{2}{3}{}{}{}} -\@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:spin-model}{{6}{3}{}{}{}} -\@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.}{3}{}\protected@file@percent } -\newlabel{lst:korg_reordering}{{3}{3}{}{}{}} -\@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{sub:impl}{{\mbox {II-D}}{2}} +\newlabel{lst:spin-model}{{6}{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 } +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A high-level overview of the \textsc {PANDA}\xspace workflow}}{3}{}\protected@file@percent } +\newlabel{fig:korg_workflow}{{1}{3}} +\newlabel{lst:korg_drop}{{1}{3}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-E}}Usage}{3}{}\protected@file@percent } +\newlabel{sub:Usage}{{\mbox {II-E}}{3}} +\newlabel{lst:abp}{{8}{3}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {8}Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}{3}{}\protected@file@percent } +\newlabel{lst:korg_replay}{{2}{4}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{4}{}\protected@file@percent } +\newlabel{lst:korg-shell}{{\mbox {II-E}}{4}} +\newlabel{lst:korg_reordering}{{3}{4}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}{4}{}\protected@file@percent } \citation{Cluzel_Georgiou_Moy_Zeller_2021,Smith_1997,Pacheco2022} \citation{Pacheco2022} \citation{Pacheco2022} -\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 } -\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-E}}Usage}{4}{}\protected@file@percent } -\newlabel{sub:Usage}{{\mbox {II-E}}{4}{}{}{}} -\newlabel{lst:abp}{{7}{4}{}{}{}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {7}Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}{4}{}\protected@file@percent } -\newlabel{lst:korg-shell}{{\mbox {II-E}}{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}{}{}{}} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016,Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Ongaro} \citation{Ongaro} \citation{Ongaro} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016} +\newlabel{lst:io-file}{{4}{5}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Example I/O file targetting channel "cn"}{5}{}\protected@file@percent } +\newlabel{lst:io-file-synth}{{5}{5}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Example gadget synthesized from an I/O file targetting the channel "cn"}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {III}Case Studies}{5}{}\protected@file@percent } +\newlabel{sec:case_studies}{{III}{5}} +\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-A}}TCP}{5}{}\protected@file@percent } +\newlabel{sub:TCP}{{\mbox {III-A}}{5}} +\newlabel{lst:drop_passer}{{7}{5}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {7}Example dropping attacker model gadget with message skipping}{5}{}\protected@file@percent } +\newlabel{res:tcp-table}{{\mbox {III-A}}{5}} +\@writefile{lof}{\contentsline {figure}{\numberline {2}{\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.}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-B}}Raft}{5}{}\protected@file@percent } +\newlabel{sub:Raft}{{\mbox {III-B}}{5}} \citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016} \bibstyle{IEEEtran} \bibdata{main} \bibcite{Lamport_1994}{1} \bibcite{Holzmann_1997}{2} -\newlabel{res:tcp-table}{{\mbox {III-A}}{5}{}{}{}} -\@writefile{lof}{\contentsline {figure}{\numberline {2}{\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.}}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-B}}Raft}{5}{}\protected@file@percent } -\newlabel{sub:Raft}{{\mbox {III-B}}{5}{}{}{}} -\newlabel{res:raft-table}{{\mbox {III-B}}{5}{}{}{}} -\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Breakdown of the attacker scenarios assessed with \textsc {PANDA}\xspace against our Raft \textsc {Promela}\xspace model. In all experiments, Raft 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.}}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {IV}Conclusion}{5}{}\protected@file@percent } -\newlabel{sec:conclusion}{{IV}{5}{}{}{}} -\@writefile{toc}{\contentsline {section}{References}{5}{}\protected@file@percent } \bibcite{Clarke_Wang}{3} \bibcite{Basin_Cremers_Dreier_Sasse_2022}{4} \bibcite{Blanchet_Smyth_Cheval_Sylvestre}{5} @@ -71,4 +68,9 @@ \bibcite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}{13} \bibcite{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}{14} \bibcite{Ongaro}{15} +\newlabel{res:raft-table}{{\mbox {III-B}}{6}} +\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Breakdown of the attacker scenarios assessed with \textsc {PANDA}\xspace against our Raft \textsc {Promela}\xspace model. In all experiments, Raft 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.}}{6}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {IV}Conclusion}{6}{}\protected@file@percent } +\newlabel{sec:conclusion}{{IV}{6}} +\@writefile{toc}{\contentsline {section}{References}{6}{}\protected@file@percent } \gdef \@abspage@last{6} diff --git a/main.log b/main.log index 19dcc40..ada342d 100644 --- a/main.log +++ b/main.log @@ -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) 29 NOV 2024 13:00 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex 2023.12.22) 29 NOV 2024 14:41 entering extended mode restricted \write18 enabled. + file:line:error style messages enabled. %&-line parsing enabled. **main.tex (./main.tex -LaTeX2e <2023-11-01> patch level 1 -L3 programming layer <2024-02-20> -(./IEEEtran.cls +LaTeX2e <2022-11-01> patch level 1 +L3 programming layer <2023-02-22> (./IEEEtran.cls Document Class: IEEEtran 2015/08/26 V1.8b by Michael Shell -- See the "IEEEtran_HOWTO" manual for usage information. -- http://www.michaelshell.org/tex/ieeetran/ \@IEEEtrantmpdimenA=\dimen140 \@IEEEtrantmpdimenB=\dimen141 \@IEEEtrantmpdimenC=\dimen142 -\@IEEEtrantmpcountA=\count188 -\@IEEEtrantmpcountB=\count189 -\@IEEEtrantmpcountC=\count190 -\@IEEEtrantmptoksA=\toks17 +\@IEEEtrantmpcountA=\count185 +\@IEEEtrantmpcountB=\count186 +\@IEEEtrantmpcountC=\count187 +\@IEEEtrantmptoksA=\toks16 LaTeX Font Info: Trying to load font information for OT1+ptm on input line 5 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. ) -- 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 \IEEEiedmathlabelsep=\dimen157 \IEEEiedtopsep=\skip48 -\c@section=\count191 -\c@subsection=\count192 -\c@subsubsection=\count193 -\c@paragraph=\count194 -\c@IEEEsubequation=\count195 +\c@section=\count188 +\c@subsection=\count189 +\c@subsubsection=\count190 +\c@paragraph=\count191 +\c@IEEEsubequation=\count192 \abovecaptionskip=\skip49 \belowcaptionskip=\skip50 -\c@figure=\count196 -\c@table=\count197 -\@IEEEeqnnumcols=\count198 -\@IEEEeqncolcnt=\count199 -\@IEEEsubeqnnumrollback=\count266 +\c@figure=\count193 +\c@table=\count194 +\@IEEEeqnnumcols=\count195 +\@IEEEeqncolcnt=\count196 +\@IEEEsubeqnnumrollback=\count197 \@IEEEquantizeheightA=\dimen158 \@IEEEquantizeheightB=\dimen159 \@IEEEquantizeheightC=\dimen160 \@IEEEquantizeprevdepth=\dimen161 -\@IEEEquantizemultiple=\count267 +\@IEEEquantizemultiple=\count198 \@IEEEquantizeboxA=\box51 \@IEEEtmpitemindent=\dimen162 \IEEEPARstartletwidth=\dimen163 -\c@IEEEbiography=\count268 +\c@IEEEbiography=\count199 \@IEEEtranrubishbin=\box52 ) ** 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 \nocite on input line 332. Package: cite 2015/02/27 v 5.5 ) -(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty -Package: amsmath 2023/05/13 v2.17o AMS math features +(/usr/local/texlive/2023/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2022/04/08 v2.17n AMS math features \@mathmargin=\skip51 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 -(/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 -\@emptytoks=\toks18 +\@emptytoks=\toks17 \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 \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 ) -\inf@bad=\count269 +\inf@bad=\count266 LaTeX Info: Redefining \frac on input line 234. -\uproot@=\count270 -\leftroot@=\count271 +\uproot@=\count267 +\leftroot@=\count268 LaTeX Info: Redefining \overline on input line 399. LaTeX Info: Redefining \colon on input line 410. -\classnum@=\count272 -\DOTSCASE@=\count273 +\classnum@=\count269 +\DOTSCASE@=\count270 LaTeX Info: Redefining \ldots on input line 496. LaTeX Info: Redefining \dots on input line 499. LaTeX Info: Redefining \cdots on input line 620. @@ -160,38 +160,38 @@ LaTeX Info: Redefining \Bigg on input line 725. \big@size=\dimen166 LaTeX Font Info: Redeclaring font encoding OML on input line 743. 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 \pmod on input line 910. LaTeX Info: Redefining \smash on input line 940. LaTeX Info: Redefining \relbar on input line 970. LaTeX Info: Redefining \Relbar on input line 971. -\c@MaxMatrixCols=\count275 +\c@MaxMatrixCols=\count272 \dotsspace@=\muskip16 -\c@parentequation=\count276 -\dspbrk@lvl=\count277 -\tag@help=\toks19 -\row@=\count278 -\column@=\count279 -\maxfields@=\count280 -\andhelp@=\toks20 +\c@parentequation=\count273 +\dspbrk@lvl=\count274 +\tag@help=\toks18 +\row@=\count275 +\column@=\count276 +\maxfields@=\count277 +\andhelp@=\toks19 \eqnshift@=\dimen167 \alignsep@=\dimen168 \tagshift@=\dimen169 \tagwidth@=\dimen170 \totwidth@=\dimen171 \lineht@=\dimen172 -\@envbody=\toks21 +\@envbody=\toks20 \multlinegap=\skip52 \multlinetaggap=\skip53 -\mathdisplay@stack=\toks22 +\mathdisplay@stack=\toks21 LaTeX Info: Redefining \[ on input line 2953. 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 -(/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 \symAMSa=\mathgroup4 \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' (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' -(/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) ) -(/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) -\KV@toks@=\toks23 +\KV@toks@=\toks22 ) -\c@ALC@unique=\count281 -\c@ALC@line=\count282 -\c@ALC@rem=\count283 -\c@ALC@depth=\count284 +\c@ALC@unique=\count278 +\c@ALC@line=\count279 +\c@ALC@rem=\count280 +\c@ALC@depth=\count281 \ALC@tlm=\skip54 \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) -(/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) -(/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) ) -(/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 ) 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 )) \Gin@req@height=\dimen173 \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 ) -(/usr/share/texmf-dist/tex/latex/xcolor/xcolor.sty -Package: xcolor 2023/11/15 v3.01 LaTeX color extensions (UK) +(/usr/local/texlive/2023/texmf-dist/tex/latex/xcolor/xcolor.sty +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 ) -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) -Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1350. -Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1354. -Package xcolor Info: Model `RGB' extended on input line 1366. -Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1368. -Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1369. -Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1370. -Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1371. -Package xcolor Info: Model `Gray' substituted by `gray' on input line 1372. -Package xcolor Info: Model `wave' substituted by `hsb' on input line 1373. +(/usr/local/texlive/2023/texmf-dist/tex/latex/graphics/mathcolor.ltx) +Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1353. +Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1357. +Package xcolor Info: Model `RGB' extended on input line 1369. +Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1371. +Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1372. +Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1373. +Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1374. +Package xcolor Info: Model `Gray' substituted by `gray' on input line 1375. +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 -\thm@style=\toks24 -\thm@bodyfont=\toks25 -\thm@headfont=\toks26 -\thm@notefont=\toks27 -\thm@headpunct=\toks28 +\thm@style=\toks23 +\thm@bodyfont=\toks24 +\thm@headfont=\toks25 +\thm@notefont=\toks26 +\thm@headpunct=\toks27 \thm@preskip=\skip56 \thm@postskip=\skip57 \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) ) -(/usr/share/texmf-dist/tex/latex/tools/array.sty -Package: array 2023/10/16 v2.5g Tabular extension package (FMi) +(/usr/local/texlive/2023/texmf-dist/tex/latex/tools/array.sty +Package: array 2022/09/04 v2.5g Tabular extension package (FMi) \col@sep=\dimen175 \ar@mcellbox=\box55 \extrarowheight=\dimen176 -\NC@list=\toks30 +\NC@list=\toks29 \extratabsurround=\skip59 \backup@length=\skip60 \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 Excluding comment 'comment') -\c@definition=\count285 +\c@definition=\count282 -(/usr/share/texmf-dist/tex/latex/listings/listings.sty -\lst@mode=\count286 +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count283 \lst@gtempboxa=\box57 -\lst@token=\toks31 -\lst@length=\count287 +\lst@token=\toks30 +\lst@length=\count284 \lst@currlwidth=\dimen177 -\lst@column=\count288 -\lst@pos=\count289 +\lst@column=\count285 +\lst@pos=\count286 \lst@lostspace=\dimen178 \lst@width=\dimen179 -\lst@newlines=\count290 -\lst@lineno=\count291 +\lst@newlines=\count287 +\lst@lineno=\count288 \lst@maxwidth=\dimen180 -(/usr/share/texmf-dist/tex/latex/listings/lstpatch.sty -File: lstpatch.sty 2024/02/21 1.10 (Carsten Heinz) -) -(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz) -\c@lstnumber=\count292 -\lst@skipnumbers=\count293 +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz) +\c@lstnumber=\count289 +\lst@skipnumbers=\count290 \lst@framebox=\box58 ) -(/usr/share/texmf-dist/tex/latex/listings/listings.cfg -File: listings.cfg 2024/02/21 1.10 listings configuration +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/listings.cfg +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 -File: lstlang1.sty 2024/02/21 1.10 listings language file +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang1.sty +File: lstlang1.sty 2023/02/27 1.9 listings language file ) -(/usr/share/texmf-dist/tex/latex/listings/lstlang2.sty -File: lstlang2.sty 2024/02/21 1.10 listings language file +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang2.sty +File: lstlang2.sty 2023/02/27 1.9 listings language file ) -(/usr/share/texmf-dist/tex/latex/listings/lstlang3.sty -File: lstlang3.sty 2024/02/21 1.10 listings language file +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstlang3.sty +File: lstlang3.sty 2023/02/27 1.9 listings language file ) -(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2024/02/21 1.10 (Carsten Heinz) +(/usr/local/texlive/2023/texmf-dist/tex/latex/listings/lstmisc.sty +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 -File: l3backend-pdftex.def 2024-02-20 L3 backend support: PDF output (pdfTeX) -\l__color_backend_stack_int=\count295 +(/usr/local/texlive/2023/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def +File: l3backend-pdftex.def 2023-01-16 L3 backend support: PDF output (pdfTeX) +\l__color_backend_stack_int=\count292 \l__pdf_internal_box=\box59 -) (./main.aux) +) +(./main.aux) \openout1 = `main.aux'. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 53. @@ -354,29 +352,29 @@ LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 53. LaTeX Font Info: ... okay on input line 53. -- 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).] -\scratchcounter=\count296 +\scratchcounter=\count293 \scratchdimen=\dimen181 \scratchbox=\box60 -\nofMPsegments=\count297 -\nofMParguments=\count298 -\everyMPshowfont=\toks32 -\MPscratchCnt=\count299 +\nofMPsegments=\count294 +\nofMParguments=\count295 +\everyMPshowfont=\toks31 +\MPscratchCnt=\count296 \MPscratchDim=\dimen182 -\MPnumerator=\count300 -\makeMPintoPDFobject=\count301 -\everyMPtoPDFconversion=\toks33 -) (/usr/share/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +\MPnumerator=\count297 +\makeMPintoPDFobject=\count298 +\everyMPtoPDFconversion=\toks32 +) (/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 Info: Redefining graphics rule for `.eps' on input line 4 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 e )) -\c@lstlisting=\count302 +\c@lstlisting=\count299 LaTeX Warning: No \author given. @@ -390,16 +388,17 @@ 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/share/texmf-dist/tex/latex/amsfonts/umsa.fd +(/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/share/texmf-dist/tex/latex/amsfonts/umsb.fd +(/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 -[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fon -ts/enc/dvips/base/8r.enc} +)) +(./sections/design.tex [1{/usr/local/texlive/2023/texmf-var/fonts/map/pdftex/up +dmap/pdftex.map}{/usr/local/texlive/2023/texmf-dist/fonts/enc/dvips/base/8r.enc +} ] @@ -407,16 +406,16 @@ ts/enc/dvips/base/8r.enc} File: assets/diagram-anon.png Graphic file (type png) Package pdftex.def Info: assets/diagram-anon.png used on input line 27. -(pdftex.def) Requested size: 258.0pt x 98.08133pt. +(pdftex.def) Requested size: 361.19843pt x 137.31522pt. -Overfull \hbox (6.0pt too wide) in paragraph at lines 27--28 - [][] - [] + +LaTeX Warning: `h' float specifier changed to `ht'. (./sections/examples.tex LaTeX Font Info: Trying to load font information for OT1+pcr on input line 5 . - (/usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd + +(/usr/local/texlive/2023/texmf-dist/tex/latex/psnfss/ot1pcr.fd File: ot1pcr.fd 2001/06/04 font definitions for OT1/pcr. ) @@ -426,21 +425,28 @@ 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 Font Warning: Font shape `OT1/ptm/m/scit' undefined -(Font) using `OT1/ptm/m/sc' instead on input line 98. +(Font) using `OT1/ptm/m/sc' instead on input line 101. -[2 <./assets/diagram-anon.png (PNG copy)>] [3] -LaTeX Font Info: Trying to load font information for TS1+pcr on input line 1 -62. +[2] -(/usr/share/texmf-dist/tex/latex/psnfss/ts1pcr.fd +LaTeX Warning: `h' float specifier changed to `ht'. + +[3 <./assets/diagram-anon.png (PNG copy)>] +LaTeX Font Info: Trying to load font information for TS1+pcr on input line 2 +09. + +(/usr/local/texlive/2023/texmf-dist/tex/latex/psnfss/ts1pcr.fd File: ts1pcr.fd 2001/06/04 font definitions for TS1/pcr. -) -Excluding 'comment' comment.) (./sections/case_studies.tex [4] +) [4] +Excluding 'comment' comment.) (./sections/case_studies.tex Underfull \hbox (badness 4144) in paragraph at lines 19--19 []\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by [] @@ -460,7 +466,10 @@ Underfull \hbox (badness 4144) in paragraph at lines 19--19 []\OT1/pcr/m/n/5 SYN_RECEIVED \OT1/ptm/m/n/5 is even-tu-ally fol-lowed by [] -Excluding 'comment' comment.) (./sections/conclusion.tex) (./main.bbl + +LaTeX Warning: `!h' float specifier changed to `!ht'. + +Excluding 'comment' comment. [5]) (./sections/conclusion.tex) (./main.bbl ** WARNING: IEEEtran.bst: No hyphenation pattern has been ** loaded for the language `en'. Using the pattern for ** the default language instead. @@ -473,7 +482,6 @@ Excluding 'comment' comment.) (./sections/conclusion.tex) (./main.bbl ** WARNING: IEEEtran.bst: No hyphenation pattern has been ** loaded for the language `en'. Using the pattern for ** the default language instead. -[5] ** WARNING: IEEEtran.bst: No hyphenation pattern has been ** loaded for the language `en'. Using the pattern for ** the default language instead. @@ -539,34 +547,33 @@ Before submitting the final camera ready copy, remember to: uses only Type 1 fonts and that every step in the generation process uses the appropriate paper size. -[6 +[6] (./main.aux) + +LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. -] (./main.aux) - *********** -LaTeX2e <2023-11-01> patch level 1 -L3 programming layer <2024-02-20> - *********** ) Here is how much of TeX's memory you used: - 6591 strings out of 476076 - 97840 string characters out of 5793776 - 2220187 words of memory out of 5000000 - 28590 multiletter control sequences out of 15000+600000 - 603547 words of font info for 123 fonts, out of 8000000 for 9000 - 14 hyphenation exceptions out of 8191 - 57i,11n,65p,1306b,1570s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on ./main.pdf (6 pages, 216304 bytes). + 6627 strings out of 476025 + 99507 string characters out of 5790016 + 2183388 words of memory out of 5000000 + 26968 multiletter control sequences out of 15000+600000 + 559531 words of font info for 121 fonts, out of 8000000 for 9000 + 1141 hyphenation exceptions out of 8191 + 57i,11n,62p,1306b,1621s stack positions out of 10000i,1000n,20000p,200000b,200000s +< +/usr/local/texlive/2023/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb> +Output written on main.pdf (6 pages, 218651 bytes). PDF statistics: 90 PDF objects out of 1000 (max. 8388607) 54 compressed objects within 1 object stream diff --git a/main.pdf b/main.pdf index ff99d4f..752a980 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.synctex.gz b/main.synctex.gz index 95ac856..0aa1a3d 100644 Binary files a/main.synctex.gz and b/main.synctex.gz differ diff --git a/sections/case_studies.tex b/sections/case_studies.tex index 613ac38..4606bbc 100644 --- a/sections/case_studies.tex +++ b/sections/case_studies.tex @@ -1,6 +1,6 @@ %!TEX root = ../main.tex -In this section we describe two case studies: the Transmission Control Protocol, a data transfer protocol, and Raft, a state machine replication protocol. +In this section we describe two case studies: the Transmission Control Protocol (TCP), a data transfer protocol, and Raft, a state machine replication protocol. \subsection{TCP}% \label{sub:TCP} diff --git a/sections/design.tex b/sections/design.tex index c45e2c7..fd04ad0 100644 --- a/sections/design.tex +++ b/sections/design.tex @@ -22,12 +22,13 @@ As aforementioned, \korg is based on \textit{LTL attack synthesis}; in particula \korg is designed to target user-specified communication channels in programs written in \promela, the modeling language of the \spin model checker. The user inputs a \promela model, their desired communication channels to attack, the attacker model of choice, and the LTL correctness property 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}. -\begin{figure}[h] +\begin{figure*}[h] \centering - \includegraphics[width=0.5\textwidth]{assets/diagram-anon.png} + \includegraphics[width=0.7\textwidth]{assets/diagram-anon.png} \caption{A high-level overview of the \korg workflow} \label{fig:korg_workflow} -\end{figure} +\end{figure*} + \subsection{Supported Attacker Models}% \label{sub:Supported Attacker Models} @@ -64,6 +65,8 @@ These attacker models can be mixed and matched as desired by the \korg user. For \input{sections/examples} + + % \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. @@ -118,6 +121,50 @@ active proctype Peer2() { %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. +\textbf{Preventing \korg Livelocks} +In general, there are two types of LTL properties: safety, and liveness. Informally, safety properties state "a bad thing never happens," and liveness properties state "a good thing always happens." +Therefore, safety properties can be violated by finite traces, while liveness properties require infinite traces to be violated. +When evaluating a \korg attacker model gadget against a \promela model and a liveness property, it is crucial to ensure the gadget has no cyclic behavior. If a \korg gadget has cyclic behavior in any way, it will trivially violate the liveness +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, +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. + +\begin{figure}[h] +\begin{lstlisting}[caption={Example dropping attacker model gadget with message skipping}, label={lst:drop_passer}] +chan cn = [8] of { int, int, int }; + +active proctype attacker_drop() { +int b_0, b_1, b_2, blocker; +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 + } + // pass over a message on a channel as needed + :: cn ? [b_0, b_1, b_2] -> atomic { + // wait for the channel to change lengths + // then, once it does, go to MAIN + blocker = len(cn); + do + :: blocker != len(cn) -> goto MAIN; + od + } + :: goto BREAK; + od +BREAK: +} +\end{lstlisting} +\end{figure} + + \subsection{Usage}% \label{sub:Usage}