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-11-11 07:03:00 -05:00
parent 3281c6d818
commit b17d5fca21
20 changed files with 960 additions and 707 deletions
Download Patch File Download Diff File Expand all files Collapse all files

125
sections/design.tex
View File

@@ -1,14 +1,88 @@
In this section we discuss the details behind the design, implementation, and guarantees of \korg.
In this section we discuss the details behind the design, formal guarantees, implementation, and usage 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.
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.
A high-level overview of the \korg pipeline is given in the Figure \ref{fig:korg_workflow}.
%from a formal model written in \promela.
%user-defined (or derived) \promela models.
%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.
\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{Soundness And Completeness of Korg}%
\label{sub:Soundness And Completeness}
\newcommand{\comp}{\mid\mid}
\newcommand{\ioint}{\mathcal{C}}
\newcommand{\ba}{B\"uchi Automata}
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.
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}.
%\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}
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.
\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}
Via the previous theorem, we can translate the threat model processes and the victim processes to \ba and intersect them. B\"uchi Automata intersection corresponds with \ba language inclusion, which is in turn solved by \spin. From this result, we naturally get a complexity-theoretic result for finding an attacker from a given threat model.
%\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}
\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}
By the previous argument the attack synthesis problem reduces to intersecting multiple \ba (or alternatively \ba language inclusion), which is well-known to be PSPACE-complete \cite{Kozen_1977}.
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 property is generally fast, but proving their absence via a state-space search can expensive \cite{Clarke_Wang}.
Since \korg uses \spin as its underlying model checker, we can effectively conclude \korg is sound and complete.
%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{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.
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{figure}[h]
\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 }
@@ -22,48 +96,13 @@ active proctype Peer2() {
msg_channel ? received_msg
}
\end{lstlisting}
\end{figure}
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}
\subsection{Usage}%
\label{sub:Usage}
\newcommand{\comp}{\mid\mid}
\newcommand{\ioint}{\mathcal{C}}
\newcommand{\ba}{B\"uchi Automata}
To use \korg, 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.
\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.
Precise details of how to use the \korg implementation are provided in the anonymous repository: (link)