Merge branch 'wsec_tutorial' into 'master'

Patching W-Sec tutorial

See merge request !436

doc/wsec_tutorial/wsec.tex

@@ -103,11 +103,7 @@ The first W-Sec stage is a modeling stage. As said previously, W-Sec uses two mo
 
 \subsubsection{The model}
 
-<<<<<<< HEAD
 The models designed in this view target capturing high-level architectural and behavioral (discrete and, if applicable, continuous) aspects of the system. The \textbf{wsec\_avatar.xml} file contains AVATAR models of the swarm: open this model in TTool and click on the tab ``\textbf{Nominal}''. You should now see the model depicted in Figure~\ref{fig:avatarmodel}.
-=======
-The models designed in this view target capturing high-level architectural and behavioral (discrete and, if applicable, continuous) aspects of the system. The \textbf{wsec\_avatar.xml} file contains AVATAR models of the swarm: open this model in TTool and click on the tab ``\textbf{Nominal}''. You should now see the model depicted in figure~\ref{fig:avatarmodel}.
->>>>>>> 0b03fe39b9868a7cfd3932c22d781ecb466c14c0
 
 \begin{figure}
 	\centering
@@ -157,7 +153,6 @@ The DIPLODOCUS view is used for modeling the low-level hardware and software asp
 \subsubsection{The application model}
 
 Open in TTool \textbf{wsec\_diplodocus.xml} and click on the \textbf{NoCountermeasureNoAttack} tab. You should now see the component task diagram of the application model of a follower (without any countermeasure). Like the state machine diagram excerpt depicted in Figure~\ref{fig:roversmd}, this application model captures the discrete component of the follower. Explore its structure and the activity diagrams of its tasks: you can notice the difference in the modeling approach between AVATAR and DIPLODOCUS views, with a far more fine-grained modeling in the DIPLODOCUS view.
-<<<<<<< HEAD
 
 \begin{figure}
 	\centering
@@ -167,10 +162,7 @@ Open in TTool \textbf{wsec\_diplodocus.xml} and click on the \textbf{NoCounterme
 \end{figure}
 
 You may have noticed that the arithmetic aspects of the algorithms modeled in the activity diagrams are only expressed with complexity operators: for instance, open the activity diagram of the \texttt{SpeedController} task by double-clicking on the icon in the upper right corner of the task. This activity diagram (see Figure~\ref{fig:ad}) models an iterative task that:
-=======
 
-You may have noticed that the arithmetic aspects of the algorithms modeled in the activity diagrams are only expressed with complexity operators: for instance, open the activity diagram of the \texttt{SpeedController} task by double-clicking on the icon in the upper right corner of the task. This activity diagrams models an iterative task that:
->>>>>>> 0b03fe39b9868a7cfd3932c22d781ecb466c14c0
 \begin{enumerate}
 	\item reads the incoming data
 	\item performs the computation of the motor command
@@ -200,11 +192,8 @@ You will also notice a set of components connected to \texttt{WiFi\_Bus}. These
 	\caption{Excerpt of the mapping model}
 	\label{fig:rovermapping}
 \end{figure}
-<<<<<<< HEAD
+
 Open the \textbf{NoCountermeasureMapping} tab. You should now see that all the tasks and the data channels modeled in the \textbf{NoCountermeasure} application model are now allocated to execution nodes (here, CPUs) and memories. Data channels can be mapped on several communication nodes (buses and bridges): for instance, click on the channel \texttt{NoCountermeasure::fromSAtoDT} mapped on \texttt{BCM2837\_RAM} (see Figure~\ref{fig:rovermapping}). You should notice red dotted lines: these lines indicate on which communication nodes the channel is mapped, i.e., on which buses and bridges the data conveyed on this channel will transit.
-=======
-Open the \textbf{NoCountermeasureMapping} tab. You should now see that all the tasks and the data channels modeled in the \textbf{NoCountermeasure} application model are now allocated to execution nodes (here, CPUs) and memories. Data channels can be mapped on several communication nodes (buses and bridges): for instance, click on the channel \texttt{NoCountermeasure::fromSAtoDT} mapped on \texttt{BCM2837\_RAM} (see figure~\ref{fig:rovermapping}). You should notice red dotted lines: these lines indicate on which communication nodes the channel is mapped, i.e., on which buses and bridges the data conveyed on this channel will transit.
->>>>>>> 0b03fe39b9868a7cfd3932c22d781ecb466c14c0
 
 From this mapping view we can now perform model verification (model-checking and simulation).
 
@@ -278,11 +267,7 @@ The third W-Sec stage consists in:
 
 \subsubsection{Security verification}
 
-<<<<<<< HEAD
 This stage consists in verifying the models of $D_a$ and $D_{a c}$ against the security properties, and then to compare the model checking results. This comparison enables to observe the security properties that are preserved thanks to the countermeasure (positive impact), and the security properties that are no longer verified due to the countermeasure (negative impact).
-=======
-This stage consists in verifying the models of $D_a$ and $D_{a c}$ against the security properties, and then to compare the model checking results in order to tobserve the security properties each countermeasure enables to recover (positive impact) or makes unreachable (negative impact).
->>>>>>> 0b03fe39b9868a7cfd3932c22d781ecb466c14c0
 
 Open \textbf{wsec\_diplodocus.xml} in TTool, and open the \textbf{NoCountermeasureMapping} tab. Perform the syntax analysis, then click on the \textbf{Security verification (ProVerif)} button. Set the \textbf{Compute state reachability} field to \textbf{none}, then click on \textbf{start}. The textbox should provide a \emph{Non Satisfied Authenticity} result for the assessed channel. You can also now click on the \textbf{NoCountermeasure} tab: in the component task diagram, you should notice that the lock linked to the \texttt{fromLSocToSoc} port of the \texttt{Socket} task is red. This backtracing indicates that neither the weak nor the strong authenticity properties are verified on this channel. Click now on the \texttt{MACMapping} tab, and launch the security verification. You should now get a \emph{Satisfied Weak Authenticity} result for the same channel, and the ``W'' part of the lock in the component task diagram under the \textbf{MAC} tab should now be green. This indicates that the channel is protected in integrity (weak authenticity) but not in strong authenticity, since replay attacks can still be led.