308 lines
11 KiB
TeX
308 lines
11 KiB
TeX
\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}
|
|
|
|
|
|
|
|
|