\subsection{Full Korg Soundness and Completeness Proofs}%
\label{sub:korg_proofs}

\begin{definition}[\ba]
A \ba is a tuple \( B = (Q, \Sigma, \delta, Q_0, F) \) where:
\begin{itemize}
    \item \( Q \) is a finite set of states,
    \item \( \Sigma \) is a finite alphabet,
    \item \( \delta \subseteq Q \times \Sigma \times Q \) is a transition relation,
    \item \( Q_0 \subseteq Q \) is a set of initial states,
    \item \( F \subseteq Q \) is a set of accepting states.
\end{itemize}
A run of a \ba is an infinite sequence of states \( q_0, q_1, q_2, \ldots \) such that \( q_0 \in Q_0 \) and \( (q_i, a, q_{i+1}) \in \delta \) for some \( a \in \Sigma \) at each step \( i \). The run is considered accepting if it visits states in \( F \) infinitely often.
\end{definition}

\begin{definition}[Process]
A \emph{Process} is a tuple \( P = \langle AP, I, O, S, s_0, T, L \rangle \), where:
\begin{itemize}
    \item \( AP \) is a finite set of atomic propositions,
    \item \( I \) is a set of inputs,
    \item \( O \) is a set of output, such that \( I \cap O = \emptyset \),
    \item \( S \) is a finite set of states,
    \item \( s_0 \in S \) is the initial state,
    \item \( T \subseteq S \times (I \cup O) \times S \) is the transition relation,
    \item \( L: S \to 2^{AP} \) is a labeling function mapping each state to a subset of atomic propositions.
\end{itemize}
A transition \( (s, x, s') \in T \) is called an \emph{input transition} if \( x \in I \) and an \emph{output transition} if \( x \in O \).
\end{definition}

\setcounter{theorem}{0} 
\begin{theorem}
  A process, as defined in Hippel et al., always directly corresponds to a \ba.
\end{theorem}

\begin{proof}

Given a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \), we construct a corresponding Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) as follows:

\begin{itemize}
    \item {Atomic Propositions: \( AP = \{ \text{accept} \} \), a singleton set containing a special proposition indicating acceptance.
    \item Inputs and Outputs: \( I = \Sigma \) and \( O = \emptyset \).
    \item States: \( S = Q \) and \( s_0 \in Q_0 \).
    \item Transition Relation: \( T = \delta \).
    \item Labeling Function: \( L: S \to 2^{AP} \) defined by
    \[        L(s) = \begin{cases}            \{ \text{accept} \} & \text{if } s \in F, \\            \emptyset & \text{otherwise}.        \end{cases}    \]
\end{itemize}

In this mapping, the states and transitions of the BA are preserved in the Process, and the accepting states \( F \) are identified via the labeling function \( L \).

Conversely, given a Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) with an acceptance condition defined by a distinguished proposition \( p \in AP \), we define a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \) as follows:

\begin{itemize}
    \item States: \( Q = S \) and \( Q_0 = \{ s_0 \} \).
    \item Alphabet: \( \Sigma = I \cup O \).
    \item Transition Relation: \( \delta = T \).
    \item Accepting States: \( F = \{ s \in S \mid p \in L(s) \} \).
\end{itemize}

Here, the accepting states in the BA correspond to those states in the Process that are labeled with the distinguished proposition \( p \).

In both structures, a run is an infinite sequence of states connected by transitions:

\begin{itemize}
    \item In the \ba: \( q_0, q_1, q_2, \ldots \) with \( q_0 \in Q_0 \) and \( (q_i, a_i, q_{i+1}) \in \delta \) for some \( a_i \in \Sigma \).
    \item In the Process: \( s_0, s_1, s_2, \ldots \) with \( s_0 = s_0 \) and \( (s_i, x_i, s_{i+1}) \in T \) for some \( x_i \in I \cup O \).
\end{itemize}

An accepting run in the \ba visits states in \( F \) infinitely often. Similarly, an accepting run in the Process visits states labeled with \( p \) infinitely often. Since \( F = \{ s \in S \mid p \in L(s) \} \), the acceptance conditions are preserved under the mappings.
  
\end{proof}

\begin{definition}[Threat Model]
A threat model is a tuple \( (P, (Q_i)_{i=0}^m, \phi) \) where:
\begin{itemize}
    \item \( P, Q_0, \ldots, Q_m \) are processes.
    \item Each process \( Q_i \) has no atomic propositions (i.e., its set of atomic propositions is empty).
    \item \( \varphi \) is an LTL formula such that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \models \phi \).
    \item The system \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) satisfies the formula \( \phi \) in a non-trivial manner, meaning that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) has at least one infinite run.
\end{itemize}
\end{definition}

\begin{theorem}
  Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
\end{theorem}

\begin{proof}
  For a given threat model \( (P, (Q_i)_{i=0}^m, \phi) \), checking $\exists ASP$ is equivalent to checking
  \[
  R = MC(P \mid \mid \text{Daisy}(Q_0) \mid \mid \ldots \mid \mid \text{Daisy}(Q_m), \phi)
  \] 
  Where $MC$ is a model checker, and Daisy($Q_i$) is for intents of this proof, equivalent to a process. Therefore, via the previous theorem we can construct \ba \( BA_{P}, BA_{\text{Daisy}(Q_0)}, \ldots, BA_{\text{Daisy}(Q_m)} \) from the processes \( P, \text{Daisy}(Q_0), \ldots ,\text{Daisy}(Q_m) \). Then, we check
  \[
    \text{\spin}(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}, \phi)
  \] 
  Or equivalently, translating $\phi$ to the equivalent \ba $BA_{\phi}$ via \cite{Holzmann_1997}, we equivalently check
  \[
    \left(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}\right) \subseteq BA_{\phi}
  \] 
\end{proof}

\begin{theorem}
Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., is PSPACE-complete.
\end{theorem}

\begin{proof}
By the previous argument the $\exists$ASP problem corresponds to \ba language inclusion, which is well-known to be PSPACE-complete \cite{Kozen_1977}.
\end{proof}

\subsection{Preventing Korg Livelocks}%
\label{sub: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'll 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{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}




