%\section{Attacker Model Gadget Examples}%
%\label{sub:Attacker Model Gadget Examples}

\begin{figure}[h]
\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() {
int b_0, b_1, b_2;
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
    }
  od
BREAK:
}
\end{lstlisting}
\end{figure}

\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}

\begin{figure}[h]
\begin{lstlisting}[caption={Example reordering attacker model gadget with the selected replay limit as 3, targetting channel "cn"}, label={lst:korg_reordering}]
chan cn = [8] of { int, int, int }; 

chan gadget_mem = [3] of { int, int, int };
active proctype attacker_reordering() priority 255 {
byte b_0, b_1, b_2, blocker;
int i = 3;
INIT:
do
  // arbitrarily choose a message to start consuming on
  :: {
      blocker = len(cn);
      do
      :: b != len(c) -> goto INIT;
      od
    }
  :: goto CONSUME;
od
CONSUME:
do
  // consume messages with high priority
  :: c ? [b_0] -> atomic {
    c ? b_0 -> gadget_mem ! b_0;
    i--;
    if 
    :: i == 0 -> goto REPLAY;
    :: i != 0 -> goto CONSUME;
    fi
  }
od
REPLAY:
  do
  // replay messages back onto the channel, also with priority
  :: atomic {
    int am;
    select(am : 0 .. len(gadget_mem)-1);
    do
    :: am != 0 ->
      am = am-1;
      gadget_mem ? b_0 -> attacker_mem_0 ! b_0;
    :: am == 0 ->
      gadget_mem ? b_0 -> c ! b_0;
      break;
    od
    }
  :: atomic { empty(gadget_mem) -> goto BREAK; }
  od
BREAK:
}

\end{lstlisting}
\end{figure}

\begin{figure}[h]
\begin{lstlisting}[caption={Example I/O file targetting channel "cn"}, label={lst:io-file}]
cn:
	I:
	O:1-1-1, 1-2-3, 3-4-5
\end{lstlisting}

\begin{lstlisting}[caption={Example gadget synthesized from an I/O file targetting the channel "cn"}, label={lst:io-file-synth}]
chan cn = [8] of { int, int, int };

active proctype daisy() {
INIT:
  do
  :: cn ! 1,1,1;
  :: cn ! 1,2,3;
  :: cn ! 3,4,5;
  :: goto RECOVERY;
  od
RECOVERY:
}
\end{lstlisting}
\end{figure}