%!TEX root = ../main.tex In this section we discuss the details behind the design, formal guarantees, implementation, and usage of \korg. \subsection{Mathematical Preliminaries}% \label{sub:Mathematical Preliminaries} Linear Temporal Logic (LTL) is a model logic for reasoning about program executions. In LTL, we say a program $P$ \textit{models} a property $\phi$ (notationally, $P \models \phi$). That is, $\phi$ holds over every execution of $P$. If $\phi$ does not hold over every execution of $P$, we say $P \not\models \phi$. The LTL language is given by predicates over a first-order logic with additional temporal operators: \textit{next}, \textit{always}, \textit{eventually}, and \textit{until}. An LTL model checker is a tool that, given $P$ and $\phi$, can automatically check whether or not $P \models \phi$; in general, LTL is a \textit{decidable} logic, and LTL model checkers will always be able to decide whether $P \models \phi$ given enough time and resources. We use $\mid \mid$ to denote rendezvous composition. That is, if $S = P \mid \mid Q$, processes $P$ and $Q$ are composed together into a singular state machine by matching their equivalent transitions. \textit{LTL program synthesis} is the problem of, given an LTL specification $\phi$, automatically deriving a program $P$ that satisfies $\phi$ (that is, $P \models \phi$). \textit{LTL attack synthesis} is logically dual to LTL program synthesis. In attack synthesis, the problem is flipped: given a program $P$ and a property $\phi$ such that $P \models \phi$, we ask whether there exists some "attack" $A$ such that $(P \mid \mid A) \not\models \phi$. Fundamentally, \korg is a synthesizer for such an $A$. \subsection{High-level design}% \label{sub:High-level design} As aforementioned, \korg is based on \textit{LTL attack synthesis}; in particular, \korg synthesizes attacks with respect to \textit{imperfect} channels. That is, \korg is designed to synthesize attacks that involve replaying, dropping, reordering, or inserting messages on one or more communication channels. %The methodology behind the construction of \korg is based on \textit{LTL attack synthesis}. \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) in the protocol model they wish to attack, the desired attacker model, and a formalized correctness property for the protocol model. The protocol 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 for an attack, returning a trace if such an attack is found. %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 visual overview of the \korg pipeline is given in Figure \ref{fig:korg_workflow}. \begin{figure}[h] \centering \includegraphics[width=0.5\textwidth]{assets/diagram3.png} \caption{A high-level overview of the \korg workflow} \label{fig:korg_workflow} \end{figure} \subsection{Supported Attacker Models}% \label{sub:Supported Attacker Models} %\korg supports the automatic synthesis of attacks with respect to four general pre-defined attacker models applicable to any communication channel: %\begin{itemize} %\item \textbf{Drop Attacker Model}. Drop attackers are capable of dropping a finite number of messages off a channel. %\item \textbf{Replay Attacker Model}. Replay attackers are capable of replaying previously seen messages back onto a channel. %\item \textbf{Reorder Attacker Model}. Reorder attackers are capable of reordering messages on a channel. %\item \textbf{Insert Attacker Model}. Insert attackers are capable of inserting arbitrary messages (as specifiable by the user) onto a channel. %\end{itemize} \korg supports four general attacker models: an attacker that can drop, replay, reorder, or insert messages on a channel. In this section we discuss the various details that went into the implementation of the gadgets that encapsulate the behavior of the respective attacker models. % Additionally, \korg supports user-defined attacker that insert arbitrary messages onto a channel. In this section we discuss the various details that go into each attacker model. \textbf{Drop Attacker Model Gadget} 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 ? -> 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}. These attacker models can be mixed and matched as desired by the \korg user. For example, a user can specify a drop attacker and replay attacker to target channel 1, a reordering attacker to target channel 2, and an insert attacker to target channel 3. If multiple attacker models are declared, \korg will synthesize attacks where the attackers on different channel \textit{coordinate} to construct a unifying attack. \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. %\korg is an implementation of the theoretical attack synthesis framework proposed by Hippel et al. This framework enjoys soundness and completeness guarantees for attacks discovered; that is, if there exists an attack, it is discovered, and if an attack is discovered, it is valid. However, the attack synthesis framework proposed by Hippel et al. reasons about an abstracted, theoretical process construct. Therefore, in order to correctly claim \korg is also sound and complete, it is necessary to demonstrate discovering an attack within the theoretical framework reduces to the semantics of \spin, the model checker \korg is built on top of. %There exists a semantic gap between the theoretical attack synthesis framework proposed by Hippel et al., and the semantics of \korg. Therefore, in order to correctly claim \korg maintains the soundness and completeness of the theoretical framework it implements, it suffices to demonstrate finding an attack within the theoretical attack synthesis framework precisely reduces to the semantics of \spin. %the model checker \korg is implemented on top of. %\begin{proof} %Recalling the definitions from Hippel et al., a \textit{process} is Kripke structure whose transitions are equipped additional input and output operations in the same flavor as a standard I/O automata.\footnote{Modeling processes in this way allows for the simultaneous modeling of message passing while also maintaining the ability to leverage Linear Temporal Logic for specification} %Hippel et al. also defines asynchronous composition on processes to match input and output transitions with the same label when constructing the product automata. %Threat models, then, contain a \textit{target process} $P$ that is unmodifiable by an attacker, a set of vulnerable processes $Q_1,\ldots,Q_n$ that are unmodifiable by an attacker, and a Linear Temporal Logic specification $\phi$. Let $\comp$ denote asynchronous composition between processes. For simplicity, let $Q = Q_1 \comp Q_2 \comp \ldots \comp Q_n$. %Given this, we initially require $P \comp Q \models \phi$ (that is, $P$ composed with $Q$ satisfies the property $\phi$.) %Now, our attacker synthesis problem becomes checking whether we can find some process $A$ such that $P \comp A \not\models \phi$. Hippel et al. showed finding such an $A$ can be done algorithmically, maintaining soundness and completeness guarantees, %given the input and output transition labels of $A$, denoted $\ioint (A)$, is a subset of $\ioint (Q)$. In particular, Hippel et al. describes gadgets dubbed "daisies" which consist of a main state, a recovery state, circular transitions for each input and output label on the main state, and a non-deterministic transition to the recovery state. To construct $A$, $P \comp Daisy(Q) \models \phi$ is checked. %In short, \spin implements model checking by reducing Promela models to a \ba (a $\omega$-regular automata), converting a Linear Temporal Logic property into a \ba, intersecting the two to construct a product automata, and determining if there exists a reachable acceptance cycle \cite{Vardi_Wolper_1986}. %We know by Vardi, we can always generate a \ba that accepts the traces of any given Kripke structure \cite{Vardi_Wolper_1986, clarke2000model}. Thus, defining the transition relations in our \ba to match the I/O transition labels in their respective processes, we can convert $P$, $Daisy(Q)$, and $\phi$ to \ba and intersect them with \spin. %Then, \spin will soundly and completely search the product automata for acceptance cycles, either finding a counterexample to $\phi$ or proving the absence of such a trace. %\end{proof} %By the previous argument, the R-$\exists$ASP problem reduces to intersecting multiple \ba, which is well-known to be PSPACE-complete \cite{Kozen_1977}. \subsection{\korg Implementation}% \label{sub:impl} We implemented \korg on top of the \spin, a popular and robust model checker for reasoning about distributed and concurrent systems. \spin has existed for over 40 years, and has been applied to dozens of real systems including the Mars Rover \cite{Holzmann_2014}, Path-Star Access server \cite{Holzmann_Smith_2000}, and an avionics operating system \cite{mcp}. Additionally, \spin has spawned a dedicated formal methods symposium, currently in its 32nd year\footnote{\url{https://spin-web.github.io/SPIN2025/}}, and earned the 2002 ACM Software System award. Intuitively, models written in \promela, the modeling language of \spin, are communicating state machines whose messages are passed over defined \textit{channels}. Channels in \promela can either be unbuffered \textit{synchronous} channels, or buffered \textit{asynchronous} channels. \korg generates attacks \textit{with respect} to these defined channels. \begin{lstlisting}[caption={Example \promela model of peers communicating over a channel. \texttt{!} indicates sending a message onto a channel, \texttt{?} indicates receiving a message from a channel.}, label={lst:spin-model}] // channel of buffer size 0 chan msg_channel = [0] of { int } active proctype Peer1() { msg_channel ! 1; } active proctype Peer2() { int received_msg; msg_channel ? received_msg; } \end{lstlisting} \korg is designed to parse user-chosen channels and generate gadgets for sending, receiving, and manipulating messages on them. \korg has built-in gadgets that are designed to emulate various real-world attacker models. %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} To demonstrate the usage of \korg, we provide a step-by-step example of proving the alternate bit protocol (ABP) is secure with respect to attackers that can replay messages. ABP is a simple communication protocol that provides reliable communication between two peers over an unreliable communication by continually agreeing on a bit value. To use \korg, the user first authors a \promela model and a correctness property in LTL. For example, take the \promela model as shown in Listing \ref{lst:abp}. The sender repeatedly sends its stored bit, \texttt{A\_curr}, to the receiver. The receiver changes its internal bit, \texttt{B\_curr}, and sends an acknowledgement to the sender. When the sender receives the acknowledgement, it will bitflip \texttt{A\_curr} and repeatedly send the updated bit. A natural specification for this protocol, formalized into the LTL property \texttt{eventually\_agrees}, states that if the sender and receiver do not currently agree on a bit, they eventually will be able to reach an agreement. \begin{lstlisting}[caption={Example (simplified) \promela model of the alternating bit protocol.}, label={lst:abp}] chan StoR = [2] of { bit }; chan RtoS = [2] of { bit }; bit A_curr = 0, B_curr = 1, rcv_a, rcv_b; active proctype Sender(){ do :: StoR ! A_curr; :: RtoS ? rcv_a -> if :: rcv_a == A_curr -> A_curr = (A_curr + 1) % 2; fi od } active proctype Receiver(){ do :: RtoS ! B_curr; :: StoR ? rcv_b -> :: rcv_b != B_curr -> B_curr = rcv_b; fi od } ltl eventually_agrees { (A_curr != B_curr) implies eventually (A_curr == B_curr) } \end{lstlisting} Next, the user selects a \textit{channel} to generate an attacker on, and an attacker model of choice. For example, we select \texttt{StoR} and \texttt{RtoS} as our channels of choice, \texttt{replay} as our attacker model of choice, and assume the ABP model is in the file \texttt{abp.pml}. Then, we run \korg via command line. \begin{lstlisting}[label={lst:korg-shell}] $ ./panda --model=abp.pml --attacker=replay --channel=StoR,RtoS --eval \end{lstlisting} \korg will then modify the \texttt{abp.pml} file to include the \texttt{replay} attacker gadgets attacking channels \texttt{StoR} and \texttt{RtoS}, and model-check it with \spin. \korg outputs the following text, cut down for readability, indicating an exhaustive search for attacks: \begin{lstlisting} Full statespace search for: never claim + (eventually_agrees) ltl eventually_agree ((A_curr!=B_curr))) implies (eventually ((A_curr==B_curr)) PANDA's exhaustive search is complete, no attacks found! \end{lstlisting} If desired, \texttt{--output} can also be specified so the \korg-modified \texttt{abp.pml} can be more closely examined and modified. A full shell-script replicating this example is available in the artifact. \begin{comment} % JAKE'S OLD EXAMPLE (TO BE IGNORED) Take the following producer-consumer model, as shown in Listing \ref{lst:prod-consume}. \begin{lstlisting}[caption={Example \promela model with four producers and one consumer.}, label={lst:prod-consume}] chan msgs = [4] of { bit }; int count = 0; active [1] proctype Producer() { do :: atomic { count++; msgs ! 1; } od } active [4] proctype Consumer() { do :: atomic { msgs ? 1 -> count--; } od } ltl always_positive { always (count >= 0) } \end{lstlisting} Next, the user selects a \textit{channel} to generate an attacker on, and an attacker model of choice (see Section \ref{sec:usage_attacker_models} for more details). For example, we select \texttt{msgs} as our channel of choice, \texttt{replay} as our attacker model of choice, and assume the producer-consumer model is in the file \texttt{pc.pml}. Then, we run \korg via command line. \begin{lstlisting}[label={lst:korg-shell}] $ ./korg --model=pc.pml --attacker=replay --channel=msgs --eval \end{lstlisting} \korg will then modify the \texttt{pc.pml} file to include the \texttt{replay} attacker gadget, and model-check it with \spin. Then, \korg will find and output the simple attack trace where a producer message is replayed, causing a consumer to consume an extra time. The (simplified) attack trace is shown below. \begin{lstlisting}[label={trace}] (Producer) ko.pml:5 Send 1 -> queue 1 (msgs) (Atk) ko.pml:22 [Recv] 1 <- queue 1 (msgs) (Atk) ko.pml:23 Send 1 -> queue 2 (a_mem) (Atk) ko.pml:47 Recv 1 <- queue 2 (a_mem) (Atk) ko.pml:47 Send 1 -> queue 1 (msgs) (Consumer) ko.pml:9 Recv 1 <- queue 1 (msgs) (Consumer) ko.pml:9 Recv 1 <- queue 1 (msgs) spin: _spin_nvr.tmp:3, assertion violated spin: text of failed assertion: assert(!(!((count>=0)))) Never claim moves to line 3 [assert(!(!((count>=0))))] \end{lstlisting} Additional examples and usage information are provided in the anonymous repository link: (link) \end{comment} %the user inputs a \promela model, a correctness property specified in LTL, a channel from the given \promela model, and an attacker model of choice. \korg will then generate an attacker model gadget corresponding to the selected attacker model with respect to the chosen channel. The attacker model gadget is then appended onto the given \promela model and evaluated against the LTL property with \spin. \korg will then either produce an attack trace demonstrating the precise actions the attacker took to violate the LTL property, or demonstrate the absence of an attack via an exhaustive state-space search. % Precise details of how to use the \korg implementation are provided in the anonymous repository: (link)