initial commit

sections/design.tex

@@ -0,0 +1,69 @@
+In this section we discuss the details behind the design, implementation, and guarantees of \korg. 
+
+\subsection{High-level design}%
+\label{sub:High-level design}
+TODO: diagram. Promela model, channel selection, gadget selection/definition get put into Korg. Korg spits out another promela model, which is put into Spin along with a property. Then, we get some attacks.
+
+\subsection{The Korg Implementation}%
+\label{sub:The Korg Implementation}
+
+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 synchronous channels, or buffered 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}]
+// 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}
+
+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.
+  
+\subsection{Soundness And Completeness of Korg}%
+\label{sub:Soundness And Completeness}
+
+\newcommand{\comp}{\mid\mid}
+\newcommand{\ioint}{\mathcal{C}}
+\newcommand{\ba}{B\"uchi Automata}
+
+\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{theorem}
+  Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in Hippel et al., reduces to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
+\end{theorem}
+
+\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}
+
+From this result, we naturally get a complexity-theoretic result for finding an attacker from a given threat model.
+
+\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 R-$\exists$ASP problem reduces to intersecting multiple \ba, which is well-known to be PSPACE-complete \cite{Kozen_1977}.
+\end{proof}
+
+Although this result implies \korg has a rough upper bound complexity, in practice due the various implementation-level optimizations of \spin finding attacks on some $\phi$ is generally fast, but proving their absence via a state-space search can expensive.