synchronous/korg-paper
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fixed a listing

Browse Source
This commit is contained in:
Cristina Nita-Rotaru
2024-12-03 18:17:05 -05:00
parent dec3d1f00d
commit 44df855bf8
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
sections/design.tex
View File

@@ -19,14 +19,14 @@ As aforementioned, \korg is based on \textit{LTL attack synthesis}; in particula
%The methodology behind the construction of \korg is based on \textit{LTL attack synthesis}. %The methodology behind the construction of \korg is based on \textit{LTL attack synthesis}.
\korg is designed to attack user-specified communication channels in state machine-based formal models of distributed protocols. To use \korg, the user inputs a formal model of a distributed protocol in the \promela language, the communication channel(s) the in the formal model they wish to attack, the desired attacker model, and a formalized correctness property for the formal model. The formal model should satisfy the correctness property in absence of \korg. \korg is designed to attack user-specified communication channels in state machine-based formal models of distributed protocols. To use \korg, the user inputs a formal model of a distributed protocol in the \promela language, the communication channel(s) in the formal model they wish to attack, the desired attacker model, and a formalized correctness property for the formal model. The formal model should satisfy the correctness property in absence of \korg.
Once \korg is invoked, it will modify the user-inputted \promela model such that it integrates the desired attacker model. Then, \korg passes the updated \promela model to the model checker, which performs the exhaustive search or provides an explicit counterexample. Once \korg is invoked, it will modify the user-inputted \promela model such that it integrates the desired attacker model. Then, \korg passes the updated \promela model to the model checker, which performs the exhaustive search or provides an explicit counterexample.
%programs written in formal models. The user inputs a formal model of choice, their desired communication channels to attack, the attacker model of choice, and the correctness property of choice. \korg then invokes the model checker, which exhaustively searches for attacks with respect to the chosen attacker model, formal protocol model, and the correctness property. %programs written in formal models. The user inputs a formal model of choice, their desired communication channels to attack, the attacker model of choice, and the correctness property of choice. \korg then invokes the model checker, which exhaustively searches for attacks with respect to the chosen attacker model, formal protocol model, and the correctness property.
%\promela, the modeling language of the \spin model checker. The user inputs a \promela model, %\promela, the modeling language of the \spin model checker. The user inputs a \promela model,
%their desired communication channels to attack, the attacker model of choice, and the LTL correctness property of choice. \korg then invokes \spin, which exhaustively searches for attacks with respect to the chosen attacker model, \promela model, and correctness property. %their desired communication channels to attack, the attacker model of choice, and the LTL correctness property of choice. \korg then invokes \spin, which exhaustively searches for attacks with respect to the chosen attacker model, \promela model, and correctness property.
A high-level visual overview of the \korg pipeline is given in the Figure \ref{fig:korg_workflow}. A high-level visual overview of the \korg pipeline is given in Figure \ref{fig:korg_workflow}.
\begin{figure}[h] \begin{figure}[h]
\centering \centering
@@ -357,7 +357,7 @@ Next, the user selects a \textit{channel} to generate an attacker on, and an att
$ ./panda --model=abp.pml --attacker=replay --channel=StoR,RtoS --eval $ ./panda --model=abp.pml --attacker=replay --channel=StoR,RtoS --eval
\end{lstlisting} \end{lstlisting}
\korg will then modify the \texttt{abp.pml} file to include the \texttt{replay} attacker gadgets attacking channels \texttt{StoR} and \texttt{RtoS}, and model-check it with \spin. \korg outputs the following text, cut down for readability, indicating an exhaustive search for attacks: \korg will then modify the \texttt{abp.pml} file to include the \texttt{replay} attacker gadgets attacking channels \texttt{StoR} and \texttt{RtoS}, and model-check it with \spin. \korg outputs the following text, cut down for readability, indicating an exhaustive search for attacks:\\\\
\begin{lstlisting} \begin{lstlisting}
Full statespace search for: Full statespace search for:
never claim + (eventually_agrees) never claim + (eventually_agrees)