more

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}