From 2d4eb9b50758cb0ac8dc76911132b3dfb1064f71 Mon Sep 17 00:00:00 2001 From: Your Name Date: Mon, 24 Feb 2025 10:55:54 -0500 Subject: [PATCH] more --- figures/drop.tex | 28 ++++++++++++++++++++++++++++ figures/reorder.tex | 38 ++++++++++++++++++++++++++++++++++++++ figures/replay.tex | 40 ++++++++++++++++++++++++++++++++++++++++ sections/gadgets.tex | 37 +++++++++++++++++++++++++++++++++++++ 4 files changed, 143 insertions(+) create mode 100644 figures/drop.tex create mode 100644 figures/reorder.tex create mode 100644 figures/replay.tex create mode 100644 sections/gadgets.tex diff --git a/figures/drop.tex b/figures/drop.tex new file mode 100644 index 0000000..27316ce --- /dev/null +++ b/figures/drop.tex @@ -0,0 +1,28 @@ +%!TEX root = ../main.tex + +\begin{figure}[h] + \centering + \begin{tikzpicture}[scale=0.15] + \tikzstyle{every node}+=[inner sep=0pt] + \draw [black] (10.7,-13) circle (4.7); + \draw (10.7,-13) node {consume}; + \draw [black] (35.6,-13) circle (4.7); + \draw (35.6,-13) node {end}; + \draw [black] (8.628,-8.802) arc (234:-54:3.525); + \draw (10.7,-1.93) node [above, align=center] {\textit{consume} \texttt{msg} from \texttt{chan} \\ \texttt{lim-=1}}; + \fill [black] (12.77,-8.8) -- (13.65,-8.45) -- (12.84,-7.86); + \draw [black] (15.4,-13) -- (30.9,-13); + \fill [black] (30.9,-13) -- (30.1,-12.5) -- (30.1,-13.5); + \draw (23.15,-12.5) node [above] {\texttt{lim=0}}; + \draw [black] (12.772,-17.198) arc (54:-234:3.525); + \draw (10.7,-24.08) node [below] {\textit{pass} \texttt{msg} on \texttt{chan}}; + \fill [black] (8.63,-17.2) -- (7.75,-17.55) -- (8.56,-18.14); + \draw [black] (0.2,-13) -- (6,-13); + \fill [black] (6,-13) -- (5.2,-12.5) -- (5.2,-13.5); + \end{tikzpicture} + + \caption{high-level state machine diagram of the \textit{drop} attacker gadget, attacking a channel \texttt{chan}. A natural number \texttt{lim} is pre-defined.} + \label{fig:drop} +\end{figure} + + diff --git a/figures/reorder.tex b/figures/reorder.tex new file mode 100644 index 0000000..4ad75df --- /dev/null +++ b/figures/reorder.tex @@ -0,0 +1,38 @@ +\begin{figure}[H] + \centering + +\begin{tikzpicture}[scale=0.145] +\tikzstyle{every node}+=[inner sep=0pt] +\draw [black] (9.6,-11.8) circle (4.4); +\draw (9.6,-11.8) node {wait}; +\draw [black] (28.9,-27.9) circle (4.4); +\draw (28.9,-27.9) node {replay}; +\draw [black] (9.6,-27.9) circle (4.4); +\draw (9.6,-27.9) node {end}; +\draw [black] (28.9,-11.8) circle (4.4); +\draw (28.9,-11.8) node {\small{consume}}; +\draw [black] (7.66,-7.87) arc (234:-54:3.3); +\draw (9.6,-1.4) node [above] {\textit{pass} \texttt{msg} on \texttt{chan}}; +\fill [black] (11.54,-7.87) -- (12.41,-7.52) -- (11.61,-6.93); +\draw [black] (0.2,-11.8) -- (5.2,-11.8); +\fill [black] (5.2,-11.8) -- (4.4,-11.3) -- (4.4,-12.3); +\draw [black] (24.5,-27.9) -- (14,-27.9); +\fill [black] (14,-27.9) -- (14.8,-28.4) -- (14.8,-27.4); +\draw (19.25,-28.4) node [below] {\small{\texttt{buf} empty}}; +\draw [black] (32.83,-25.96) arc (144:-144:3.3); +\draw (39.3,-27.9) node [right, align=center] {\textit{consume} \texttt{msg} from \texttt{buf} \\ \textit{send} \texttt{msg} to \texttt{chan}}; +\fill [black] (32.83,-29.84) -- (33.18,-30.71) -- (33.77,-29.91); +\draw [black] (28.9,-16.2) -- (28.9,-23.5); +\fill [black] (28.9,-23.5) -- (29.4,-22.7) -- (28.4,-22.7); +\draw (29.4,-19.85) node [right] {\texttt{lim=0}}; +\draw [black] (14,-11.8) -- (24.5,-11.8); +\fill [black] (24.5,-11.8) -- (23.7,-11.3) -- (23.7,-12.3); +\draw [black] (32.83,-9.86) arc (144:-144:3.3); +\draw (39.3,-11.8) node [right, align=center] {\textit{consume} \texttt{msg} from \texttt{chan} \\ \textit{add} \texttt{msg} to \texttt{buf} \\ \texttt{lim-=1}}; +\fill [black] (32.83,-13.74) -- (33.18,-14.61) -- (33.77,-13.81); +\end{tikzpicture} + +\caption{High-level state machine diagram of the \textit{reorder} attacker gadget, attacking a channel \texttt{chan}. A natural number \texttt{lim} is pre-defined. \texttt{buf} is a simple FIFO buffer of length \texttt{lim}.} + \label{fig:reorder} + +\end{figure} diff --git a/figures/replay.tex b/figures/replay.tex new file mode 100644 index 0000000..8677396 --- /dev/null +++ b/figures/replay.tex @@ -0,0 +1,40 @@ +\begin{figure}[h] + \centering + + \begin{tikzpicture}[scale=0.155] + \tikzstyle{every node}+=[inner sep=0pt] + \draw [black] (8.6,-13) circle (4.7); + \draw (8.6,-13) node {observe}; + \draw [black] (26.9,-13) circle (4.7); + \draw (26.9,-13) node {replay}; + \draw [black] (46.1,-13) circle (4.7); + \draw (46.1,-13) node {end}; + \draw [black] (6.528,-8.802) arc (234:-54:3.525); + \draw (8.6,-1.93) node [above, align=center] {\textit{copy} \texttt{msg} from \texttt{chan} to \texttt{buf} \\ \texttt{lim-=1}}; + \fill [black] (10.67,-8.8) -- (11.55,-8.45) -- (10.74,-7.86); + \draw [black] (10.672,-17.198) arc (54:-234:3.525); + \draw (8.6,-24.08) node [below] {\textit{pass} \texttt{msg} on \texttt{chan}}; + \fill [black] (6.53,-17.2) -- (5.65,-17.55) -- (6.46,-18.14); + \draw [black] (0.2,-13) -- (3.9,-13); + \fill [black] (3.9,-13) -- (3.1,-12.5) -- (3.1,-13.5); + \draw [black] (31.6,-13) -- (41.4,-13); + \fill [black] (41.4,-13) -- (40.6,-12.5) -- (40.6,-13.5); + \draw (36.5,-12.5) node [above] {\texttt{buf} empty}; + \draw [black] (13.3,-13) -- (22.2,-13); + \fill [black] (22.2,-13) -- (21.4,-12.5) -- (21.4,-13.5); + \draw (17.75,-12.5) node [above] {\texttt{lim=0}}; + \draw [black] (28.972,-17.198) arc (54:-234:3.525); + \draw (26.9,-24.08) node [below] {pass \texttt{msg} on \texttt{chan}}; + \fill [black] (24.83,-17.2) -- (23.95,-17.55) -- (24.76,-18.14); + \draw [black] (24.828,-8.802) arc (234:-54:3.525); + \draw (26.9,-1.93) node [above] {\textit{send} \texttt{msg} from \texttt{buf} to \texttt{chan}}; + \fill [black] (28.97,-8.8) -- (29.85,-8.45) -- (29.04,-7.86); + \draw [black] (24.828,-8.802) arc (234:-54:3.525); + \fill [black] (28.97,-8.8) -- (29.85,-8.45) -- (29.04,-7.86); + \end{tikzpicture} + + \caption{High-level state machine diagram of the \textit{replay} attacker gadget, attacking a channel \texttt{chan}. A natural number \texttt{lim} is pre-defined. \texttt{buf} is a simple FIFO buffer of length \texttt{lim}.} + + \label{fig:replay} + +\end{figure} diff --git a/sections/gadgets.tex b/sections/gadgets.tex new file mode 100644 index 0000000..cb95fab --- /dev/null +++ b/sections/gadgets.tex @@ -0,0 +1,37 @@ +In this section, we introduce our methodology for the automatic synthesis of drop, replay, and reorder attacks on distributed protocols. + +We design our gadgets in \textit{generality}; that is, they can be applied to arbitrary communication channels, agnostic to what is actually transmitted. In this section we describe the design for our \textit{drop}, \textit{replay}, and \textit{reorder} gadgets. Fundamentally, these gadgets are designed to be analyzed in respect to composition with the other processes, as described in the gadgetry-based mathematical attack synthesis framework in \cite{Hippel2022}. Therefore, these gadgets are best realized within program models such as Kripke Structures or I/O automata. Note, these gadgets have been mechanized within \spin, as further described in \ref{sec:design}. + +%Note, these gadgets have been mechanized within \spin, as further described in section \ref{sec:design}. + +% \subsection{Foundations of Gadgetry}% +% \label{sub:Supported Attackers} +% Fundamentally, our approach is based off +% - based off gadgetry via hippel et al. + +% \subsection{Gadget Design}% +% \label{sub:Gadget Design Approach} + +% We designed our gadgets in \textit{generality}; that is, they can be applied to arbitrary communication channels, agnostic to what is actually transmitted. In this section we describe the design for our \textit{drop}, \textit{replay}, and \textit{reorder} gadgets. Note, these gadgets have been mechanized within \spin, as further described in section \ref{sec:design}. + +%In this section we describe our gadgets in generality. We emphasize that these attacker gadgets have been mechanized within \spin, as further described in section (). + +%these gadgets have been mechanized within \spin. + +%We design three gadgets, designed to be composed with the rest of the protocol. + +\textbf{Drop Attacker Gadget Design}. The most simple attacker gadget we define is the \textit{drop} gadget, which drops a select number of messages from the victim channel. The user specifies a "drop limit" value that limits the number of packets the attacker can drop from the channel. Note, a higher drop limit will increase the search space of possible attacks, thereby increasing execution time. +The dropper attacker model gadget \korg synthesizes works as follows. The gadget will nondeterministically choose to observe a message on a channel. Then, if the drop limit variable is not zero, it will consume the message. The state diagram of the drop gadget is shown in Figure \ref{fig:drop}. + +\input{figures/drop} + +\textbf{Replay Attacker Gadget Design}. +The next attacker gadget we define is the \textit{replay} gadget, which copies and replays messages back onto a channel. Similarly to the drop limit for the dropping attacker model, the user can specify a "replay limit" that caps the number of observed messages the attacker can replay back onto the specified Channel. +The replay attacker gadget works as follows. The gadget has two states, \textsc{Consume} and \textsc{Replay}. The gadget starts in the \textsc{Consume} state and nondeterministically reads (but not consumes) messages on the target channel, sending them into a local storage buffer. Once the gadget read the number of messages on the channel equivalent to the defined replay limit, its state changes to \textsc{Replay}. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{fig:replay}. + +\input{figures/replay} + +\textbf{Reorder Attacker Gadget Design}. +The final attacker gadget we define is the \textit{reorder} gadget, which supports reordering messages on a channel. Like the drop and replay attacker model gadgets, the user can specify a "reordering limit" that caps the number of messages that can be reordered by the attacker on the specified channel. The gadget has three states: \textsc{Init}, \textsc{Consume}, and \textsc{Replay}. The gadget begins in the \textsc{Init} state, where it arbitrarily chooses a message to start consuming by transitioning to the \textsc{Consume} state. When in the \textsc{Consume} state, the gadget consumes all messages that appear on the channel, filling up a local buffer, until hitting the defined reordering limit. Once this limit is hit, the gadget transitions into the \textsc{Replay} state. In the \textsc{Replay} state, the gadget nondeterministically selects messages from its storage buffer to replay onto the channel until out of messages. An example is shown in Figure \ref{fig:reorder}. + +\input{figures/reorder}