more

sections/design.tex

@@ -3,7 +3,7 @@ In this section we discuss the details behind the design, formal guarantees, imp
 \subsection{High-level design}%
 \label{sub:High-level design}
 
-At the highest level, \korg sits on a user-defined channel in a program written in \promela, the modeling language of the \spin model checker. The user selects an attacker model of choice and correctness properties of choice. \korg then invokes the \spin, which exhaustively searches for attacks with respect to the chosen model and properties. 
+At the highest level, \korg sits on user-specified communication channels in a program written in \promela, the modeling language of the \spin model checker. The user selects an attacker model of choice and correctness properties 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}.
 
 \begin{figure}[h]
@@ -13,6 +13,20 @@ A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg
     \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}
+
+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. 
+
 \subsection{Soundness And Completeness of Korg}%
 \label{sub:Soundness And Completeness}
 
@@ -21,9 +35,12 @@ A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg
 
 Fundamentally, the theoretical framework that \korg implements proposed by Hippel et al. reasons about \textit{communicating processes}; similarly, \korg is best understood as a synthesizer for attackers that sit \textit{between} communicating processes. 
 
-The attack synthesis framework proposed by Hippel et al. and \korg use slightly different formalisms. Both employ derivations the general \textit{input/output automata}, state machines whose transitions indicate sending or receiving a message. In particular, the framework proposed by Hippel et al. defines their own notion of a \textit{process} and argues their attack synthesis framework maintains soundness and completeness guarantees with respect to it, while \korg relies upon \spin's preferred model checking formalism, the B\"uchi Automata. Both utilize linear temporal logic as their specification of choice.
+The theoretical attack synthesis framework and \korg use slightly different formalisms. Both employ derivations the general \textit{Input/Output (I/O) automata}, state machines whose transitions indicate sending or receiving a message.\footnote{
+A fundamental assumption both \korg and the theoretical attack synthesis framework rely upon is unicast transition relations of I/O automata within this context. That is, if one sending automata has an output transition matching an input transition of two receiving automata, only one input/output transition pair can be composed upon. Model checkers for I/O automata such as \spin will explore both possibilities.
+} 
+In particular, the theoretical attack synthesis framework defines their own notion of a \textit{process} and argues their attack synthesis algorithm maintains soundness and completeness guarantees with respect to it, while \korg relies upon \spin's preferred model checking formalism, the B\"uchi Automata. Both utilize linear temporal logic as their specification language of choice.
 
-We ultimately seek to conclude \korg maintains the guarantees of the theoretical framework it implements, therefore it is necessary to demonstrate the equivalence of \textit{processes} from Hippel et al. with the B\"uchi Automata. For ease of reading and clarity, we only provide the shortened arguments here. The detailed theorems and proofs are provided in Appendix Section \ref{sub:korg_proofs}.
+We ultimately seek to conclude \korg maintains the guarantees of the theoretical framework it implements, therefore it is necessary to demonstrate the equivalence of \textit{processes} from the theoretical attack synthesis framework with the B\"uchi Automata. For ease of reading and clarity, we only provide shortened narrations of the arguments here. The detailed, definitions, theorems, and proofs are provided in Appendix Section \ref{sub:korg_proofs}.
 
 %\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.
 
@@ -34,7 +51,7 @@ We ultimately seek to conclude \korg maintains the guarantees of the theoretical
   A process, as defined in Hippel et al., always directly corresponds to a B\"uchi Automata. 
 \end{theorem}
 
-In short, a process as defined in Hippel et al. is a Kripke Structure equipped with input and output transitions. That is, when composing two processes, an output transition must be matched to a respective input transition. Processes also include atomic propositions, which the given linear temporal logic specifications are defined over. We invoke and build on the well-known correspondence between Kripke Structures and \ba to show our desired correspondence.
+In short, a process in the theoretical attack synthesis framework is a Kripke Structure equipped with input and output transitions. That is, when composing two processes, an output transition must be matched to a respective input transition. Processes also include atomic propositions, which the given linear temporal logic specifications are defined over. We invoke and build on the well-known correspondence between Kripke Structures and \ba to show our desired correspondence.
 
 \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).
@@ -75,7 +92,7 @@ Since \korg uses \spin as its underlying model checker, we can effectively concl
 
 We implemented \korg on top of the \spin, a popular and robust model checker for reasoning about distributed and concurrent systems. 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}, label={lst:spin-model}]
+\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 } 
 
@@ -89,12 +106,69 @@ active proctype Peer2() {
 }
 \end{lstlisting}
 
-Following the gadgetry framework as described in Hippel et al., \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, as further described in Section \ref{sec:usage_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.
+\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, as further described in Section \ref{sec:usage_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.
   
 \subsection{Usage}%
 \label{sub:Usage}
 
-To use \korg, the user first authors a \promela model and a correctness property in LTL. Take the following producer-consumer model, as shown in Listing \ref{lst:prod-consume}.
+
+
+To demonstrate the usage of \korg, we'll walk through an 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}]
+$ ./korg --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))
+
+Korg'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 };
@@ -133,6 +207,8 @@ Never claim moves to line 3	[assert(!(!((count>=0))))]
 
 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.