more

sections/proofs.tex

@@ -1,36 +1,115 @@
-\subsection{Soundness And Completeness of \korg}%
-\label{sub:Soundness And Completeness}
+\korg is an implementation of the theoretical attack synthesis framework proposed by \cite{Hippel2022_anonym}. 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 \cite{Hippel2022_anonym} 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.
 
-\newcommand{\comp}{\mid\mid}
-\newcommand{\ioint}{\mathcal{C}}
+There exists a semantic gap between the theoretical attack synthesis framework proposed by \cite{Hippel2022_anonym}, 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.
 
-Fundamentally, the theoretical framework that \korg implements was presented in \cite{Hippel2022_anoym} about \textit{communicating processes}; similarly, \korg is best understood as a synthesizer for attackers that sit \textit{between} communicating processes. 
+\begin{definition}[\ba]
+A \ba is a tuple \( B = (Q, \Sigma, \delta, Q_0, F) \) where:
+\begin{itemize}
+    \item \( Q \) is a finite set of states,
+    \item \( \Sigma \) is a finite alphabet,
+    \item \( \delta \subseteq Q \times \Sigma \times Q \) is a transition relation,
+    \item \( Q_0 \subseteq Q \) is a set of initial states,
+    \item \( F \subseteq Q \) is a set of accepting states.
+\end{itemize}
+A run of a \ba is an infinite sequence of states \( q_0, q_1, q_2, \ldots \) such that \( q_0 \in Q_0 \) and \( (q_i, a, q_{i+1}) \in \delta \) for some \( a \in \Sigma \) at each step \( i \). The run is considered accepting if it visits states in \( F \) infinitely often.
+\end{definition}
 
-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 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}.
+\begin{definition}[Process]
+A \emph{Process} is a tuple \( P = \langle AP, I, O, S, s_0, T, L \rangle \), where:
+\begin{itemize}
+    \item \( AP \) is a finite set of atomic propositions,
+    \item \( I \) is a set of inputs,
+    \item \( O \) is a set of output, such that \( I \cap O = \emptyset \),
+    \item \( S \) is a finite set of states,
+    \item \( s_0 \in S \) is the initial state,
+    \item \( T \subseteq S \times (I \cup O) \times S \) is the transition relation,
+    \item \( L: S \to 2^{AP} \) is a labeling function mapping each state to a subset of atomic propositions.
+\end{itemize}
+A transition \( (s, x, s') \in T \) is called an \emph{input transition} if \( x \in I \) and an \emph{output transition} if \( x \in O \).
+\end{definition}
 
+\setcounter{theorem}{0} 
 \begin{theorem}
-  A process, always directly corresponds to a B\"uchi Automata. 
+  A process, as defined in \cite{Hippel2022_anonym}, always directly corresponds to a \ba.
 \end{theorem}
 
-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{proof}
+
+Given a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \), we construct a corresponding Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) as follows:
+
+\begin{itemize}
+    \item Atomic Propositions: \( AP = \{ \text{accept} \} \), a singleton set containing a special proposition indicating acceptance.
+    \item Inputs and Outputs: \( I = \Sigma \) and \( O = \emptyset \).
+    \item States: \( S = Q \) and \( s_0 \in Q_0 \).
+    \item Transition Relation: \( T = \delta \).
+    \item Labeling Function: \( L: S \to 2^{AP} \) defined by
+\end{itemize}
+\[        
+  L(s) = 
+  \begin{cases}            
+  \{ \text{accept} \} & \text{if } s \in F, \\            
+  \emptyset & \text{otherwise}.        
+  \end{cases}    
+\]
+
+In this mapping, the states and transitions of the BA are preserved in the Process, and the accepting states \( F \) are identified via the labeling function \( L \).
+
+Conversely, given a Process \( P = \langle AP, I, O, S, s_0, T, L \rangle \) with an acceptance condition defined by a distinguished proposition \( p \in AP \), we define a \ba \( B = (Q, \Sigma, \delta, Q_0, F) \) as follows:
+
+\begin{itemize}
+    \item States: \( Q = S \) and \( Q_0 = \{ s_0 \} \).
+    \item Alphabet: \( \Sigma = I \cup O \).
+    \item Transition Relation: \( \delta = T \).
+    \item Accepting States: \( F = \{ s \in S \mid p \in L(s) \} \).
+\end{itemize}
+
+Here, the accepting states in the BA correspond to those states in the Process that are labeled with the distinguished proposition \( p \).
+
+In both structures, a run is an infinite sequence of states connected by transitions:
+
+\begin{itemize}
+    \item In the \ba: \( q_0, q_1, q_2, \ldots \) with \( q_0 \in Q_0 \) and \( (q_i, a_i, q_{i+1}) \in \delta \) for some \( a_i \in \Sigma \).
+    \item In the Process: \( s_0, s_1, s_2, \ldots \) with \( s_0 = s_0 \) and \( (s_i, x_i, s_{i+1}) \in T \) for some \( x_i \in I \cup O \).
+\end{itemize}
+
+An accepting run in the \ba visits states in \( F \) infinitely often. Similarly, an accepting run in the Process visits states labeled with \( p \) infinitely often. Since \( F = \{ s \in S \mid p \in L(s) \} \), the acceptance conditions are preserved under the mappings.
+  
+\end{proof}
+
+\begin{definition}[Threat Model]
+A threat model is a tuple \( (P, (Q_i)_{i=0}^m, \phi) \) where:
+\begin{itemize}
+    \item \( P, Q_0, \ldots, Q_m \) are processes.
+    \item Each process \( Q_i \) has no atomic propositions (i.e., its set of atomic propositions is empty).
+    \item \( \varphi \) is an LTL formula such that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \models \phi \).
+    \item The system \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) satisfies the formula \( \phi \) in a non-trivial manner, meaning that \( P \parallel Q_0 \parallel \cdots \parallel Q_m \) has at least one infinite run.
+\end{itemize}
+\end{definition}
 
 \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).
+  Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022_anonym}, 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}
+  For a given threat model \( (P, (Q_i)_{i=0}^m, \phi) \), checking $\exists ASP$ is equivalent to checking
+  \[
+  R = MC(P \mid \mid \text{Daisy}(Q_0) \mid \mid \ldots \mid \mid \text{Daisy}(Q_m), \phi)
+  \] 
+  Where $MC$ is a model checker, and Daisy($Q_i$) is for intents of this proof, equivalent to a process. Therefore, via the previous theorem we can construct \ba \( BA_{P}, BA_{\text{Daisy}(Q_0)}, \ldots, BA_{\text{Daisy}(Q_m)} \) from the processes \( P, \text{Daisy}(Q_0), \ldots ,\text{Daisy}(Q_m) \). Then, we check
+  \[
+    \text{\spin}(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}, \phi)
+  \] 
+  Or equivalently, translating $\phi$ to the equivalent \ba $BA_{\phi}$ via \cite{Holzmann_1997}, we equivalently check
+  \[
+    \left(BA_{P} \mid \mid BA_{\text{Daisy}(Q_0)} \mid \mid \ldots \mid \mid BA_{\text{Daisy}(Q_m)}\right) \subseteq BA_{\phi}
+  \] 
+\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.
+  Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022_anonym}, 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. 
-
+\begin{proof}
+By the previous argument the $\exists$ASP problem corresponds to \ba language inclusion, which is well-known to be PSPACE-complete \cite{Kozen_1977}.
+\end{proof}