synchronous/korg-paper
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

more

Browse Source
This commit is contained in:
JakeGinesin
2024-12-03 17:35:01 -05:00
parent b636781367
commit 673782c888
17 changed files with 2417 additions and 2175 deletions
Download Patch File Download Diff File Expand all files Collapse all files

153
sections/design.tex
View File

@@ -19,18 +19,21 @@ As aforementioned, \korg is based on \textit{LTL attack synthesis}; in particula
%The methodology behind the construction of \korg is based on \textit{LTL attack synthesis}.
\korg is designed to target user-specified communication channels in programs written in formal models. The user inputs a formal model of choice, their desired communication channels to attack, the attacker model of choice, and the correctness property of choice. \korg then invokes the model checker, which exhaustively searches for attacks with respect to the chosen attacker model, formal protocol model, and the correctness property.
\korg is designed to attack user-specified communication channels in state machine-based formal models of distributed protocols. To use \korg, the user inputs a formal model of a distributed protocol in the \promela language, the communication channel(s) the in the formal model they wish to attack, the desired attacker model, and a formalized correctness property for the formal model. The formal model should satisfy the correctness property in absence of \korg.
Once \korg is invoked, it will modify the user-inputted \promela model such that it integrates the desired attacker model. Then, \korg passes the updated \promela model to the model checker, which performs the exhaustive search or provides an explicit counterexample.
%programs written in formal models. The user inputs a formal model of choice, their desired communication channels to attack, the attacker model of choice, and the correctness property of choice. \korg then invokes the model checker, which exhaustively searches for attacks with respect to the chosen attacker model, formal protocol model, and the correctness property.
%\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}.
A high-level visual overview of the \korg pipeline is given in the Figure \ref{fig:korg_workflow}.
\begin{figure*}[h]
\begin{figure}[h]
\centering
\includegraphics[width=0.7\textwidth]{assets/diagram-anon.png}
\includegraphics[width=0.5\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}%
@@ -53,14 +56,154 @@ A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg
The most simple 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 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}
\textbf{Replay Attacker Model Gadget}
The next 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 observed messages the attacker can replay back onto the specified channel.
The replay attacker model gadget \korg employs 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}
\textbf{Reorder Attacker Model Gadget}
\korg supports synthesizing attackers that can \textit{reorder} messages on a channel. Like the drop and replay attacker model gadgets, the user can specify a "reordering limit" that caps the number of messages that can be reordered by the attacker on the specified channel.
The reordering attacker model gadget \korg synthesizes works as follows. The gadget has three states, \textsc{Init}, \textsc{Consume}, and \textsc{Replay}. The gadget begins in the \textsc{Init} state, where it arbitrarily chooses a message to start consuming by transitioning to the \textsc{Consume} state. When in the \textsc{Consume} state, the gadget consumes all messages that appear on the channel, filling up a local buffer, until hitting the defined reordering limit. Once this limit is hit, the gadget transitions into the \textsc{Replay} state. 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_reordering}.
\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}
\textbf{Insert Attacker Models}
\korg supports the synthesis of attackers that can simply insert messages onto a channel. While the drop, replay, and reordering attacker model gadgets as previously described have complex gadgets that \korg synthesizes with respect to a user-specified channel, the insert attacker model gadget is synthesized with respect to a user-defined \textit{IO-file}. This file denotes the specific outputs and channels the attacker is capable of sending, and \korg generates a gadget capable of synthesizing attacks using the given inputs. An example I/O file is given in Figure \ref{lst:io-file}, and the generated gadget is given in Figure \ref{lst:io-file-synth}.