more

sections/proofs.tex

@@ -1,4 +1,20 @@
-\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.
+In this section we describe the theoretical foundations of \korg, arguments of its soundness, completeness, and complexity.
+
+\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$, based upon the distributed systems attacker framework as described in \cite{Hippel2022}.
+
+\subsection{Proofs of Soundness and Completeness}%
+\label{sub:Proofs of Soundness and Completeness}
+
+As aforementioned, \korg is an extended implementation of the theoretical attack synthesis framework proposed by \cite{Hippel2022}. 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} 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 \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.
@@ -31,7 +47,7 @@ A transition \( (s, x, s') \in T \) is called an \emph{input transition} if \( x
 
 \setcounter{theorem}{0} 
 \begin{theorem}
-  A process, as defined in \cite{Hippel2022_anonym}, always directly corresponds to a \ba.
+  A process, as defined in \cite{Hippel2022}, always directly corresponds to a \ba.
 \end{theorem}
 
 \begin{proof}
@@ -87,7 +103,7 @@ A threat model is a tuple \( (P, (Q_i)_{i=0}^m, \phi) \) where:
 \end{definition}
 
 \begin{theorem}
-  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).
+  Checking whether there exists an attacker under a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022}, is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
 \end{theorem}
 
 \begin{proof}
@@ -107,7 +123,7 @@ Where rendezvous composition for I/O \ba is precise the same as for I/O Kripke A
 \end{proof}
 
 \begin{theorem}
-  Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022_anonym}, is in PSPACE.
+  Checking whether there exists an attacker for a given threat model, the R-$\exists$ASP problem as proposed in \cite{Hippel2022}, is in PSPACE.
 \end{theorem}
 
 \begin{proof}