% implementation

\subsection{Model implementation}
The optimization model described in the Section~\ref{sec:optimal_model} represent a SAT Problem, build of boolean variables and equations.
Since the SAT problem is NP-complete, only algorithms with exponential complexity are known for it and a lot of efficient software were developed to solve these types of problems. In this thesis the \textit{z3 Prover} it is chosen to be the engine of the optimization process. 

The optimization process is made of different steps, each one has a representation in the model defined in Section~\ref{sec:optimal_model}.
The process is implemented in {\ttfamily it.polito.policyorchestration .impl.optimization.distribution} package.

\subsection{Binary equation}

\begin{itemize}
	\item 
	The first step is the creation of boolean variables which values represent if a specific rule will be present in a filtering point or not.
	
	\item
	The second step is the creation of the boolean equation that defines all the necessary rules that have to be enforced. The task of this part is to find the rules and policy anomalies and to delete them.
	
	
	\begin{algorithm}[H]
		\SetAlgoLined
		
		\texttt{loop1:}
		$\;$\\
		
		\ForAll{ \textit{fp} in filtering points list}{
			
			$\;$\\
			$\;$\\
			\texttt{loop2:}\Comment{find generalization rule}
			$\;$\\
			\ForAll{ \textit{rule1} in rule list}{
				$\textit{rule2} \gets \text{findIntersectingRule(\textit{rule1})}$\;
				$\;$\\
				\If{$\textit{rule1}.action \ne \textit{rule2}.action$}{
					\For{\textit{rule3} in rule list between \textit{rule1} and \textit{rule2}}{
						$\textit{rule3} \gets \text{findSuperSetRule(\textit{rule1})}$\;
						$\;$\\
						\If{$\textit{rule1}.action = \textit{rule2}.action$}{
							mark: \textit{rule1} as ``redundant''\;
							\Goto \texttt{loop2}
						}
					}
					
				}
				
				\Comment{find preceding superset}
				
				\For{\textit{rule4} in rule list between \textit{firstRule} and \textit{rule1}}{
					
					\If{$\textit{rule1} \subseteq \textit{rule3}$}{
						mark: \textit{rule1} as ``shadowed''\;
						\Goto \texttt{loop2}
					}
				}
				$\;$\\
				mark: \textit{rule1} as ``necessary''\;
				$\;$\\
			}
		}
		
		\caption{optimization model - vertical equation}
		
	\end{algorithm}
\end{itemize}
\clearpage

\subsection{Hard constraints computing}

\begin{itemize}
	\item
	The third step is about adding the constrains to the problem, which is to say make sure that the number of rules injected in each filtering point, does not exceeded the hard constraints given.
	
	\begin{algorithm}[H]
		\SetAlgoLined
		\Begin{
			\ForAll{ \textit{fp} in filtering points list}{
				
				$\textit{counter} \gets 0$\;
				\Comment{count all the rules injected}
				
				\ForAll{ \textit{rule1} in rule list}{
					
					\If{$\textit{rule1} \; is \; marked \; as \; ``necessary''$}{
						$\textit{counter} \gets \textit{counter} + 1$\;
					}
				}
				$\;$\\
				$\textit{max} \gets maxNumberOfRulesSupported(fp)$\;
				
				Set constrain: \textit{counter} $\le$ \textit{max}\;
				$\;$\\
			}
		}
		\caption{optimization model - maximum number of rules}
		
	\end{algorithm}
\end{itemize}

\subsection{Cost function}

\begin{itemize}
	\item 
	The fourth step is the building of the cost function, which exploits the \code{performance tool} to retrieve the performance cost of each filtering point. At this point the STM problem is defined and complete.
	
	\begin{algorithm}[H]
		\SetAlgoLined
		\Begin{
			
			$\textit{costSum} \gets 0$\;
			\Comment{sum performance cost for each filtering point}
			
			\ForAll{ \textit{fp} in filtering points list}{
				
				$currentCost \gets getPerformanceCost(fp)$
				
				$costSum \gets costSum + currentCost$
				
			}
			$\;$\\
			
			Set: $ costFunction \gets costSum $
			$\;$\\
			$\;$\\
		}
		\caption{optimization model - cost function}
		
	\end{algorithm}
	
	
	\item
	The last step has two tasks, the first one checks if the model is \textit{SATISFIABLE}, if it is not the administration will be notified. The second one is to compute the optimization by minimizing the cost function and set for each filtering point the security rules.
\end{itemize}

At the end of this process each filtering point has an minimal ordered list of rules that will be injected on the real or virtual devices behaving as firewall.
