attack synthesis
This commit is contained in:
JakeGinesin
1275
.latexrun.db
1275
.latexrun.db
File diff suppressed because it is too large
Load Diff
54
main.aux
54
main.aux
@@ -6,44 +6,42 @@
|
||||
\newlabel{sec:introduction}{{I}{1}{}{}{}}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {II}\textsc {PANDA}\xspace Architecture}{1}{}\protected@file@percent }
|
||||
\newlabel{sec:design}{{II}{1}{}{}{}}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-A}}High-level design}{1}{}\protected@file@percent }
|
||||
\newlabel{sub:High-level design}{{\mbox {II-A}}{1}{}{}{}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces A high-level overview of the \textsc {PANDA}\xspace workflow}}{1}{}\protected@file@percent }
|
||||
\newlabel{fig:korg_workflow}{{1}{1}{}{}{}}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-B}}Supported Attacker Models}{1}{}\protected@file@percent }
|
||||
\newlabel{sub:Supported Attacker Models}{{\mbox {II-B}}{1}{}{}{}}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-A}}Mathematical Preliminaries}{1}{}\protected@file@percent }
|
||||
\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}{}{}{}}
|
||||
\@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 }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {II-C}}\textsc {PANDA}\xspace Implementation}{2}{}\protected@file@percent }
|
||||
\newlabel{sub:impl}{{\mbox {II-C}}{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{toc}{\contentsline {subsection}{\numberline {\mbox {II-D}}Usage}{2}{}\protected@file@percent }
|
||||
\newlabel{sub:Usage}{{\mbox {II-D}}{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{lst:abp}{{7}{3}{}{}{}}
|
||||
\@writefile{lol}{\contentsline {lstlisting}{\numberline {7}Example (simplified) \textsc {Promela}\xspace model of the alternating bit protocol.}{3}{}\protected@file@percent }
|
||||
\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}
|
||||
\newlabel{lst:io-file}{{4}{4}{}{}{}}
|
||||
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Example I/O file targetting channel "cn"}{4}{}\protected@file@percent }
|
||||
\newlabel{lst:io-file-synth}{{5}{4}{}{}{}}
|
||||
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Example gadget synthesized from an I/O file targetting the channel "cn"}{4}{}\protected@file@percent }
|
||||
\newlabel{lst:korg-shell}{{\mbox {II-D}}{4}{}{}{}}
|
||||
\@writefile{toc}{\contentsline {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}{}{}{}}
|
||||
\newlabel{res:tcp-table}{{\mbox {III-A}}{4}{}{}{}}
|
||||
\@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.}}{4}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {\mbox {III-B}}Raft}{4}{}\protected@file@percent }
|
||||
\newlabel{sub:Raft}{{\mbox {III-B}}{4}{}{}{}}
|
||||
\citation{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}
|
||||
\citation{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
|
||||
@@ -51,6 +49,15 @@
|
||||
\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}
|
||||
@@ -64,9 +71,4 @@
|
||||
\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}}{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 }
|
||||
\gdef \@abspage@last{6}
|
||||
|
||||
41
main.fls
41
main.fls
@@ -184,12 +184,7 @@ INPUT ./sections/design.tex
|
||||
INPUT ./sections/design.tex
|
||||
INPUT ./sections/design.tex
|
||||
INPUT ./sections/design.tex
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
OUTPUT ./main.pdf
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmrc7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
@@ -215,23 +210,26 @@ INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./assets/diagram-anon.png
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT ./sections/examples.tex
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/tex/latex/psnfss/ts1pcr.fd
|
||||
@@ -243,9 +241,11 @@ INPUT ./sections/case_studies.tex
|
||||
INPUT ./sections/case_studies.tex
|
||||
INPUT ./sections/case_studies.tex
|
||||
INPUT ./sections/case_studies.tex
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr7t.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr8r.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr8c.vf
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
|
||||
INPUT ./sections/conclusion.tex
|
||||
INPUT ./sections/conclusion.tex
|
||||
INPUT ./sections/conclusion.tex
|
||||
@@ -264,6 +264,7 @@ INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/urw/courier/ucrr8a.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/urw/times/utmb8a.pfb
|
||||
INPUT /usr/share/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb
|
||||
|
||||
71
main.log
71
main.log
@@ -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) 29 NOV 2024 05:26
|
||||
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
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
%&-line parsing enabled.
|
||||
@@ -398,21 +398,21 @@ LaTeX Font Info: Trying to load font information for U+msb on input line 6.
|
||||
(/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd
|
||||
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
|
||||
)) (./sections/design.tex
|
||||
<assets/diagram-anon.png, id=1, 584.1825pt x 222.07968pt>
|
||||
File: assets/diagram-anon.png Graphic file (type png)
|
||||
<use assets/diagram-anon.png>
|
||||
Package pdftex.def Info: assets/diagram-anon.png used on input line 14.
|
||||
(pdftex.def) Requested size: 258.0pt x 98.08133pt.
|
||||
|
||||
Overfull \hbox (6.0pt too wide) in paragraph at lines 14--15
|
||||
[][]
|
||||
[]
|
||||
|
||||
[1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texmf-dist/fon
|
||||
ts/enc/dvips/base/8r.enc}
|
||||
|
||||
|
||||
<./assets/diagram-anon.png (PNG copy)>]
|
||||
]
|
||||
<assets/diagram-anon.png, id=13, 584.1825pt x 222.07968pt>
|
||||
File: assets/diagram-anon.png Graphic file (type png)
|
||||
<use assets/diagram-anon.png>
|
||||
Package pdftex.def Info: assets/diagram-anon.png used on input line 27.
|
||||
(pdftex.def) Requested size: 258.0pt x 98.08133pt.
|
||||
|
||||
Overfull \hbox (6.0pt too wide) in paragraph at lines 27--28
|
||||
[][]
|
||||
[]
|
||||
|
||||
(./sections/examples.tex
|
||||
LaTeX Font Info: Trying to load font information for OT1+pcr on input line 5
|
||||
.
|
||||
@@ -426,30 +426,21 @@ 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 85.
|
||||
(Font) using `OT1/ptm/m/sc' instead on input line 98.
|
||||
|
||||
|
||||
Underfull \vbox (badness 10000) has occurred while \output is active []
|
||||
|
||||
[2]
|
||||
Underfull \vbox (badness 1067) has occurred while \output is active []
|
||||
|
||||
[3]
|
||||
[2 <./assets/diagram-anon.png (PNG copy)>] [3]
|
||||
LaTeX Font Info: Trying to load font information for TS1+pcr on input line 1
|
||||
49.
|
||||
62.
|
||||
|
||||
(/usr/share/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
|
||||
Excluding 'comment' comment.) (./sections/case_studies.tex [4]
|
||||
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
|
||||
[]
|
||||
@@ -469,7 +460,7 @@ 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. [4]) (./sections/conclusion.tex) (./main.bbl
|
||||
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.
|
||||
@@ -482,6 +473,7 @@ Excluding 'comment' comment. [4]) (./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.
|
||||
@@ -535,7 +527,7 @@ Underfull \hbox (badness 1509) in paragraph at lines 76--81
|
||||
** WARNING: IEEEtran.bst: No hyphenation pattern has been
|
||||
** loaded for the language `en'. Using the pattern for
|
||||
** the default language instead.
|
||||
[5])
|
||||
)
|
||||
|
||||
** Conference Paper **
|
||||
Before submitting the final camera ready copy, remember to:
|
||||
@@ -556,27 +548,28 @@ L3 programming layer <2024-02-20>
|
||||
***********
|
||||
)
|
||||
Here is how much of TeX's memory you used:
|
||||
6590 strings out of 476076
|
||||
97808 string characters out of 5793776
|
||||
2208187 words of memory out of 5000000
|
||||
28589 multiletter control sequences out of 15000+600000
|
||||
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,1644s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
57i,11n,65p,1306b,1570s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
</usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/
|
||||
texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/share/texmf-dist/font
|
||||
s/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texmf-dist/fonts/type1/public/
|
||||
amsfonts/cm/cmr10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr
|
||||
5.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/shar
|
||||
e/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texmf-dist/fon
|
||||
ts/type1/urw/courier/ucrr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/ut
|
||||
mb8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/t
|
||||
exmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texmf-dist/fonts/type1/u
|
||||
rw/times/utmri8a.pfb>
|
||||
Output written on ./main.pdf (6 pages, 204728 bytes).
|
||||
ts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texmf-dist/fonts/type1/urw/c
|
||||
ourier/ucrr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr
|
||||
/share/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/texmf-dist/font
|
||||
s/type1/urw/times/utmr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmri
|
||||
8a.pfb>
|
||||
Output written on ./main.pdf (6 pages, 216304 bytes).
|
||||
PDF statistics:
|
||||
85 PDF objects out of 1000 (max. 8388607)
|
||||
51 compressed objects within 1 object stream
|
||||
90 PDF objects out of 1000 (max. 8388607)
|
||||
54 compressed objects within 1 object stream
|
||||
0 named destinations out of 1000 (max. 500000)
|
||||
6 words of extra memory for PDF output out of 10000 (max. 10000000)
|
||||
|
||||
|
||||
BIN
main.synctex.gz
BIN
main.synctex.gz
Binary file not shown.
@@ -110,6 +110,6 @@ Dropping AppendEntryResponse messages & no \\
|
||||
\end{figure}
|
||||
In our experiments, we found just one attack on our Raft \promela model, violating election safety in particular. In this scenario, peer A and peer B are candidates for election. Peer A receives three votes, one from itself and two from other peers, and Peer B receives two votes, one from itself and one from another peer. The replay attacker simply replays the vote sent to peer B. Then, both Peer A and Peer B are convinced they won the election and change their state to leader. Following this, leader completeness is also naturally violated.
|
||||
|
||||
To be clear, this is not an attack on the general Raft protocol, but rather an attack on our specific Raft implementation: in this case, the bug \korg exploits involves our Raft model not ensuring votes received are from unique peers\footnote{Naturally, this requires cryptography and therefore is challenging to express in the semantics of \promela.}. In general, the complete Raft protocol has been proven to resist drop and replay attackers \cite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}. In this scenario, \korg demonstrates its ability to discover subtle bugs in protocol logic ; 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.
|
||||
To be clear, this is not an attack on the general Raft protocol, but rather an attack on our specific Raft implementation: in this case, the bug \korg exploits involves our Raft model not ensuring votes received are from unique peers\footnote{Naturally, this requires cryptography and therefore is challenging to express in the semantics of \promela.}. In general, the complete Raft protocol has been proven to resist drop and replay attackers \cite{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}. In this scenario, \korg demonstrates its ability to discover subtle bugs in protocol logic; 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.
|
||||
|
||||
% We note our analysis is in no
|
||||
|
||||
@@ -1,12 +1,25 @@
|
||||
%!TEX root = ../main.tex
|
||||
In this section we discuss the details behind the design, formal guarantees, implementation, and usage of \korg.
|
||||
|
||||
\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 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$.
|
||||
|
||||
|
||||
\subsection{High-level design}%
|
||||
\label{sub:High-level design}
|
||||
|
||||
\cnr{need introductory paragraph about program synthesis, the main idea}
|
||||
As aforementioned, \korg is based on \textit{LTL attack synthesis}; in particular, \korg synthesizes attacks with respect to \textit{imperfect} channels. That is, \korg is designed to synthesize attacks that involve replaying, dropping, reordering, or inserting messages on a communication channel.
|
||||
|
||||
At the highest level, \korg sits on user-specified communication channels in a program written in \promela, the modeling language of the \spin model checker. The user selects an attacker model of choice and correctness properties of choice. \korg then invokes \spin, which exhaustively searches for attacks with respect to the chosen attacker model, \promela model, and correctness property.
|
||||
%The methodology behind the construction of \korg is based on \textit{LTL attack synthesis}.
|
||||
|
||||
\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]
|
||||
|
||||
Reference in New Issue
Block a user