moar

sections/attacker_models.tex

@@ -5,8 +5,10 @@
 
 The first and most simple general attacker model \korg supports is an attacker that can \textit{drop} messages from a 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. An example is shown in Figure \ref{lst:korg_drop}.
+
 \begin{figure}[h]
-\begin{lstlisting}[caption={Example dropping attacker model gadget}, label={lst:spin-model}]
+\begin{lstlisting}[caption={Example dropping attacker model gadget with drop limit of 3, targetting channel "cn"}, label={lst:korg_drop}]
 chan cn = [8] of { int, int, int }; 
 
 active proctype attacker_drop() {
@@ -31,9 +33,56 @@ BREAK:
 
 \subsection{Replaying Attacker Model}%
 \label{sub:Replay Attacker}
-The second attacker model \korg supports is an attacker that can observe and replay 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 messages the attacker can replay back onto the specified channel. 
+The second attacker model \korg supports is an attacker that can observe and \textit{replay} 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 messages the attacker can replay back onto the specified channel. 
 
-\jg{todo: describe impl more}
+The dropper attacker model gadget \korg synthesizes 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{lst:korg_replay}.
+
+\begin{figure}[h]
+\begin{lstlisting}[caption={Example replay attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_replay}]
+chan cn = [8] of { int, int, int }; 
+
+// local memory for the gadget
+chan gadget_mem = [3] of { int, int, int };
+
+active proctype attacker_replay() {
+int b_0, b_1, b_2;
+int i = 3;
+CONSUME:
+  do
+  // read messages until the limit is passed
+  :: cn ? [b_0, b_1, b_2] -> atomic {
+   cn ? <b_0, b_1, b_2> -> gadget_mem ! b_0, b_1, b_2;
+    i--;
+    if
+    :: i == 0 -> goto REPLAY;
+    :: i != 0 -> goto CONSUME;
+    fi
+    }
+  od
+REPLAY:
+  do
+  :: atomic {
+    // nondeterministically select a random value from the storage buffer
+    int am;
+    select(am : 0 .. len(gadget_mem)-1);
+    do
+    :: am != 0 ->
+      am = am-1;
+      gadget_mem ? b_0, b_1, b_2 -> gadget_mem ! b_0, b_1, b_2;
+    :: am == 0 ->
+      gadget_mem ? b_0, b_1, b_2 -> cn ! b_0, b_1, b_2;
+      break;
+    od
+    }
+  // doesn't need to use all messages on the channel
+  :: atomic {gadget_mem ? b_0, b_1, b_2; }
+  // once mem has no more messages, we're done
+  :: empty(gadget_mem) -> goto BREAK;
+  od
+BREAK:
+}
+\end{lstlisting}
+\end{figure}
 
 \subsection{Rearranging Attacker Model}%
 \label{sub:Rearrange Attacker}