edits

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}