185 lines
13 KiB
TeX
185 lines
13 KiB
TeX
\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{Arguments for \korg's Soundness, Completeness, and Complexity}%
|
|
\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.
|
|
|
|
\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}
|
|
|
|
\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, as defined in \cite{Hippel2022}, always directly corresponds to a \ba.
|
|
\end{theorem}
|
|
|
|
\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 \cite{Hippel2022}, is equivalent to B\"uchi Automata language inclusion (which is in turn solved by the \spin model checker).
|
|
\end{theorem}
|
|
|
|
\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}
|
|
\]
|
|
Where rendezvous composition for I/O \ba is precise the same as for I/O Kripke Automata; that is, input and output transitions are matched. It's easy to see these composition operations are equivalent.
|
|
\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}, is in PSPACE.
|
|
\end{theorem}
|
|
|
|
\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}
|
|
|
|
\subsection{Priorities \& On-the-fly B\"uchi Automata Composition}%
|
|
\label{sub:Priority}
|
|
|
|
As described in Appendix Section \ref{sub:Proofs of Soundness and Completeness}, \spin reduces verification problems to deciding B\"uchi Automata intersection emptiness. That is, given $n$ B\"uchi Automata programs $P_1,\ldots.,P_n$, \spin decides:
|
|
\[
|
|
L(P_1) \cap L(P_2) \cap \ldots \cap L(P_n) = \emptyset
|
|
\]
|
|
Or equivalently:
|
|
\[
|
|
\exists w \in \Sigma \text{ such that } w \in \bigcap_{i=1}^n L(P_i)
|
|
\]
|
|
The canonical decision procedure for deciding intersection emptiness involves constructing a composite automata $P_1 \mid \mid P_2 \mid \mid \ldots \mid \mid P_n$ whose acceptance states are the intersection of each process's acceptance states. Then, this composite automata is exhaustively searched. This method is infeasible in practice, as it requires building the entire automata -- which is $\: \vert \: P_1 \: \vert \: \times \ldots \times \: \vert \: P_n \: \vert \:$ in size -- in memory.
|
|
|
|
Therefore, every practical intersection emptiness implementation employs \textit{on-the-fly composition} to search the composite automata without explicitly constructing it in memory. Recall the \BA is defined as a 5-tuple (as defined in Appendix Section \ref{sub:Proofs of Soundness and Completeness}), $(Q, \Sigma, \delta, Q_0, F)$. The state of the composite automata is denoted as $(q^{(P_1)}, \ldots,q^{(P_n)}$) where $q^{(P_i)} \in Q^{(P_i)}$, for $1 \leq i \leq n$. Similarly, the transition function becomes:
|
|
\begin{equation*}
|
|
\begin{aligned}
|
|
\delta : &\left( (\delta^{(P_1)} : Q^{(P_1)} \times \Sigma) \times \ldots \right \left. \times (\delta^{(P_n)} : Q^{(P_n)} \times \Sigma) \right) \\
|
|
& \to (Q^{(P_1)} \times \ldots \times Q^{(P_n)})
|
|
\end{aligned}
|
|
\end{equation*}
|
|
Such that only one such $\delta^{(P_i)}$ can be invoked per transition of $\delta$. Therefore, \textit{priorities} in \spin are implemented by always invoking the highest priority $\delta^{(P_i)}$ among all the possible process transition functions that can be invoked.
|
|
|
|
% \begin{figure}[h!]
|
|
% \centering
|
|
% \begin{tikzpicture}
|
|
% % Top row (adjusted X positions for even closer horizontal spacing)
|
|
% \node (M) at (0,6.25) {\Large $\mathcal{M}$};
|
|
% \node (mod) at (2.5,6.25) {\Large $\models$}; % Moved even closer horizontally
|
|
% \node (phi) at (5,6.25) {\Large $\varphi$}; % Moved even closer horizontally
|
|
|
|
% % Labels for the top row
|
|
% % \node (t1) at (0, 5.5) {\text{Kripke Structure} \\ \text{of Promela Model}};
|
|
|
|
% \node (t1) at (0, 5.5) {\parbox{3cm}{\centering Kripke Structure \\ of Promela Model}};
|
|
% \node (t2) at (2.5, 5.65) {\textcolor{red}{\text{???}}}; % Moved even closer horizontally
|
|
% \node (t3) at (5, 5.5) {\text{LTL Formula}}; % Moved even closer horizontally
|
|
|
|
% % Downward arrows
|
|
% \node (d1) at (0, 4.75) {\Large \textcolor{red}{$\downarrow$}};
|
|
% \node (d2) at (5, 4.75) {\Large \textcolor{red}{$\downarrow$}}; % Moved even closer horizontally
|
|
|
|
% % Middle row with the automaton languages
|
|
% \node (q1) at (0,4) {\Large $L(\mathcal{M}_A)$};
|
|
% \node (q2) at (2.5,4) {\Large $\cap$}; % Moved even closer horizontally
|
|
% \node (q3) at (5,4) {\Large $L(\overline{\varphi_A})$}; % Moved even closer horizontally
|
|
|
|
% % Bottom row (Büchi Automata labels)
|
|
% \node (t4) at (0, 3.25) {\text{B\"uchi Automaton}};
|
|
% \node (t5) at (5, 3.25) {\text{B\"uchi Automaton}}; % Moved even closer horizontally
|
|
|
|
% \end{tikzpicture}
|
|
% \caption{The SPIN model checker translates user-defined Promela models into Kripkie structures, which is then translated into a B\"uchi Automata. The LTL formula is turned into a never claim (as to avoid an expensive complementation procedure), then translated into a B\"uchi Automata. Then, intersection non-emptiness is checked. }
|
|
% \label{fig:trs}
|
|
% \end{figure}
|